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

Context-Aware Verification of a Cruise-Control System

Ciprian Teodorov 1, 2 Luka Leroux 1, 2 Philippe Dhaussy 1, 2
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
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192)
Abstract : Despite the high-level of automation, the practicability of model-checking large asynchronous models is hindered by the state-space explosion problem. To address this challenge the Context-aware Verification technique relies on the identification and explicit specification of the environment (context) in which the system-under-study operates. In this paper we apply this technique for the verification of a Cruise-control System (CCS). The asynchrony of this system renders traditional model-checking approaches almost impossible. Using the Context-aware Verification technique this task becomes manageable by relying on two powerful optimisation strategies enabled by the structural properties of the contexts: automatic context-splitting, a recursive state-space decomposition strategy; context-directed semi-external reachability analysis, an exhaustive analysis technique that reduces the memory pressure during verification through the use of external memory. In the case of the CCS system, this approach enabled the analysis of up to 5 times larger state-spaces than traditional approaches.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01203701
Contributeur : Annick Billon-Coat <>
Soumis le : mercredi 23 septembre 2015 - 15:44:32
Dernière modification le : mercredi 24 juin 2020 - 16:19:35

Identifiants

Citation

Ciprian Teodorov, Luka Leroux, Philippe Dhaussy. Context-Aware Verification of a Cruise-Control System. MEDI 2014, Sep 2015, Larnaca, Cyprus. pp.53-64, ⟨10.1007/978-3-319-11587-0_7⟩. ⟨hal-01203701⟩

Partager

Métriques

Consultations de la notice

642