Write a Blog >>
ECSA 2020
Mon 14 - Fri 18 September 2020 L'Aquila, Italy

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 - 13:00: S2: Model-based ApproachesPaper Presentations / Research Papers / Tool Demos at ECSA 2020 Teams Channel
Chair(s): Rafael CapillaUniversidad Rey Juan Carlos, Manuel WimmerJohannes Kepler University Linz

Virtualization support: Claudio Di Sipio

12:00 - 12:20
Research Papers
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
Research Papers
Martina De SanctisGran Sasso Science Institute, Ludovico IovinoGran Sasso Science Institute, L'Aquila, Maria Teresa RossiGran Sasso Science Institute, Manuel WimmerJohannes Kepler University Linz
12:40 - 13:00
Tool Demos
Bahar SchwichtenbergPaderborn University, Gregor EngelsPaderborn University