The presence of round-off errors in floating-point programs may provoke a significant divergence between the actual result of the computation and the one ideally obtained using exact real-number arithmetic. These rounding errors are particularly problematic in the context of safety-critical systems such as aerospace applications. In fact, in this context, even a small rounding error can lead to catastrophic consequences when not appropriately accounted for. This paper shows how different formal methods tools can be combined to perform rigorous round-off error analysis of avionics software and outlines the challenges and the open problems in this field. Three case studies taken from real-world avionics applications are presented: the ADS-B Compact Position Reporting Algorithm, the winding number point-in-polygon algorithm used for geofencing of unmanned vehicles, and a function from the NASA DAIDALUS suite of detect-and-avoid solutions developed by NASA.
Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software
Intel.Syst.Ref.Library
2023-07-22
24 pages
Article/Chapter (Book)
Electronic Resource
English
Reusing Safety-Critical Avionics Software
SAE Technical Papers | 2012
|Reusing Safety-Critical Avionics Software
British Library Conference Proceedings | 2012
|Reusing certified, safety-critical avionics software
IEEE | 2012
|