In air traffic management, conflict detection algorithms are used to determine whether or not aircraft are predicted to lose horizontal and vertical separation minima within a time interval assuming a trajectory model. In the case of linear trajectories, conflict detection algorithms have been proposed that are both sound, i.e., they detect all conflicts, and complete, i.e., they do not present false alarms. In general, for arbitrary nonlinear trajectory models, it is possible to define detection algorithms that are either sound or complete, but not both. This paper considers the case of nonlinear aircraft trajectory models based on polynomial functions. In particular, it proposes a conflict detection algorithm that precisely determines whether, given a lookahead time, two aircraft flying polynomial trajectories are in conflict. That is, it has been formally verified that, assuming that the aircraft trajectories are modeled as polynomial functions, the proposed algorithm is both sound and complete.
A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories
AIAA Aerospace Sciences Meeting (AIAA SciTech 2015) ; 2015 ; Kissimmee , FL, United States
2015-01-05
Conference paper
No indication
English
A Formally Verified Conflict Detection Algorithm for Polynomial Trajectories (AIAA 2015-0795)
British Library Conference Proceedings | 2015
|Software safety architecture that can be formally verified
Automotive engineering | 2004
|