Une méthode d'abstraction pour la vérification des systèmes embarqués distribués (application à l'avionique)

Le caractère distribué des nouvelles architectures embarquées fait apparaître de nouveaux problèmes dans le développement des systèmes. En effet, leur comportement asynchrone nécessite la mise en œuvre de techniques permettant, d une part, la prise en compte de ce phénomène au niveau de la spéci cation, et, d autre part, d aider à la validation de ces systèmes. C est dans le cadre de la vérification formelle et, plus particulièrement, dans l'application du "model checking" que les travaux présentés dans ce mémoire s inscrivent. Après une présentation des techniques couramment utilisées dans le domaine des systèmes temps-réel, la première partie de ce mémoire est consacrée à l étude d un modèle formel permettant la spéci cation des systèmes embarqués distribués. Ce modèle est fondé sur la dé nition d une architecture fonctionnelle, d une plateforme d exécution et d une fonction d allocation. Afin de rendre possible la véri cation formelle d un système, deux étapes de transformation sont détaillées a n de mener à l'expression du modèle de spéci cation dans le formalisme des automates temporisés. En second lieu, nous présentons une méthode de véri cation basée sur l'abstraction d un système. Si l'abstraction d un système tend à limiter l espace des états d un système, cette technique fait naître de nouvelles propriétés devant être véri ées. Pour ce faire, nous proposons un cadre compositionnel permettant de dégager ces obligations de preuve. La validation d une exigence conduit alors à valider les obligations de preuve engendrées par l'abstraction du modèle et l'exigence elle-même.TOULOUSE-ISAE (315552318) / SudocSudocFranceF