Formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqués
Résumé
Un des défis posés aux méthodes formelles est leur intégration dans les processus de développement industriel. Une des difficultés rencontrées par les techniques formelles telles que le model-checking est l'explosion de l'espace des états à explorer lors de la vérification. Pour réduire cet espace des états, il est nécessaire de décrire le comportement de l'environnement qui est en interaction avec le système à valider. Cet article s'intéresse à la formalisation de cet environnement que nous nommons " contexte " en lien avec la formalisation des propriétés. Dans ce but, nous proposons et expérimentons un DSL, nommé CDL (Context Description Language) reposant d'une part sur des diagrammes d'activités et de séquences pour l'expression du comportement de l'environnement, et d'autre part sur la notion d'observateur pour l'expression des propriétés à vérifier. Afin de contourner l'explosion des états produite par la composition des modèles de l'environnement et du système à valider, nous appliquons une technique de partitionnement du comportement de l'environnement en sous-contextes analysables séparément. Nous illustrons notre contribution par un exemple, et présentons les retours d'expérience obtenus sur six cas d'études industriels.