Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Vérification formelle de propriétés : Application de l'outil OBP au cas d'étude CCS

Philippe Dhaussy 1 Luka Le Roux 2 Ciprian Teodorov 1
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
2 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest]
Résumé : Malgré le niveau élevé d'automatisation des techniques de model-checking, celles-ci se trouvent limitées par le problème de l'explosion du nombre d'états générés lors de l'exploration de modèles de taille importante. Pour répondre à ce défi, nous proposons une technique de vérification prenant en compte la spécification explicite de l'environnement (contexte) dans lequel le modèle du système est plongé lors de son exploration par le vérifieur. Le principe est d'amener l'explorateur à concentrer ses efforts non plus sur l'exploration de l'espace complet des comportements, mais sur une restriction pertinente de ce dernier pour la vérification de propriétés spécifiques. Dans cet article, nous appliquons cette technique à la vérification du régulateur de vitesse (CCS ou Control Cruise Control) décrit dans l'article précédent [21]. L'asynchronisme intrinsèque de ce système rend les approches traditionnelles presque impossibles. En exploitant les contextes, nous montrons que la vérification devient possible en s'appuyant sur deux stratégies efficaces d'optimisation basées sur les propriétés structurelles des contextes. Une première qui met en œuvre un fractionnement automatique du contexte par une décomposition récursive de son espace d'état. Une seconde qui exploite la mémoire disque externe optimisant l'utilisation de la mémoire lors de l'exploration exhaustive du modèle. Dans le cas du système CCS, cette approche a permis l'analyse d'espace d'états 5 fois plus grands que les approches traditionnelles.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01006676
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 16 juin 2014 - 15:09:06
Dernière modification le : mercredi 24 juin 2020 - 16:19:23

Identifiants

  • HAL Id : hal-01006676, version 1

Citation

Philippe Dhaussy, Luka Le Roux, Ciprian Teodorov. Vérification formelle de propriétés : Application de l'outil OBP au cas d'étude CCS. Génie logiciel, C & S, 2014, 109. ⟨hal-01006676⟩

Partager

Métriques

Consultations de la notice

502