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

4th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'14)


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. We note inconsistencies, ambiguities and gaps in the case study and summarise our experiences during modelling and the proof of safety properties.



% BibTex
  author    = {Boniol, Fr\'ed\'eric and Wiels, Virginie},
  title     = {{T}he {L}anding {G}ear {S}ystem {C}ase {S}tudy},
  booktitle = {ABZ Case Study},
  year      = {2014},
  publisher = {Springer},
  series    = {Communications in Computer Information Science},
  volume    = {433},

  title = {Landing gear system},
  author = {Frederic Boniol and Virginie Wiels},
  year = {2013},
 howpublished = {Challenge for the {ABZ}'14 conference, \url{}, accessed 2013-12-19}

  title = {Abstract State Machines - A Method for High-Level System Design and
  publisher = {Springer Verlag},
  year = {2003},
  author = {Egon B\"orger and Robert St\"ark}

  title = {Landing Gear System: An {ASM}-based Solution for the {ABZ'14} Case Study. {Technical Report SCCH-TR-1401} with the complete model and proofs},
  author = {Felix Kossak},
  year = {2014},
  howpublished = {\url{}}

  author = {Felix Kossak and Atif Mashkoor and Verena Geist and Christa Illibauer},
  title = {Improving the Understandability of Formal Specifications: An Experience Report},
  booktitle = {Proc. of the 20th Conf. on Requirements Engineering: Foundation for Software Quality (REFSQ'14; to appear)},
  year = {2014}


  • Presentation: PPT

  • Used formal method: ASM

  • Resources and tools: Paper & Pencil

    For more information, please contact the authors