Modelling an Aircraft Landing System in Event-B (Full Report)

TL;DR

This paper presents a formal, stepwise development of an aircraft landing system using Event-B, demonstrating how formal methods can ensure correctness in complex safety-critical systems.

Contribution

It provides a detailed formal model of an aircraft landing system in Event-B, including complex and temporal behaviors, serving as a benchmark for verification techniques.

Findings

Formal models capture complex landing gear behaviors

Refinement supports incremental development

Benchmark for verification of behavioral properties

Abstract

The failure of hardware or software in a critical system can lead to loss of lives. The design errors can be main source of the failures that can be introduced during system development process. Formal techniques are an alternative approach to verify the correctness of critical systems, overcoming limitations of the traditional validation techniques such as simulation and testing. The increasing complexity and failure rate brings new challenges in the area of verification and validation of avionic systems. Since the reliability of the software cannot be quantified, the \textit{correct by construction} approach can implement a reliable system. Refinement plays a major role to build a large system incrementally from an abstract specification to a concrete system. This paper contributes as a stepwise formal development of the landing 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 modelling language, which supports stepwise refinement. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of systems. The report is the full version of a paper published for the ABZ 2014 Case Study. is