Formal Verification of AADL models with Fiacre and Tina
| Autor: | Bodeveix, Jean-Paul, Berthomieu, Bernard, Dal Zilio, Silvano, Gaufillet, Pierre, Dissaux, Pierre, Heim, Sebastien, Filali, Mamoun, Vernadat, François |
|---|---|
| Přispěvatelé: | Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université Toulouse III - Paul Sabatier (UT3), Ellidiss Technologies [Brest], Ellidiss Technologies, Centre National de la Recherche Scientifique (CNRS), Airbus [France], Communication & Systèmes [Toulouse] (C-S), Communication & Systèmes-CS-SI France, DGE Topcased, 3AF Midi-Pyrénées: the French Society of Aeronautic and Aerospace, SEE: the French Society for Electricity, Electronics, and Information & Communication Technologies, SIA: the French Society of Automobive Engineers, ITEA Spices, European Project, Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, 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-Université Toulouse 1 Capitole (UT1) |
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: |
Architecture Description
0209 industrial biotechnology 020901 industrial engineering & automation Verification and Validation 0202 electrical engineering electronic engineering information engineering 020207 software engineering Transportation Model-Driven Engineering [INFO.INFO-ES]Computer Science [cs]/Embedded Systems 02 engineering and technology |
| Zdroj: | ERTSS 2010-Embedded Real-Time Software and Systems ERTSS 2010-Embedded Real-Time Software and Systems, 3AF Midi-Pyrénées: the French Society of Aeronautic and Aerospace; SEE: the French Society for Electricity, Electronics, and Information & Communication Technologies; SIA: the French Society of Automobive Engineers, May 2010, Toulouse, France. pp.1-9, ⟨10.5281/zenodo.32930⟩ ERTSS 2010-Embedded Real-Time Software and Systems, May 2010, TOULOUSE (31000), France. pp.1-9 HAL |
| DOI: | 10.5281/zenodo.32930⟩ |
| Popis: | 9 pages; International audience; This paper details works undertaken in the scope of the Spices project concerning the behavioral verification of AADL models. We give a high-level view of the tools involved and describe the successive transformations performed by our verification process. We also report on an experiment carried out in order to evaluate our framework and give the first experimental results obtained on real-size models. This demonstrator models a network protocol in charge of data communications between an airplane and ground stations. From this study we draw a set of conclusions about the integration of model-checking tools in an industrial development process. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|