%0 Conference Proceedings
%T Context-aware Veri cation of a Landing Gear System
%+ Lab-STICC_ENSTAB_CACS_MOCS
%A Dhaussy, Philippe
%A Teodorov, Ciprian
%< avec comité de lecture
%( ABZ 2014
%B ABZ 2014
%C Toulouse, France
%Y Springer
%P 52-65
%8 2014-06-02
%D 2014
%K observer-automata
%K formal veri cation
%K context-aware model-checking
%K OBP
%K observer-automata...
%Z Computer Science [cs]/Symbolic Computation [cs.SC]
%Z Computer Science [cs]/Software Engineering [cs.SE]
%Z Computer Science [cs]/Modeling and SimulationConference papers
%X 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.
%G English
%L hal-01006697
%U https://hal.science/hal-01006697
%~ UNIV-BREST
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ ENSTA-BRETAGNE-STIC
%~ LAB-STICC
%~ TDS-MACS
%~ INSTITUTS-TELECOM