Towards software architecture formalization

Abstract

Errors during the software development may give rise to flaws in the system that can cause important damages. One of the most important stages in the software development process is modelling the system architecture, possibly using software architecture description languages~(ADLs). The ADLs currently adopted by industry for software-intensive systems are mostly semi-formal and essentially based on SysML and specialized profiles. These ADLs allow describing the structure and the behavior of the system. Besides, it is possible to generate executable models or produce code in a target programming language and simulate its behaviour. This, however, does not constitute a proof that the system is correct or safe. This work proposes a novel approach for empowering SysML-based ADLs with formal verification tools supported by model checking. It presents a CSP-based semantics to SysADL models. Furthermore, this work presents how correctness properties can be formally specified using CSP, and how the FDR4 refinement model-checker can verify these correctness properties. Finally, we present the new extension to SysADL studio that allows the automated transformation from SysADL architecture descriptions to CSP processes and the verification of important system correctness properties. The whole approach is illustrated via a case study, which is also part of this document. This case study demonstrates the usefulness of our approach in practice.