Développement et validation d'architectures dynamiques
Résumé
In this thesis, we study the development and the validation of asynchronous real time systems. We choose to use the language AADL for its specificities issued from the avionic industry, and for the precise description of its execution model. This thesis is divided in two main parts. In the first part we study the use of AADL as a support for the development of satellite flight software. In a second part we present a reduced version of AADL and the formal definition of its execution model. The objective of the first part is to demonstrate that AADL can be integrated in an existing development process of the spatial industry. In this part, we have identified several patterns used in the conception of flight software In the second part we define a mini-AADL enough complete to express most of the current concepts of real time systems. The formalization part of the execution model is mandatory for the validation of dynamic properties. This formal description allow to describe the behavior of AADL models. This description can be used with a model checker to animate AADL models and validate dynamic properties.
Dans le cadre de cette thèse, nous nous proposons d'étudier le développement et la validation de systèmes dans un contexte temps réel asynchrone. On a choisi d'utiliser le langage AADL pour ses spécificités issues de l'avionique, domaine proche du spatial, et pour la précision de la description de son modèle d'exécution. Le travail de cette thèse se divise en deux axes principaux : d'une part, on étudie l'utilisation du langage AADL dans le cadre du développement d'un logiciel de vol ; et d'autre part, on présente une version réduite du langage AADL, et la définition formelle de son modèle d'exécution à l'aide du langage TLA+. L'objectif de la première partie est d'envisager l'utilisation d'AADL dans le cadre d'un processus de développement existant dans le domaine du spatial. Dans cette partie, on a cherché à identifier des motifs de conceptions récurrents dans les logiciels de vol. Enfin, on étudie l'expression en AADL des différents éléments de ce processus de développement. La seconde partie comporte la définition d'un mini AADL suffisant pour exprimer la plupart des concepts de parallélisme, de communication et de synchronisation qui caractérisent AADL. La partie formalisation est nécessaire afin de pouvoir vérifier des propriétés dynamiques. En effet, la définition formelle du modèle d'exécution permet de décrire le comportement attendu des modèles AADL. Une fois ce modèle défini, on peut à l'aide d'un vérificateur de modèles (model-checker) animer une modélisation AADL ou aborder la vérification de propriétés dynamiques. Cette étude a par ailleurs été menée dans le cadre de la standardisation du langage AADL.
Loading...