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 implementations in C of CPR, which became the reference implementations 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, Volume 33, Number 1, pp. 65-86, 2021. BibTeX Reference. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018.
• 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