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

Context-aware Veri cation of a Landing Gear System

Philippe Dhaussy 1 Ciprian Teodorov 1
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Despite the high level of automation, the practicability of formal veri cation through model-checking of large models is hindered by the combinatorial explosion problem. In this paper we apply a novel context-aware veri cation technique to the Landing Gear System (LGS). The idea is to express and verify requirements relative to certain environ- mental situations. The system environment is decomposed into several independent scenarios (contexts), which are successively composed with the system during reachability analysis. These contexts are speci ed us- ing a language called CDL (Context Description Language), based on activity and message sequence diagrams. The properties to be veri ed are speci ed with observer automata and attached to speci c regions in the context. This approach enables an automated context-guided de- composition of the veri cation into smaller problems, hence e ectively reducing the state-space explosion problem. In the case of the LGS this technique enabled the fully-automated decomposition of the veri cation into 885 smaller model-checking problems.
Liste complète des métadonnées
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 16 juin 2014 - 15:27:56
Dernière modification le : mercredi 24 juin 2020 - 16:19:23


  • HAL Id : hal-01006697, version 1


Philippe Dhaussy, Ciprian Teodorov. Context-aware Veri cation of a Landing Gear System. ABZ 2014, Jun 2014, Toulouse, France. pp.52-65. ⟨hal-01006697⟩



Consultations de la notice