Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Context Aware Model Exploration with OBP tool to Improve Model-Checking

Abstract : This paper deals with the problem of the usage of formal techniques, based on model checking, where models are large and formal verification techniques face the combinatorial explosion issue. The goal of the approach is to express and verify requirements relative to certain context situations. The idea is to unroll the context into several scenarios and successively compose each scenario with the system and verify the resulting composition. We propose to specify the context in which the behavior occurs using a language called CDL (Context Description Language), based on activity and message sequence diagrams. The properties to be verified are specified with textual patterns and attached to specific regions in the context. This article shows how this combinatorial explosion could be reduced by specifying the environment of the system to be validated. Our contribution is illustrated on an industrial embedded system and using the TINA and OBP modelcheckers.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-00676640
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 5 mars 2012 - 18:25:29
Dernière modification le : mercredi 24 juin 2020 - 16:19:22

Identifiants

  • HAL Id : hal-00676640, version 1

Citation

Philippe Dhaussy, Jean-Charles Roger, Luka Leroux, Frédéric Boniol. Context Aware Model Exploration with OBP tool to Improve Model-Checking. ERTS 2012, Feb 2012, Toulouse, France. ⟨hal-00676640⟩

Partager

Métriques

Consultations de la notice

377