OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Towards a verified transformation from AADL to the formal component-based language FIACRE

Bodeveix, Jean-Paul and Filali, Mamoun and Garnacho, Manuel and Spadotti, Régis and Yang, Zhibin Towards a verified transformation from AADL to the formal component-based language FIACRE. (2015) Science of Computer Programming, 106. 30-53. ISSN 0167-6423

(Document in English)

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

Official URL: http://dx.doi.org/10.1016/j.scico.2015.03.003


During the last decade, aadl  is an emerging architecture description languages addressing the modeling of embedded systems. Several research projects have shown that aadl  concepts are well suited to the design of embedded systems. Moreover, aadl  has a precise execution model which has proved to be one key feature for effective early analysis. In this paper, we are concerned with the foundational aspects of the verification support for aadl. More precisely, we propose a verification toolchain for aadl  models through its transformation to the Fiacre language which is the pivot verification language of the TOPCASED project: high level models can be transformed to Fiacre  models and then model-checked. Then, we investigate how to prove the correctness of the transformation from AADL into Fiacre and present related elementary ingredients: the semantics of aadl  and Fiacre  subsets expressed in a common framework, namely timed transition systems. We also briefly discuss experimental validation of the work.

Item Type:Article
Additional Information:Thanks to Elsevier editor. The definitive version is available at http://www.sciencedirect.com The original PDF of the article can be found at Science of Computer Programming website : http://www.sciencedirect.com/science/article/pii/S0167642315000647
HAL Id:hal-01278902
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Nanjing University of Aeronautics and Astronautics – NUAA (CHINA)
Laboratory name:
Deposited On:02 Feb 2016 12:40

Repository Staff Only: item control page