Accéder directement au contenu Accéder directement à la navigation
Chapitre d'ouvrage

Context Aware Model-Checking for Embedded Software

Philippe Dhaussy 1 Jean-Charles Roger 2 Frédéric Boniol 3, 4
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192), STIC - Pôle STIC [Brest]
2 IDM
STIC - Pôle STIC [Brest]
Abstract : Reactive systems are becoming extremely complex with the huge increase in high technologies. Despite technical improvements, the increasing size of the systems makes the introduction of a wide range of potential errors easier. Among reactive systems, the asynchronous systems communicating by exchanging messages via buffer queues are often characterized by a vast number of possible behaviors. To cope with this difficulty, manufacturers of industrial systems make significant efforts in testing and simulation to successfully pass the certification process. Nevertheless revealing errors and bugs in this huge number of behaviors remains a very difficult activity. An alternative method is to adopt formal methods, and to use exhaustive and automatic verification tools such as model-checkers. Model-checking algorithms can be used to verify requirements of a model formally and automatically. Several model checkers as (Berthomieu et al., 2004; Holzmann, 1997; Larsen et al., 1997), have been developed to help the verification of concurrent asynchronous systems. It is well known that an important issue that limits the application of model checking techniques in industrial software projects is the combinatorial explosion problem (Clarke et al., 1986; Holzmann & Peled, 1994; Park & Kwon, 2006). Because of the internal complexity of developed software, model checking of requirements over the system behavioral models could lead to an unmanageable state space. The approach described in this chapter presents an exploratory work to provide solutions to the problems mentioned above. It is based on two joint ideas: first, to reduce behaviors system to be validated during model-checking and secondly, help the user to specify the formal properties to check. For this, we propose to specify the behavior of the entities that compose the system environment. These entities interact with the system. Their behaviors are described by use cases (scenarios) called here contexts. They describe how the environment interacts with the system. Each context corresponds to an operational phase identified as system initialization, reconfiguration, graceful degradation, etc.. In addition, each context is associated with a set of properties to check. The aim is to guide the model-checker to focus on a restriction of the system behavior for verification of specific properties instead on exploring the global system automaton.
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-00676423
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 5 mars 2012 - 12:03:09
Dernière modification le : mercredi 24 juin 2020 - 16:19:23

Identifiants

  • HAL Id : hal-00676423, version 1

Citation

Philippe Dhaussy, Jean-Charles Roger, Frédéric Boniol. Context Aware Model-Checking for Embedded Software. Embedded Systems - Theory and Design Methodology, InTech, ISBN: 978-953-51-0167-3 p. 167-184, 2012. ⟨hal-00676423⟩

Partager

Métriques

Consultations de la notice

424