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

Un des defis poses aux methodes formelles est leur integration dans les processus de developpement industriel. Une des difficultes rencontrees par les techniques formelles telles que le model-checking est l'explosion de l'espace des etats a explorer lors de la verification. Pour reduire cet espace des etats, il est necessaire de decrire le comportement de l'environnement qui est en interaction avec le systeme a valider. Cet article s'interesse a la formalisation de cet environnement que nous nommons " contexte " en lien avec la formalisation des proprietes. Dans ce but, nous proposons et experimentons un DSL, nomme CDL (Context Description Language) reposant d'une part sur des diagrammes d'activites et de sequences pour l'expression du comportement de l'environnement, et d'autre part sur la notion d'observateur pour l'expression des proprietes a verifier. Afin de contourner l'explosion des etats produite par la composition des modeles de l'environnement et du systeme a valider, nous appliquons une technique de partitionnement du comportement de l'environnement en sous-contextes analysables separement. Nous illustrons notre contribution par un exemple, et presentons les retours d'experience obtenus sur six cas d'etudes industriels.