Back to Search
Start Over
Formal analysis of the compact positionreporting algorithm
- Source :
- Formal Aspects of Computing. 33:65-86
- Publication Year :
- 2021
- Publisher :
- Association for Computing Machinery (ACM), 2021.
-
Abstract
- The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate current state information, including position and velocity messages, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B protocol responsible for the encoding and decoding of aircraft positions. CPR is sensitive to computer arithmetic since it relies on functions that are intrinsically unstable such as floor and modulus. In this paper, a formal verification of the CPR algorithm is presented. In contrast to previous work, the algorithm presented here encompasses the entire range of message types supported by ADS-B. The paper also presents two implementations of the CPR algorithm, one in double-precision floating-point and one in 32-bit unsigned integers, which are both formally verified against the real-number algorithm. The verification proceeds in three steps. For each implementation, a version of CPR, which is simplified and manipulated to reduce numerical instability and leverage features of the datatypes, is proposed. Then, the Prototype Verification System (PVS) is used to formally prove real conformance properties, which assert that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify software conformance properties, which say that the software implementation of the improved algorithm is correct with respect to its idealized real-number counterpart. In concert, the two properties guarantee that the implementation meets the original specification. The two implementations will be included in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.
- Subjects :
- business.industry
Computer science
0102 computer and information sciences
01 natural sciences
Theoretical Computer Science
Software
010201 computation theory & mathematics
Theory of computation
Prototype Verification System
Leverage (statistics)
Reference implementation
business
Algorithm
Implementation
Formal verification
Decoding methods
Subjects
Details
- ISSN :
- 1433299X and 09345043
- Volume :
- 33
- Database :
- OpenAIRE
- Journal :
- Formal Aspects of Computing
- Accession number :
- edsair.doi...........2e3e0ca0e88b9eeb85c33c1332f476f5