This paper presents experiences in using several model checking tools to verify properties of a critical real time embedded system. The tools they tested are Lesar, SMV, Prover Plug In for SCADE and Uppaal. The application is the landing gear control system of a military aircraft, developed by Dassault Aviation. The property to be verified states that the gear must be down in at most 14 seconds. Results (success and verification time) depend a lot on the way time is handled by the verification tools.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Experimentations de techniques de verification de proprietes temps reel sur un systeme de controle de train d' atterrissage


    Weitere Titelangaben:

    Experiences in using model checking to verify real time properties of a landing gear control system


    Beteiligte:


    Erscheinungsdatum :

    2007


    Format / Umfang :

    13 Seiten, 4 Bilder, 7 Tabellen, 18 Quellen



    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Print


    Sprache :

    Französisch





    Un systeme de test temps reel ouvert

    Belanger, Nicolas / Favarcq, Nicolas / Fusero, Yann et al. | Tema Archiv | 2010


    SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX

    THIRIET ROMAIN JEAN GILBERT / BEDDOK STÉPHANE MEYER | Europäisches Patentamt | 2022

    Freier Zugriff

    SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX

    THIRIET ROMAIN / BEDDOK STÉPHANE | Europäisches Patentamt | 2020

    Freier Zugriff

    Système de propulsion hybride pour aéronef à décollage et atterrissage verticaux

    THIRIET ROMAIN JEAN GILBERT / BEDDOK STÉPHANE MEYER | Europäisches Patentamt | 2021

    Freier Zugriff