zbMATH — the first resource for mathematics

Formal analysis of the compact position reporting algorithm. (English) Zbl 1458.68273
Summary: 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.
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
65Y04 Numerical algorithms for computer arithmetic, etc.
68P30 Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science)
68Q60 Specification and verification (program logics, model checking, etc.)
68W40 Analysis of algorithms
Full Text: DOI
[1] Barrett C, Tinelli C (2007) CVC3. In: Proceedings of the 19th international conference on computer aided verification, CAV 2007, pp 298-302
[2] Bouissou O, Conquet E, Cousot P, Cousot R, Feret J, Goubault E, Ghorbal K, Lesens D, Mauborgne L, Miné A, Putot S, Rival X, Turin M (2009) Space software validation using abstract interpretation. In: Proceedings of the international space system engineering conference, data systems in aerospace (DASIA 2009). ESA Publications, pp 1-7
[3] Bertrane, J.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Rival, X., Static analysis and verification of aerospace software by abstract interpretation, Found Trends Program Lang., 2, 2-3, 71-190 (2015)
[4] Boldo, S.; Clément, F.; Filliâtre, JC; Mayero, M.; Melquiond, G.; Weis, P., Wave equation numerical resolution: a comprehensive mechanized proof of a C program, J. Autom Reason, 50, 4, 423-456 (2013) · Zbl 1267.68208
[5] Baudin P, Cuoq P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V (2016) ACSL: ANSI/ISO C Specification Language, version 1.12
[6] Bobot, F.; Filliâtre, JC; Marché, C.; Paskevich, A., Let’s verify this with Why3, Int J Softw Tools Technol Transf, 17, 6, 709-727 (2015)
[7] Boldo, S.; Marché, C., Formal verification of numerical programs: from C annotated programs to mechanical proofs, Math Comput Sci, 5, 4, 377-393 (2011) · Zbl 1264.68054
[8] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977. ACM, pp 238-252
[9] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival (2005) The ASTREÉ analyzer. In: Proceedings of the 14th European Symposium on Programming (ESOP 2005), vol 3444 of lecture notes in computer science. Springer, Berlin, pp 21-30 · Zbl 1108.68422
[10] Conchon, S.; Contejean, E.; Kanig, J.; Lescuyer, S., CC(X): semantic combination of congruence closure with solvable theories, Electron Notes Theor Comput Sci, 198, 2, 51-69 (2008) · Zbl 1277.68240
[11] Chen L, Miné A, Cousot P (2008) A sound floating-point polyhedra abstract domain. In: Proceedings of the 6th Asian symposium on programming languages and systems, APLAS 2008, vol 5356 of lecture notes in computer science. Springer, Berlin, pp 3-18
[12] Code of Federal Regulations (2015) Automatic dependent surveillance-broadcast (ADS-B) out, 91 c.f.r., section 225
[13] de Dinechin, F.; Lauter, C.; Melquiond, G., Certifying the floating-point implementation of an elementary function using Gappa, IEEE Trans Comput, 60, 2, 242-253 (2011) · Zbl 1367.65250
[14] de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, vol 4963 of lecture notes in computer science. Springer, Berlin, pp 337-340
[15] Dutle A, Moscato M, Titolo L, Muñoz C (2017) A formal analysis of the compact position reporting algorithm. In: 9th Working conference on verified software: theories, tools, and experiments, VSTTE 2017, revised selected papers, vol 10712, pp 19-34 · Zbl 1403.68324
[16] Delmas D, Souyris J (2007) Astrée: from research to industry. In: Proceedings of the 14th international symposium on static analysis, SAS, pp 437-451
[17] European Commission (2017) Commission implementing regulation (EU) 2017/386 of 6 march 2017 amending implementing regulation (EU) No 1207/2011, C/2017/1426, 2017
[18] Goodloe A, Muñoz C, Kirchner F, Correnson L (2013) Verification of numerical programs: from real numbers to floating point numbers. In: Proceedings of NFM 2013, vol. 7871 of lecture notes in computer science. Springer, Berlin, pp 441-446
[19] Goubault E, Putot S (2006) Static analysis of numerical algorithms. In: Proceedings of SAS 2006, vol 4134 of lecture notes in computer science. Springer, Berlin, pp 18-34 · Zbl 1225.68073
[20] Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B., Frama-C: a software analysis perspective, Formal Aspects Comput, 27, 3, 573-609 (2015)
[21] Marché, C., Verification of the functional behavior of a floating-point program: an industrial case study, Sci Comput Program, 96, 279-296 (2014)
[22] Miné A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Proceedings of the 13th European symposium on programming languages and systems, ESOP 2004, vol 2986 of lecture notes in computer science. Springer, Berlin, pp 3-17 · Zbl 1126.68353
[23] Marché C, Moy Y (2017) The Jessie Plugin for deductive verification in Frama-C
[24] Moscato MM, Titolo L, Dutle A, Muñoz C (2017) Automatic estimation of verified floating-point round-off errors via static analysis. In: Proceedings of the 36th international conference on computer safety, reliablilty, and security, SAFECOMP 2017 · Zbl 1403.68324
[25] Moscato MM, Titolo L, Feliú MA, Muñoz CA (2019) Provably correct floating-point implementation of a point-in-polygon algorithm. In: Proceedings of the third World congress on formal methods-the next 30 years (FM 2019), vol 11800 of lecture notes in computer science. Springer, Berlin, pp 21-37
[26] Owre S, Rushby J, Shankar N (1992) PVS: a prototype verification system. In: Proceedings of CADE 1992, vol 607 of lecture notes in artificial intelligence. Springer, Berlin, pp 748-752
[27] RTCA SC-186 (2009) Minimum operational performance standards for 1090 MHz extended squitter automatic dependent surveillance-broadcast (ADS-B) and traffic information services-broadcast (TIS-B)
[28] Titolo L, Feliú M, Moscato M, Muñoz C (2018) An abstract interpretation framework for the round-off error analysis of floating-point programs. In: Proceedings of the 19th international conference on verification, model checking, and abstract interpretation, VMCAI 2018, vol 10747. Springer, Berlin, pp 516-537 · Zbl 1446.68036
[29] Titolo L, Moscato MM, Muñoz CA, Dutle A, Bobot F (2018) A formally verified floating-point implementation of the compact position reporting algorithm. In: Proceedings of the 22nd international symposium on formal methods (FM 2018), vol 10951 of lecture notes in computer science. Springer, Berlin, pp 364-381
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.