ABZ 2014 Landing Gear Case Study in Hybrid Event-B — Conference Version

Technical content last updated 18.12.13.

This page contains the machines etc. for the ABZ 2014 Landing Gear Case Study done in Hybrid Event-B.
This is the version of the case study done for the ABZ 2014 Conference itself.

This has been done as a substantial paper exercise in modelling a system of such complexity.

The case study is broken up into a number of documents because of LaTeX limits on number of unassigned floats in the style used :-)

The work here is subject to improvement and extension, as time allows.

If you spot any bugs, please don't hesitate to contact the author. Thanks.

Nominal Regime

  • First few levels: up to the splitting of the two computing modules.

  • Next few levels: the analogical switch, general electro-valve, and their sensors.

  • Last few levels: the movement electro-valves, their sensors, and the computing module's timing automaton.