1. Verification of AADL Models with Timed Abstract State Machines
- Author
-
Yang, Zhibin, Hu, Kai, Zhao, Yong-Wang, Ma, Dian-Fu, Bodeveix, Jean-Paul, Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées, Beihang University (BUAA), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Toulouse III - Paul Sabatier (UT3), Centre National de la Recherche Scientifique - CNRS (FRANCE), Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE), Université Toulouse III - Paul Sabatier - UT3 (FRANCE), Université Toulouse - Jean Jaurès - UT2J (FRANCE), Université Toulouse 1 Capitole - UT1 (FRANCE), Beihang University (CHINA), and Institut National Polytechnique de Toulouse - INPT (FRANCE)
- Subjects
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] ,[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] ,Modélisation et simulation ,Systèmes embarqués ,Interface homme-machine ,[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation ,Model transformation ,Formal verification ,[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] ,Architectures Matérielles ,Cryptographie et sécurité ,AADL (architecture analysis and design language) ,Génie logiciel ,TASM (timed abstract state machine ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,[INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC] - Abstract
National audience; This paper presents a formal verification method for AADL (architecture analysis and design language) models by TASM (timed abstract state machine) translation. The abstract syntax of the chosen subset of AADL and of TASM are given. The translation rules are defined clearly by the semantic functions expressed in a ML-like language. Furthermore, the translation is implemented in the model transformation tool AADL2TASM, which provides model checking and simulation for AADL models. Finally, a case study of space GNC (guidance, navigation and control) system is provided.
- Published
- 2015