OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

An ocarina extension for AADL formal semantics generation

Mkaouar, Hana and Zalila, Bechir and Hugues, Jérôme and Jmaiel, Mohamed An ocarina extension for AADL formal semantics generation. (2018) In: ACM Symposium on Applied Computing (SAC'18), 9 April 2018 - 13 April 2018 (Pau, France).

(Document in English)

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

Official URL: http://doi.org/10.1145/3167132.3167282


The formal veri cation has become a recommended practice in safety-critical software engineering. The hand-written of the for- mal speci cation requires a formal expertise and may become com- plex especially with large systems. In such context, the automatic generation of the formal speci cation seems helpful and reward- ing, particularly for reused and generic mapping such as hardware representations and real-time features. In this paper, we aim to formally verify real-time systems designed by AADL language. We propose an extension AADL2LNT of the Ocarina tool suite allowing the automatic generation of an LNT speci cation to draw a gateway for the CADP formal analysis toolbox. This work is illustrated with the Pacemaker case study.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-01852034
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > Digital Research Center of Sfax (TUNISIA)
Other partners > Université de Sfax (TUNISIA)
Laboratory name:
Deposited On:31 Jul 2018 13:21

Repository Staff Only: item control page