Model-based techniques for the future integration for formal verification of critical real-time software systems

Abstract

Integrated modular avionics architectures combined with the emerging SAE TTEthernet standard provides a strong infrastructure for the deployment of mixed-critical avionic applications that meet stringent safety, reliability and performance requirements. Integrating these systems is a complex and challenging engineering task. Of paramount importance is the development of a model-based approach that can endow system engineers with a methodology and supporting tools to cope with this complexity. In this thesis, we present an extension of AADL, the standard language used for architecture and analysis modeling, in order to enable the modeling of integrated multi-critical avionic applications deployed on TTEthernet-based IMA architectures. To do this, we first present a metamodel for the TTEthernet domain followed by an extension of the core AADL metamodel with concepts and constraints relevant for this domain. In doing so, we define the concrete textual syntax for this extension, and we outline the implementation of this extension using the Open Source AADL Tool Environment (OSATE). To verify the AADL model for TTEthernet, we build on our extension of AADL and leverage model transformations to assess the system models produced with this methodology. In this process, we transform the system models to a target model that is compatible with DEVS formalism in its dedicated simulation environment. We illustrate the proposed approach using a case study provided by Bombardier, our industrial partner in this project, and we show the benefits of our AADL extension and verification approach to the contention-freedom property of the TTEthernet schedule.

Date	19 Oct 2016
Original language	American English
Awarding Institution	École de technologie supérieure
Supervisor	Abdelouahed Gherbi (Supervisor)