Abstract Aircrafts are the safest means of transport, which requires an excellent management and development. Whereas, Aircraft landing is one of the most complex problems in this domain, Due to the huge increase of aircrafts number in the world. One of the main challenges to develop landing system is specifying it in the first place. In this paper, we focus on modeling aircrafts scheduling in the Traffic Management Advisor, our approach is based on deadline monotonic algorithm that shows a lot of advantages compared to the currently used method -First come First Served-. To ensure a very strong assurance of bug’s absence, we model this system using a formal method -Event-B- prove that it is correct by construction. This modeling is done by mean of refinement, invariants preservation proof and deadlock freedom, whereby the result system, will be correct by construction. However, the number of proofs that ensure system correctness is huge, therefore we use a platform called RODIN to minimize the number of proofs done manually.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Modeling Aircraft Landing Scheduling in Event B


    Contributors:


    Publication date :

    2017-12-02


    Size :

    16 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 an Aircraft Landing System in Event-B

    Méry, Dominique / Singh, Neeraj Kumar | Springer Verlag | 2014


    Mobile Aircraft Landing Stair Scheduling

    Liu, Ming / Liu, Zhongzheng | IEEE | 2019


    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 / LAURELO-FERNANDEZ ANDREA | European Patent Office | 2025

    Free access