Compact Position Reporting Algorithm
The Compact Position Reporting (CPR) algorithm is a safety-critical
element of the Automatic Dependent Surveillance - Broadcast (ADS-B)
protocol. This protocol enables aircraft to share their current
states, i.e., position and velocity, with traffic aircraft in their
vicinity. CPR consists of a collection of functions that encode and
decode aircraft position data (latitude and longitude).
The Formal Methods Team at NASA LaRC conducted a
formal analysis of the CPR algorithm. This analysis includes:
- A formal proof that the published requirements for correct decoding are insufficient, even if
computations are assumed to be performed using exact
- A set of tightened requirements that formally proven to guarantee correct
decoding under exact real arithmetic.
- Mathematically equivalent, but computationally simpler forms to several
expressions in the CPR functions in order to reduce imprecise calculation.
- Fixed-point and floating-point implementation in C of CPR, which became the reference implemenation
of CPR in the international standard ED-102B/DO-260C.
The CPR formal development and C implementations are available under NASA's Open Source Agreement at GitHub.
- Aaron Dutle, Mariano Moscato, Laura Titolo, César
Muñoz, Gregory Anderson, and François Bobot,
of the Compact Position Reporting Algorithm,
Formal Aspects of Computing (to appear), 2020. BibTeX Reference.
- Laura Titolo, Mariano Moscato, César
Dutle, and François Bobot, A Formally Verified
Floating-Point Implementation of the Compact Position Reporting
Algorithm, Proceedings of the 22nd
International Symposium on Formal Methods (FM 2018), Lecture
Notes in Computer Science, Vol. 10951, pp. 364-381, 2018. BibTeX Reference.
- Aaron Dutle, Mariano Moscato, Laura Titolo, and César
Muñoz, A Formal Analysis of the Compact Position Reporting Algorithm
, Proceedings of the 9th Working Conference on Verified Software:
Theories, Tools, and Experiments (VSTTE 2017), Lecture Notes in Computer Science,
Vol. 10712, pp. 19-34, 2017. BibTeX Reference.
identifies links that are outside
the NASA domain