Verification of an Airport Taxiway Path-Finding Algorithm

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.