OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

From AADL to Timed Abstract State Machines: A Verified Model Transformation

Yang, Zhibin and Hu, Kai and Ma, Dianfu and Bodeveix, Jean-Paul and Pi, Lei and Talpin, Jean-Pierre From AADL to Timed Abstract State Machines: A Verified Model Transformation. (2014) Journal of Systems and Software, vol. 93. pp. 42-68. ISSN 0164-1212

[img]
Preview
(Document in English)

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

Official URL: http://dx.doi.org/10.1016/j.jss.2014.02.058

Abstract

Architecture Analysis and Design Language (AADL) is an architecture description language standard for embedded real-time systems widely used in the avionics and aerospace industry to model safety-critical applications. To verify and analyze the AADL models, model transformation technologies are often used to automatically extract a formal specification suitable for analysis and verification. In this process, it remains a challenge to prove that the model transformation preserves the semantics of the initial AADL model or, at least, some of the specific properties or requirements it needs to satisfy. This paper presents a machine checked semantics-preserving transformation of a subset of AADL (including periodic threads, data port communications, mode changes, and the AADL behavior annex) into Timed Abstract State Machines (TASM). The AADL standard itself lacks at present a formal semantics to make this translation validation possible. Our contribution is to bridge this gap by providing two formal semantics for the subset of AADL. The execution semantics provided by the AADL standard is formalized as Timed Transition Systems (TTS). This formalization gives a reference expression of AADL semantics which can be compared with the TASM-based translation (for verification purpose). Finally, the verified transformation is mechanized in the theorem prover Coq.

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 Journal of Systems and Software website : http://www.sciencedirect.com/science/article/pii/S0164121214000727
HAL Id:hal-01123837
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Other partners > Conservatoire National des Arts et Métiers - CNAM (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Institut National de la Recherche en Informatique et en Automatique - INRIA (FRANCE)
Université de Toulouse > Université Paul Sabatier-Toulouse III - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université de Toulouse I-Sciences Sociales - UT1 (FRANCE)
Other partners > Beihang University (CHINA)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:05 Mar 2015 15:09

Repository Staff Only: item control page