A Formal Metamodel for Software Architectures with Composite Components

Formal component-based modeling has been shown to be invaluable for verifying the compatibility of specified components, discovering flaws early in design stages, and enabling the reuse of components, across multiple projects and teams. However, complex system specifications are large and difficult to reason with which has limited the adoption of formal approaches. In this paper, we use a formal language to build a metamodel to represent software architectures consisting of composite components. First, we propose a metamodel to describe the high-level concepts of software architectures in a component-port-connector fashion. We focus on providing hierarchical modeling capabilities by considering the construction of composite components from existing ones. Second, using Alloy as a tooled formal language, we formalize the metamodel concepts to build a reusable framework for modeling complex systems consisting of composite component structures that can be automatically constructed and checked for architectural conformance. We use a smart metering system to demonstrate the use our formal metamodel.