↓Skip to main content

Formal Verification of AADL models with Fiacre and Tina

Verification Architecture Languages Fiacre
Table of Contents

Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, Mamoun Filali, Sébastien Heim, Pierre Gaufillet, François Vernadat
In ERTSS 2010 — 5th International Congress and Exhibition on Embedded Real-Time Software and Systems, may 2010.

conference paper

 PDF  DOI〈10.5281/zenodo.32930〉  HAL-00494348

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.

Citation
#


@InProceedings{DalzilioS:aadlTopcased,
   author    = {Berthomieu, Bernard and Bodeveix, Jean-Paul and {Dal Zilio}, Silvano and Dissaux, Pierre and Filali, Mamoun and Heim, Sébastien and Gaufillet, Pierre and Vernadat, François},
   title     = {{Formal Verification of AADL models with Fiacre and Tina}},
   booktitle = {ERTSS 2010 -- 5th International Congress and Exhibition on Embedded Real-Time Software and Systems},
   doi = {10.5281/zenodo.32930},
   month     = may, 
   year      = 2010
}