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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Additional title:

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


    Contributors:


    Publication date :

    2007


    Size :

    13 Seiten, 4 Bilder, 7 Tabellen, 18 Quellen



    Type of media :

    Article (Journal)


    Type of material :

    Print


    Language :

    French





    Un systeme de test temps reel ouvert

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


    SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX

    THIRIET ROMAIN JEAN GILBERT / BEDDOK STÉPHANE MEYER | European Patent Office | 2022

    Free access

    SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX

    THIRIET ROMAIN / BEDDOK STÉPHANE | European Patent Office | 2020

    Free access

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

    THIRIET ROMAIN JEAN GILBERT / BEDDOK STÉPHANE MEYER | European Patent Office | 2021

    Free access