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 real arithmetic.
• 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.

Publications

• Aaron Dutle, Mariano Moscato, Laura Titolo, César Muñoz, Gregory Anderson, and François Bobot, Formal Analysis of the Compact Position Reporting Algorithm, Formal Aspects of Computing (to appear), 2020. BibTeX Reference.
• Laura Titolo, Mariano Moscato, César Muñoz, Aaron 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.

The tag identifies links that are outside the NASA domain