A Formal Analysis of the 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). Incorrect position decoding from CPR has been reported to the American and European organizations responsible for the ADS-B standard. This paper presents a formal analysis of the CPR algorithm in the Prototype Verification System (PVS). This formal analysis shows that the published requirements for correct decoding are insufficient, even if computations are assumed to be performed using exact real arithmetic. As a result of this analysis tightened requirements are proposed. These requirements, which are being considered by the standards organizations, are formally proven to guarantee correct decoding under exact real arithmetic. In addition, this paper proposes mathematically equivalent, but computationally simpler forms to several expressions in the CPR functions in order to reduce imprecise calculation.
- 1.Crow, J., Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: Evaluating, testing, and animating PVS specifications. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, March 2001. http://www.csl.sri.com/users/rushby/abstracts/attachments
- 3.Code of Federal Regulations: Automatic Dependent Surveillance-Broadcast (ADS-B) out equipment and use, 91 C.F.R., Sect. 225 (2015)Google Scholar
- 4.ICAO: Manual on the Universal Access Transceiver (UAT). Doc (International Civil Aviation Organization), vol. 9861 (2012)Google Scholar
- 5.Muñoz, C.: Rapid prototyping in PVS. Contractor Report NASA/CR-2003-212418, NASA, Langley Research Center, Hampton, VA, USA, May 2003Google Scholar
- 7.RTCA SC-186: RTCA-DO-260B, minimum operational performance standards for 1090 MHz extended squitter Automatic Dependent Surveillance - Broadcast (ADS-B) and Traffic Information Services - Broadcast (TIS-B), December 2009Google Scholar