Performance Evaluation and Verification of System-Level Architecture Models

In this talk, I will outline the work we carried out for the European Space Agency the past two years under the project COMPASS. The aim was to develop a comprehensive and coherent toolset for analysing aerospace systems using model checking techniques. First I will introduce our case studies in order to get a feeling about the scope of the modelling domain. This is followed by an introduction to AADL, an industry-accepted high-level modelling language for embedded systems, and it is the input language of our tool. We extended it and formally characterised it to cover probabilistic, hybrid and functional aspects. I will close the presentation with a live demo of our toolset, showing a selection of our analyses, among which, hybrid systems model checking of LTL properties, simulation, dynamic fault tree generation, FMEA table generation and performance evaluation of CSL properties.

This is joint work with Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll and Marco Roveri.