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

Jean-Paul Bodeveix (1, 2) , M Filali (1, 3) , Manuel Garnacho (4) , Régis Spadotti (4) , Zhibin Yang (4, 5)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UT3 - Université Toulouse III - Paul Sabatier
3 CNRS - Centre National de la Recherche Scientifique
4 IRIT - Institut de recherche en informatique de Toulouse
5 NUAA - Nanjing University of Aeronautics and Astronautics [Nanjing]

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.

Mots clés: Formal verification; Architecture description languages; Model driven engineering; Model transformation; Timed transition systems

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Jean-Paul Bodeveix, M Filali, Manuel Garnacho, Régis Spadotti, Zhibin Yang. Towards a verified transformation from AADL to the formal component-based language FIACRE. Science of Computer Programming, 2015, vol. 106, pp. 30-53. ⟨10.1016/j.scico.2015.03.003⟩. ⟨hal-01278902⟩