Modeling an Aircraft Landing System in Event-B

Dominique Méry 1, 2 Neeraj Kumar Singh 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : This paper presents a step wise formal development oft helanding system of an aircraft. The formal models include the complex behaviour, temporal behaviour and sequence of operations of the landing gear system. The models are formalized in Event-B modeling language, and then the ProB model checker is used to verify the deadlock freedom and to validate the behaviour requirements by animating the formalized models. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of the complex critical systems.
Type de document :
Communication dans un congrès
Frédéric Boniol. ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. Springer, 433, pp.154-159, 2014, CCIS
Liste complète des métadonnées

https://hal.inria.fr/hal-00985010
Contributeur : Dominique Méry <>
Soumis le : mardi 29 avril 2014 - 10:23:13
Dernière modification le : mardi 19 février 2019 - 15:40:03

Identifiants

  • HAL Id : hal-00985010, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Modeling an Aircraft Landing System in Event-B. Frédéric Boniol. ABZ 2014 Case Study Track, Jun 2014, Toulouse, France. Springer, 433, pp.154-159, 2014, CCIS. 〈hal-00985010〉

Partager

Métriques

Consultations de la notice

305