Modélisation des systèmes temps-réel embarqués en utilisant AADL pour la génération automatique d'applications formellement vérifiées
Mohamed Yassin Chkouri · HAL (Le Centre pour la Communication Scientifique Directe) · 2010
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.