Mkaouar, Hana and Zalila, Bechir and Hugues, Jérôme and Jmaiel, Mohamed From AADL Model to LNT Specification. (2015) In: Reliable Software Technologies - Ada-Europe 2015 - 20th Ada-Europe International Conference on Reliable Software Technologies, 22 June 2015 - 26 June 2015 (Madrid, Spain).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 352kB |
Official URL: http://dx.doi.org/10.1007/978-3-319-19584-1_10
Abstract
The verification of distributed real-time systems designed by architectural languages such as AADL (Architecture Analysis and Design Language) is a research challenge. These systems are often used in safety- critical domains where one mistake can result in physical damages and even life loss. In such domains, formal methods are a suitable solution for rigorous analysis. This paper studies the formal verification of distributed real-time systems modelled with AADL. We transform AADL model to another specification formalism enabling the verification. We choose LNT language which is an input to CADP toolbox for formal analysis. Then, we illustrate our approach with the ”Flight Control System” case study.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. The definitive version is available at http://link.springer.com/ The original PDF of the article can be found at Reliable Software Technologies – Ada-Europe 2015 website : http://link.springer.com/chapter/10.1007%2F978-3-319-19584-1_10 |
| 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 > Université de Sfax (TUNISIA) |
| Laboratory name: | |
| Statistics: | download |
| Deposited On: | 03 Sep 2015 11:45 |
Repository Staff Only: item control page
