Two Formal Semantics of a Subset of the AADL

The analysis and verification of an AADL model usually requires its transformation into the meta-model of this model-checker or that schedulability analysis tool. However, one challenging problem is to prove that the transformation into the target model of computation (MoC) preserves the semantics of the original AADL model or at least some of its properties. Moreover, the AADL standard lacks a formal semantics to make the validation of this translation possible. Albeit some of the related works give informal explanations on the model transformations they apply to interpret or compile AADL, the formal proof of semantics preservation remains in most cases altogether impossible. Our contribution is to bridge this gap by providing two formal semantics for a synchronous subset of AADL, which includes periodic threads and data port communications. Its operational semantics is formalized as a TTS (Timed Transition System). This formalization is one prerequisite to the formal proof of semantics preservation for our model transformation from AADL sources to our target verification formalism: TASM (Timed Abstract State Machine). In this paper, an abstract syntax of (our subset of) AADL is given, together with the abstract syntax of TASM. The translation is formalized by a family of semantics functions, which associates each AADL construct to a TASM fragment. Then, the proof of simulation equivalence between the TTSs of the AADL and the TASM models is formalized and mechanized using the proof assistant Coq.