NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • 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:

    Publications

    Formal Development

    The formal development requires PVS 6.0[*] and the current version of the NASA PVS Library[*].

    The tag [*] identifies links that are outside the NASA domain