Abstract We describe our experience with modeling the landing gear system of an aircraft using the formal specification language Fiacre. Our model takes into account the behavior and timing properties of both the physical parts and the control software of this system. We use this formal model to check safety and real-time properties on the system but also to find a safe bound on the maximal time needed for all gears to be down and locked (assuming the absence of failures). Our approach ultimately relies on the model-checking tool Tina, that provides state-space generation and model-checking algorithms for an extension of Time Petri Nets with data and priorities.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre


    Contributors:


    Publication date :

    2014-01-01


    Size :

    16 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre

    Berthomieu, B. / Zilio, S.D. / Fronc, L. | British Library Conference Proceedings | 2014



    LANDING GEAR OF AIRCRAFT AND AIRCRAFT COMPRISING LANDING GEAR

    SAKAMOTO FUMINOBU / KUROSE TOYOTOSHI | European Patent Office | 2018

    Free access

    A Physically Representative Aircraft Landing Gear Model for Real-Time Simulation

    York, B. / Alaverdi, O. / American Institute of Aeronautics and Astronautics | British Library Conference Proceedings | 1996


    Aircraft landing gear system

    PETER SHARPE | European Patent Office | 2021

    Free access