In autonomous air-traffic management scenarios of the future, manned and unmanned aircraft will be able to safely navigate through the National Airspace System, independent of centralized air-traffic controllers. They will do this by sharing critical data necessary for maintaining standard separation with each other. Under such conditions, every aircraft must have sufficient knowledge about other aircraft sharing the airspace to operate safely. In this paper, we specify a safe state of knowledge that is necessary for aircraft to operate safely in the absence of a centralized air-traffic controller and present a distributed knowledge propagation protocol to attain this safe state. This protocol can be used by network-connected aircraft to achieve collaborative situational awareness for cooperative flight planning. We identify certain system conditions necessary to guarantee two correctness properties for our protocol – safety and progress. We use the TLA+ Specification Language to formally specify our protocol, the correctness properties, and the conditions necessary to guarantee the properties. Using the formal specifications, we also provide mechanically-verified proofs of the correctness properties in the TLA+ Proof System.
Collaborative Situational Awareness for Conflict-Aware Flight Planning
2020-10-11
2011465 byte
Conference paper
Electronic Resource
English
Situational Awareness and Awareness of Auto-flight Modes
British Library Conference Proceedings | 1997
|Situational awareness on the flight deck
Emerald Group Publishing | 2000
Verifying Situational Awareness Associated with Flight Symbology
British Library Conference Proceedings | 1999
|METHODS FOR SITUATIONAL AWARENESS DURING FORMATION FLIGHT
European Patent Office | 2017
|