Abstract This paper presents a stepwise formal development of the landing system of an aircraft. The formal models include the complex behaviour, temporal behaviour and sequence of operations of the landing gear system. The models are formalized in Event-B modeling language, and then the ProB model checker is used to verify the deadlock freedom and to validate the behaviour requirements by animating the formalized models. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of the complex critical systems.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Modeling an Aircraft Landing System in Event-B


    Contributors:


    Publication date :

    2014-01-01


    Size :

    6 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Modeling an Aircraft Landing System in Event-B

    Mery, D. / Singh, N.K. | British Library Conference Proceedings | 2014


    Modeling Aircraft Landing Scheduling in Event B

    Jarrar, Abdessamad / Balouki, Youssef / Gadi, Taoufiq et al. | Springer Verlag | 2017


    Aircraft landing event system and method

    GEORGE HOWELL / ANDREW HEBBORN / JAMES BULLEN et al. | European Patent Office | 2022

    Free access

    AIRCRAFT LANDING EVENT SYSTEM AND METHOD

    HOWELL GEORGE / HEBBORN ANDREW / BULLEN JAMES et al. | European Patent Office | 2022

    Free access

    Aircraft landing event system and method

    European Patent Office | 2021

    Free access