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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Collaborative Situational Awareness for Conflict-Aware Flight Planning


    Contributors:


    Publication date :

    2020-10-11


    Size :

    2011465 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Situational Awareness and Awareness of Auto-flight Modes

    Newman, T. P. / Flight Safety Foundation | British Library Conference Proceedings | 1997


    Situational awareness on the flight deck

    Emerald Group Publishing | 2000


    Verifying Situational Awareness Associated with Flight Symbology

    Gawron, V. J. / Weingarten, N. C. / Hughes, T. et al. | British Library Conference Proceedings | 1999


    Methods for situational awareness during formation flight

    FROLOV SERGEY V / CYRUS MICHAEL / BRUCE ALLAN J et al. | European Patent Office | 2019

    Free access

    Improved Conjunction Analysis via Collaborative Space Situational Awareness

    Kelso, T.S. / Vallado, D. / Chan, J. et al. | British Library Conference Proceedings | 2009