At controlled airports, aircraft taxi on the ground following precise instructions from Air Traffic Control. Those instructions can get quite intricate and complicated and lead to errors from Air Traffic Control or confusion from pilots, especially at larger airports. In order to reduce the pilots' workload and lower the risk of accidents from pilot error or Air Traffic Control mistakes, it is desirable to automate taxiing of aircraft. One aspect of automated taxiing is to automatically find the correct taxiway path from Air Traffic Control instructions. In this paper, we implement and formally verify a taxiway path-finding algorithm in the Coq proof assistant, and test it on three different airports of various sizes (Ann Arbor, Willow Run and Detroit Wayne). We first build an undirected airport taxiway graph topology, extend it to a directed expanded graph, disallowing some unrealistic paths such as U-turns, and formally encode the two graphs into Coq types. We then implement the path-finding algorithm on the directed expanded graph, and map downward the result back to the undirected graph. We formally verify the correctness of our algorithm in the Coq theorem prover.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Verification of an Airport Taxiway Path-Finding Algorithm


    Contributors:


    Publication date :

    2020-10-11


    Size :

    955455 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Lighting airport taxiway sign

    Engineering Index Backfile | 1954


    Scheduling and Airport Taxiway Path Planning Under Uncertainty

    J. Li / H. Zhang / M. Gong et al. | NTIS | 2019


    Scheduling and Airport Taxiway Path Planning Under Uncertainty

    Li, Jiaoyang / Zhang, Han / Gong, Mimi et al. | NTRS | 2019


    Omni-directional airport taxiway light

    SCHÖNERT OLIVER | European Patent Office | 2018

    Free access

    OMNI-DIRECTIONAL AIRPORT-TAXIWAY LIGHT

    SCHÖNERT OLIVER | European Patent Office | 2017

    Free access