CTL
7 April 2010 - 13h30
Modelling real-time embedded systems using AADL for the automatic generation of applications formally verified (Phd Defense)
by Mohamed Yassin CHKOURI from VERIMAG
Abstract: The Architecture Analysis & Design Language (AADL) is the subject of increasing interest in the industry of real-time embedded systems. It defines several categories of components, grouped into three major categories (software, hardware, systems). The work realized in this thesis exploits the
features offered by AADL to specify the exact requirements of an application and to express all the features both functional and nonfunctional (temporal and spatial dimensions) required to produce automatically the application. The production methodology that we propose generates automatically from an application described in AADL, an application described in BIP. BIP allows to implement robust and safe systems by producing a correct execution controller design and providing a formal model. The objectives of this production process are : (1) provide to AADL a formal semantics defined in terms of labeled transition systems ; (2) allow analysis and validation, i.e. exhaustive exploration of the state space of the system, the detection of potential deadlocks and verification of certain properties ; (3) allow the generation of an executable application to simulate and debug the AADL models. These last three step play a cental rule for the use of formal methods in the development cycle.
Jury :
M. Jean Claude Fernandez : Professeur UJF (Président)
M. Jean-Paul Bodeveix : Professeur IRIT (Rapporteur)
M. Elie Najm : Professeur ENST (Rapporteur)
M. Marius Bozga : Ingénieur de recherche CNRS (Examinateur)
M. Iulian Ober : Maître de Conférences IRIT (Examinateur)
M. Pierre Gaufillet : AIRBUS (Invité)
M. Joseph Sifakis : DR CNRS (Directeur de thèse)
