Formal Verification of AADL models with Fiacre and Tina

Bernard Berthomieu 1 Jean-Paul Bodeveix 2 Silvano Dal Zilio 1 Pierre Dissaux 3 Mamoun Filali 2 Pierre Gaufillet 4 Sebastien Heim 5 François Vernadat 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 IRIT - Institut de recherche en informatique de Toulouse
3 Ellidiss Technologies [Brest]
4 Airbus [France]
5 C-S - Communication & Systèmes [Toulouse]
Abstract : 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.
Keywords : Architecture Description Verification and Validation Model-Driven Engineering Transportation
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download
https://hal.archives-ouvertes.fr/hal-00494348
Contributor : Silvano Dal Zilio <>
Submitted on : Friday, October 30, 2015 - 11:39:19 AM
Last modification on : Friday, October 25, 2019 - 6:20:09 PM
Long-term archiving on : Friday, April 28, 2017 - 5:13:11 AM

File

aadlTopcased.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00494348, version 1

Collections

CNRS | UNIV-TLSE2 | INSA-TOULOUSE | SMS | LAAS-VERTICS | LAAS-INFORMATIQUE-CRITIQUE | LAAS | INSA-GROUPE | UNIV-TLSE3 | INSA-TOULOUSE-GEI | UT1-CAPITOLE

Citation

Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, Mamoun Filali, et al.. Formal Verification of AADL models with Fiacre and Tina. ERTSS 2010 - Embedded Real-Time Software and Systems, May 2010, TOULOUSE (31000), France. pp.1-9. ⟨hal-00494348⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

596

Files downloads

279

CONTACT

scd.ao@univ-tlse3.fr