Formal Evaluation of Landing Gear System

Abstract : The failure of hardware or software in a critical system can lead to loss of lives. Design errors are a major source of the defects that can be introduced during the system devel- opment. A complementary approach like formal methods is considered as an alternative approach to identify the possible defects in the software development process using rigorous mathematical reasoning. The increasing system complexity and failure rate invoke the area of verification and validation of avionic systems. This paper describes a stepwise formal development of an aircraft landing system using Event-B. The formal models include the complex behaviour, tempo- ral behaviour and sequence of operations of a landing gear system. The refinement based incremental development al- lows to verify and to validate the required safety properties. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural prop- erties of systems.
Type de document :
Communication dans un congrès
Ngo Hong Son; Yves Deville; Marc Bui. SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam. ACM, 2014, SoICT 2014 fifth symposium on Information and Communication Technology
Liste complète des métadonnées

https://hal.inria.fr/hal-01097645
Contributeur : Dominique Méry <>
Soumis le : samedi 20 décembre 2014 - 15:09:45
Dernière modification le : jeudi 22 septembre 2016 - 14:31:38

Identifiants

  • HAL Id : hal-01097645, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Formal Evaluation of Landing Gear System. Ngo Hong Son; Yves Deville; Marc Bui. SoICT 2014 fifth symposium on Information and Communication Technology,, Dec 2014, HANOI, Vietnam. ACM, 2014, SoICT 2014 fifth symposium on Information and Communication Technology. 〈hal-01097645〉

Partager

Métriques

Consultations de la notice

218