Enabling Formal Verification of SysML-Based Dynamic Software Architecture: A Model-Driven Approach
Software Architecture, Formal Verification, Architecture Description Language, Model Transformation, Dynamic Architectures.
The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML, SysML, and their derivatives to describe the structure and behavior of software architectures. However, these semi-formal notations have limitations regarding the sought support for architectural analysis, particularly formal verification. This work investigates how to conciliate formal support and SysML-based architecture descriptions, to enable the formal verification of dynamic software architectures. The main contribution is proposing a model-driven approach that: (i) provides formal semantics to a SysML-based architectural language, SysADL, by transforming SysADL architecture descriptions in specifications expressed in pi-ADL, a well-founded theoretically language based on the higher-order typed pi-calculus, and (ii) enables the formal verification of properties for dynamic architectures. These facilities are integrated into an environment that facilitates modeling SysML architectures and formally verifying them.