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 is conducting
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.
- 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.
The formal development requires PVS 6.0 and the current version
of the NASA PVS Library.
identifies links that are outside
the NASA domain