Real-Time Model Checking Support for AADL

Silvano Dal Zilio, Bernard Berthomieu, François Vernadat, Mamoun Filali, Jean-Paul Bodeveix, Guillaume Verdier
Research Report 15036, LAAS, mar 2015.

 PDF  HAL-01121605

Abstract

#

We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the AADL Behavioral Annex. We give a high-level view of the tools and transformations involved in the verification process and focus on the support offered by our framework for checking user-defined properties. We also describe the experimental results obtained on a significant avionic demonstrator, that models a network protocol in charge of data communications between an airplane and ground stations.

Citation

#

@TechReport{DalzilioS:rtaadlmodelcheck2015,
   author      = {{Dal Zilio}, Silvano and Berthomieu, Bernard and Vernadat, François and Filali, Mamoun and Bodeveix, Jean-Paul and Verdier, Guillaume},
   title       = {{Real-Time Model Checking Support for AADL}},
   institution = {LAAS},
   number      = {15036}, 
   month       = mar, 
   year        = 2015
}