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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

12:00 - 13:00
S2: Model-based ApproachesPaper Presentations / Journal First / Industry Program / Workshops / Research Papers / JSS Special Issue / Doctoral Symposium / Gender Diversity in SA / Tool Demos / Social at ECSA 2020 Teams Channel
Chair(s): Rafael Capilla Universidad Rey Juan Carlos, Manuel Wimmer Johannes Kepler University Linz

Virtualization support: Claudio Di Sipio

Empowering SysML-based Software Architecture Description with Formal Verification: From SysADL to CSPResearch Track
Research Papers
Fagner Dias Federal University of Rio Grande do Norte, Marcel Oliveira Federal University of Rio Grande do Norte, Thais Batista Federal University of Rio Grande do Norte, Everton Cavalcante Federal University of Rio Grande do Norte, Jair Leite Federal University of Rio Grande do Norte, Flavio Oquendo IRISA (UMR CNRS) - Univ. Bretagne-Sud (UBS), Camila Araújo State University of Rio Grande do Norte
A Flexible Architecture for the Key Performance Indicators Assessment in Smart CitiesResearch Track
Research Papers
Martina De Sanctis Gran Sasso Science Institute, Ludovico Iovino Gran Sasso Science Institute, L'Aquila, Maria Teresa Rossi Gran Sasso Science Institute, Manuel Wimmer Johannes Kepler University Linz
SecoArc: A Framework for Architecting Healthy Software EcosystemsTool Demo
Tool Demos
Bahar Schwichtenberg Paderborn University, Gregor Engels Paderborn University