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.
Experimentations de techniques de verification de proprietes temps reel sur un systeme de controle de train d' atterrissage
Experiences in using model checking to verify real time properties of a landing gear control system
2007
13 Seiten, 4 Bilder, 7 Tabellen, 18 Quellen
Aufsatz (Zeitschrift)
Französisch
Le controle des faisceaux d'automobile en temps reel
Kraftfahrwesen | 1992
Un systeme de test temps reel ouvert
Tema Archiv | 2010
|SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX
Europäisches Patentamt | 2022
|SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX
Europäisches Patentamt | 2020
|Système de propulsion hybride pour aéronef à décollage et atterrissage verticaux
Europäisches Patentamt | 2021
|