Paper Info
Title
From AADL to Timed Abstract State Machines: A verified model transformation.
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 (ITS). 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. (C) 2014 Elsevier Inc. All rights reserved.
Year
DOI
Venue
2014
10.1016/j.jss.2014.02.058
Journal of Systems and Software
Keywords
Field
DocType
Model-driven engineering,Architecture Analysis and Design Language (AADL),Model transformation,Semantics preservation,Timed Abstract State Machine (TASM),Coq
Model transformation,Programming language,Model-driven architecture,Computer science,Automated theorem proving,Abstract state machines,Formal specification,Real-time computing,Architecture Analysis & Design Language,Semantics,Architecture description language
Journal
Volume
ISSN
Citations 
93
0164-1212
14
PageRank 
References 
Authors
0.61
49
6
Name
Order
Citations
PageRank
Zhibin Yang1352.85
Kai Hu29012.83
Dianfu Ma318130.51
Jean-paul Bodeveix423029.15
Lei Pi5463.15
Jean-Pierre Talpin61163108.42