From AADL to timed abstract state machine: a certified model transformation

Abstract : Architecture Analysis and Design Language (AADL) is an architecture description language standard for embedded realtime systems widely used in the avionics and aerospace industry to model safetycritical 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 semanticspreserving 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 TASMbased translation (for verification purpose). Finally, the verified transformation is mechanized in the theorem prover Coq.
Type de document :
Article dans une revue
Journal of Systems and Software, Elsevier, 2014, Journal of Systems and Software, pp.20
Liste complète des métadonnées

https://hal.inria.fr/hal-01095002
Contributeur : Jean-Pierre Talpin <>
Soumis le : dimanche 14 décembre 2014 - 19:38:35
Dernière modification le : mercredi 11 avril 2018 - 02:01:16

Identifiants

  • HAL Id : hal-01095002, version 1

Citation

Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, et al.. From AADL to timed abstract state machine: a certified model transformation. Journal of Systems and Software, Elsevier, 2014, Journal of Systems and Software, pp.20. 〈hal-01095002〉

Partager

Métriques

Consultations de la notice

336