Advertisement

A Formal Analysis of the Compact Position Reporting Algorithm

  • Aaron DutleEmail author
  • Mariano Moscato
  • Laura Titolo
  • César Muñoz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

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.

References

  1. 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
  2. 2.
    Dutle, A.M., Muñoz, C.A., Narkawicz, A.J., Butler, R.W.: Software validation via model animation. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 92–108. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21215-9_6 CrossRefGoogle Scholar
  3. 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. 4.
    ICAO: Manual on the Universal Access Transceiver (UAT). Doc (International Civil Aviation Organization), vol. 9861 (2012)Google Scholar
  5. 5.
    Muñoz, C.: Rapid prototyping in PVS. Contractor Report NASA/CR-2003-212418, NASA, Langley Research Center, Hampton, VA, USA, May 2003Google Scholar
  6. 6.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55602-8_217 Google Scholar
  7. 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

Copyright information

© 2015 US Government Work subject to 17 USC 105. All other rights reserved. 2017

Authors and Affiliations

  • Aaron Dutle
    • 1
    Email author
  • Mariano Moscato
    • 2
  • Laura Titolo
    • 2
  • César Muñoz
    • 1
  1. 1.NASA Langley Research CenterHamptonUSA
  2. 2.National Institute of AerospaceHamptonUSA

Personalised recommendations