Expérimentation de composants de preuve pour le développement de composants logiciels embarqués

Pour ameliorer les pratiques industrielles dans le domaine de la validation formelle de modeles de composants embarques, la division Air Systems de Thales et l'ENSIETA ont engage une reflexion commune et des experimentations pour la mise en oeuvre de composants MDA nommes Unites de Modelisation et Unites de Preuve. Le but recherche est de capitaliser au sein de composants de modelisation les donnees et les activites mises en oeuvre dans les processus de conduite des analyses formelles sur les modeles de conception de composants. Ces unites doivent etre manipulees a differents niveaux d'abstraction. En particulier, les Unites de Preuve sont exploitees actuellement dans nos experimentations par une technique de verification de type model-checking avec la mise en oeuvre d'observateurs. Dans une approche Ingenierie Dirigee par les Modeles (IDM), les modeles d'Unites de Modelisation et de preuve sont transformes en modeles d'automates temporises puis en codes exploitables par l'outil OBP (Observer-Based Prover) developpe a l'ENSIETA. Dans cet article, nous decrivons une application de cette approche pour la validation d'un modele de gestion des etats d'un systeme Thales de controle et d'engagement. L'article rend compte du retour d'experience sur la mise en oeuvre de cette technique et la mise en oeuvre des Unites de Preuve.