Experiences in using model checking to verify real time properties of a landing gear control system
Overview & Synopsis
This paper presents experiences in using several model checking tools to verify properties of a critical real time embedded system. The tools we 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.
Indexed from repository: HAL Open Science
(
hal.science)
Keyboard Shortcuts:
← / → for pages • + / - for zoom • 0 to fit width
Powered by Mozilla PDF.js v3.11
Document Information
| Document Title | Experiences in using model checking to verify real time properties of a landing gear control system |
|---|---|
| Author / Organization | Frédéric Boniol, Virginie Wiels, Emmanuel Ledinot |
| Subject & Discipline | Multidisciplinary Academic Open Research |
| Categories | Science & Mathematics |
| Publication Year | 2006 |
| License / Rights | Open Access / Creative Commons |
| Resource Verification | Listed PDF (Verification Pending) |
| Original Host Website |
HAL Open Science
(hal.science)
|
| File Format | application/pdf (Portable Document Format) |
| Language | EN |
| Catalog ID | DOC-148334 |
| Original Source Link | Visit Source Page on hal.science » |