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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software


    Additional title:

    Intel.Syst.Ref.Library


    Contributors:


    Publication date :

    2023-07-22


    Size :

    24 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English