Analysis of a Complex Architectural Style C2 Using Modeling Language Alloy

摘要

Software architecture plays an important role in the high level design of a system in terms of components, connectors, and configuration. The main building block of software architecture is an architectural style that provides domain specific design semantics. Although many architectural description languages (ADLs) are available in literature for modeling notations to support architecture based development, these ADLs lack proper tool support in terms of formal modeling and visualization. Hence formal methods are used for modeling and verification of architectural styles. In this study, an attempt has been made to formalize one complex style i.e., C2 (component and connector) using formal specification language Alloy. For consistency checking of modeling notations, the model checker Alloy Analyzer is used. It automatically checks properties such as compatibility between components and connectors, satisfiability of predicates over the architectural structure, and consistency of a style. For modeling and verification of C2 architectural style, one case study on cruise control system has been considered. At the end of this study performance evaluation among different SAT solvers associated with Alloy Analyzer has been performed in order to assess the quality.