Formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqués

Un défi bien connu dans le domaine des méthodes formelles est d'améliorer leur intégration dans
les processus de développement industriel. Dans le contexte des systèmes embarqués, l’utilisation des
techniques de vérification formelle nécessitent tout d'abord de modéliser le système à valider, puis de
formaliser les propriétés devant être satisfaites sur le modèle et enfin de décrire le comportement de
l'environnement du modèle. Ce dernier point que nous nommons « contexte de preuve » est souvent négligé.
Il peut être, cependant, d'une grande importance afin de réduire la complexité de la preuve. Dans notre
contribution, nous cherchons à proposer à l’utilisateur une aide pour la formalisation de ce contexte en lien
avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un langage (DSL),
nommée CDL (Context Description Language), pour la description des acteurs de l’environnement, basée sur
des diagrammes d’activités et de séquence et des patrons de définition des propriétés à vérifier. Les propriétés
sont modélisées et reliées à des régions d’exécution spécifiques du contexte. Nous illustrons notre
contribution sur un exemple et décrivons des résultats sur plusieurs applications industrielles embarquées.