Modelling an Aircraft Landing System in Event-B (Full Report)
This work addresses the reliability of aircraft landing systems to prevent failures that could lead to loss of lives, but it is incremental as it applies an existing formal method to a specific case study.
The paper tackled the problem of verifying the correctness of critical avionic systems by developing a formal model of an aircraft landing system using Event-B, resulting in a stepwise refinement from abstract specification to concrete implementation that includes complex and temporal behaviors. It serves as a benchmark for verification techniques and tools.
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