Title: Towards a formal specification for an AADL behavioural subset using the LNT language

Authors: Hana Mkaouar; Bechir Zalila; Jérôme Hugues; Mohamed Jmaiel

Addresses: ReDCAD Laboratory, National School of Engineers of Sfax, University of Sfax, 3038 Sfax, Tunisia ' ReDCAD Laboratory, National School of Engineers of Sfax, University of Sfax, 3038 Sfax, Tunisia ' Institut Supérieur de l'Aéronautique et de l'Espace (ISAE-SUPAERO), Université de Toulouse, 31055 Toulouse Cedex 4, France ' Digital Research Center of Sfax, Technopark of Sfax, Sakiet Ezzit, 3021 Sfax, Tunisia

Abstract: The analysis of real-time systems designed by architectural languages such as architecture analysis and design language (AADL) is a challenging research topic. In such a context, formal methods become an advocated practice in software engineering for rigorous analysis. Yet, they are applied on specific formalisms to be analysed on dedicated tools. This paper studies the formal verification of real-time systems modelled with the AADL language and its behaviour annex. We define a formal semantics of an AADL behavioural subset using the LNT language. This work is illustrated with a robot case study.

Keywords: real-time systems; formal verification; architecture analysis and design language; AADL; behaviour annex.

DOI: 10.1504/IJBSR.2020.106278

International Journal of Business and Systems Research, 2020 Vol.14 No.2, pp.162 - 190

Received: 04 Jul 2018
Accepted: 06 Sep 2018
Published online: 02 Apr 2020 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article