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.
Type de document :
Article dans une revue
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2012, VOL 31 (6), pp.797-826. <10.3166/tsi.31.797-826>
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-00744434
Contributeur : Annick Billon-Coat <>
Soumis le : mardi 23 octobre 2012 - 10:48:55
Dernière modification le : vendredi 13 janvier 2017 - 14:37:15

Identifiants

Citation

Philippe Dhaussy, Frédéric Boniol, Jean-Charles Roger, Amine Raji, Yves Le Traon, et al.. Formalisation de contextes et d'exigences pour la validation formelle de logiciels embarqués. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2012, VOL 31 (6), pp.797-826. <10.3166/tsi.31.797-826>. <hal-00744434>

Partager

Métriques

Consultations de la notice

568