OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A formal approach to AADL model-based software engineering

Mkaouar, Hana and Zalila, Bechir and Hugues, Jérôme and Jmaiel, Mohamed A formal approach to AADL model-based software engineering. (2020) International Journal on Software Tools for Technology Transfer, 22 (2). 219-247. ISSN 1433-2779

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/s10009-019-00513-7


Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies.

Item Type:Article
HAL Id:hal-02988005
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Other partners > Digital Research Center of Sfax (TUNISIA)
Other partners > École Nationale d'Ingénieurs de Sfax - ENIS (TUNISIA)
Other partners > Université de Sfax (TUNISIA)
Laboratory name:
Deposited On:04 Nov 2020 12:38

Repository Staff Only: item control page