Airborne Coordinated Conflict Resolution and Detection (ACCoRD)
ACCoRD is a framework for the formal specification and verification
of state-based conflict detection and resolution algorithms. ACCoRD
originates from KB3D, a state-based conflict detection
and resolution algorithm. ACCoRD provides:
- A 3-D conflict detection algorithm, called CD3D, that is correct and complete.
- A 3-D conflict resolution algorithm, called CR3D, that is independent
and coordinated for track only, ground speed only, vertical
only, and combined track and ground speed resolution maneuvers.
- A loss of separation recovery algorithm that is correct.
- A 3-D prevention bands algorithm that computes all the critical vectors.
- Definition of provably correct safety buffers for CD&R algorithms (assuming that track and ground speed errors are unknown but bounded).
- Least but not last, formal specifications and proofs in
The ACCoRD framework is part of our research
on Formal Analysis of
Conflict Detection and Resolution Algorithms.
Software prototypes in
Java and C++ are available upon request.
Note that these prototypes are not suitable for use in a real system
and they should not be used as such.
identifies links that are outside
the NASA domain