Empowering SysML-based Software Architecture Description with Formal Verification: From SysADL to CSP
Software architecture description languages (ADLs) currently adopted by industry for software-intensive systems are largely semi-formal and essentially based on SysML and specialized profiles. Despite these ADLs allow describing both structure and behavior of the architecture, there is no guarantee regarding the satisfaction of correctness properties. Due to their nature, semi-formal ADLs do not support automated verification of the specified properties, in particular those related to safety and liveness of the specified behavior. This paper proposes a novel approach for empowering SysML-based ADLs with formal verification support founded on model checking. It presents (i) how the semantics of SysADL, a SysML-based ADL, can be formalized in terms of the CSP process calculus, (ii) how correctness properties can be formally specified in CSP, and (iii) how the FDR4 refinement checker allows verifying correctness properties through model checking. The automated model transformation from SysADL architecture descriptions to CSP composite processes has been implemented as a plug-in to the Eclipse-based SysADL Studio tool. This paper also describes an application of SysADL empowered with CSP to validate its usefulness in practice.
Wed 16 Sep Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|12:00 - 12:20|
Empowering SysML-based Software Architecture Description with Formal Verification: From SysADL to CSPResearch Track
Fagner DiasFederal University of Rio Grande do Norte, Marcel OliveiraFederal University of Rio Grande do Norte, Thais BatistaFederal University of Rio Grande do Norte, Everton CavalcanteFederal University of Rio Grande do Norte, Jair LeiteFederal University of Rio Grande do Norte, Flavio OquendoIRISA (UMR CNRS) - Univ. Bretagne-Sud (UBS), Camila AraújoState University of Rio Grande do Norte
|12:20 - 12:40|
|12:40 - 13:00|