Abstract Despite the high level of automation, the practicability of formal verification through model-checking of large models is hindered by the combinatorial explosion problem. In this paper we apply a novel context-aware verification technique to the Landing Gear System Case Study (LGS) [2]. The idea is to express and verify requirements relative to certain environmental situations. The system environment is decomposed into several independent scenarios (contexts), which are successively composed with the system during reachability analysis. These contexts are specified using a language called CDL (Context Description Language), based on activity and message sequence diagrams. The properties to be verified are specified with observer automata and attached to specific regions in the context. This approach enables an automated context-guided decomposition of the verification into smaller problems, hence effectively reducing the state-space explosion problem. In the case of the LGS this technique enabled the fully-automated decomposition of the verification into 885 smaller model-checking problems.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Context-Aware Verification of a Landing Gear System


    Beteiligte:


    Erscheinungsdatum :

    2014-01-01


    Format / Umfang :

    14 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Context-Aware Verification of a Landing Gear System

    Dhaussy, P. / Teodorov, C. | British Library Conference Proceedings | 2014


    CONTEXT-AWARE LANDING ZONE CLASSIFICATION

    STATHIS CHRISTOPHER | Europäisches Patentamt | 2016

    Freier Zugriff

    CONTEXT-AWARE LANDING ZONE CLASSIFICATION

    STATHIS CHRISTOPHER | Europäisches Patentamt | 2016

    Freier Zugriff

    Context-aware landing zone classification

    STATHIS CHRISTOPHER | Europäisches Patentamt | 2018

    Freier Zugriff