## 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