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
Article (Journal)
French
Le controle des faisceaux d'automobile en temps reel
Automotive engineering | 1992
Un systeme de test temps reel ouvert
Tema Archive | 2010
|SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX
European Patent Office | 2020
|SYSTEME DE PROPULSION HYBRIDE POUR AERONEF A DECOLLAGE ET ATTERRISSAGE VERTICAUX
European Patent Office | 2022
|Atterrissage de deux équipages
Online Contents | 2012