The landing gear case study: challenges and experiments

Abstract Embedded critical systems need to be validated very thoroughly; it usually results in very long and onerous test phases. Formal techniques, in particular formal specification languages and associated proof tools, could be an advantageous alternative, or at least a good complement and allow a significant reduction of test phases.

Modeling a landing gear system in Event-B

Abstract This article describes the Event-B modeling of a landing gear system of an aircraft whose complete description can be found in Boniol and Wiels (The Landing Gear System Case Study, ABZ Case Study, Communications in Computer Information Science, vol 433, Springer, Berlin, 2014).

Validation of the ABZ landing gear system using ProB

Abstract In this article, we present our formalization of the ABZ landing gear case study in Event-B. The development was carried out using the Rodin platform and mainly used superposition refinement to structure the specification.

ABZ 2014 (Toulouse, France)

4th International Conference on ASM, Alloy, B, TLA, VDM, and Z

The Landing Gear System Case Study

Abstract This document presents the landing system of an aircraft. It describes the system and provides some of its requirements. We propose this case study as a benchmark for techniques and tools dedicated to the verification of behavioral properties of systems.

Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System

Abstract This paper describes the modeling, done using the Event-B notation, of the aircraft landing gear case study that is proposed in a special track of the ABZ’2014 Conference. In the course of our development, we discovered some problems in our initial modeling approach.

Co-simulation Environment for Rodin: Landing Gear Case Study

Abstract This work in progress presents a prototype multi-simulation environment for the Rodin platform that enables import, co-modelling and co-simulation of dynamic models and formal Event-B specifications, which can help in the design of mixed discrete-event/continuous-time systems.

Context-Aware Verification of a Landing Gear System

Abstract Despite the high level of automation, the practicability of formal verification through model-checking of large models is hindered by the combinatorial explosion problem. In this paper we apply a novel context-aware verification technique to the Landing Gear System Case Study (LGS).

Landing Gear System: An ASM-based Solution for the ABZ Case Study

Abstract We present an ASM model for the case study given as a challenge for the ABZ'14 conference, which specifies the digital part of a landing gear system for aircraft. We strove to make the formal model well understandable for humans.

Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre

Abstract We describe our experience with modeling the landing gear system of an aircraft using the formal specification language Fiacre. Our model takes into account the behavior and timing properties of both the physical parts and the control software of this system.