Landing Gear System

This use case has been submitted to 4th International ABZ 2014 Conference[BDF2014] and is based on specification[WB2014].

The model

The model is available in this archive. Due to a large number of configurations, a preprocessor (GPP) was used to produce individual cases. The archive contains a Makefile that can be used to produce all cases.

Macros used to configure our cases are:

The model can also be retrieved as individual files:

Generated cases

If you do not want to install GPP, an archive containing generated cases is available here

But you can also retrieve each case, where:


We also provide cases for on the fly model checking of requirement R1.1. Here the pilot will some times wait X seconds before performing another move. We can detect the state of the pilot and check if gears are retracted and doors are closed. This test can be performed on the fly using command:

sift case_N_V3_H2_8500.tts -E -f "Pilot_1_shandle__up__elapsed => (LandingSystem_w1 /\ LandingSystem_w3)"



[BDF2014] Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre, B. Berthomieu, S. Dal Zilio and L. Fronc, 4th International ABZ 2014 Conference.

[WB2014] Landing Gear System, Case study for the ABZ 2014 conference, V. Wiels and F. Boniol