A formally verified floating-point implementation of the Compact Position Reporting algorithm
Mariano M. Moscato
The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate their current state, including position and velocity information, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B module responsible for the encoding and decoding of aircraft positions. CPR is highly sensitive to computer arithmetic since it heavily relies on functions that are intrinsically unstable such floor and modulo.
This talk reports on how Frama-C was used to verify that a double-precision implementation of CPR is correct with respect to its operational requirement. In this effort, Frama-C is used synergically with different kinds of provers such as Gappa, Alt-Ergo, and PVS. The verified algorithm is currently being considered for inclusion in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.
About Mariano M. Moscato
Mariano Moscato got his Ph.D. in Computer Science from the University of Buenos Aires (Argentina) in 2014 and since then is working in the National Institute of Aerospace as part of the NASA Langley Formal Methods Group. He has been involved in diverse endeavors related to the development and application of formal techniques to the validation and verification of safety-critical systems. Among other topics, his is currently working in the development of tools aimed at the formally-certified analysis of floating-point programs.