Abstract In this paper we present our formalisation 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. To validate the model we complemented proof with animation and model checking. For the latter, we used the ProB animator and model checker. Graphical representation of the model turned out to be crucial in the development and validation of the model; this was achieved using a new version of BMotion Studio integrated into ProB 2.0.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Validation of the ABZ Landing Gear System Using ProB


    Contributors:


    Publication date :

    2014-01-01


    Size :

    14 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Validation of the ABZ Landing Gear System Using ProB

    Hansen, D. / Ladenberger, L. / Wiegard, H. et al. | British Library Conference Proceedings | 2014


    LANDING GEAR DOOR SYSTEM FOR LANDING GEAR COMPARTMENT

    SEAN C WEBB | European Patent Office | 2022

    Free access

    LANDING GEAR DOOR SYSTEM FOR A LANDING GEAR COMPARTMENT

    WEBB SEAN C | European Patent Office | 2024

    Free access

    Landing gear bay door system for landing gear bay

    WEBB STEPHEN C | European Patent Office | 2022

    Free access

    LANDING GEAR DOOR SYSTEM FOR A LANDING GEAR COMPARTMENT

    WEBB SEAN C | European Patent Office | 2022

    Free access