Runtime Assurance (RTA) is a design-time architecture for safety-critical systems where an internal monitor acts upon detecting a violation of a property. The simplex architecture is an instance of RTA, where the action taken is to give control of the overall system to a trusted controller when an untrusted controller violates a safety property. Simplex RTA is emerging as a method for allowing AI/ML and other unverified software to be integrated into safety-critical applications like aircraft operations. To this end, the American Society for Testing and Materials (ASTM) and NASA have each published guidelines on the use of RTA in such systems. A formal verification of the simplex RTA framework in the language of hybrid programs is extended in this work. Hybrid programs are programs that include both discrete and continuous dynamics and can be used to model complex cyber-physical systems. Plaidypvs is a tool that enables formalization of hybrid programs in the PVS theorem prover. Plaidypvs enables the verification of the general simplex RTA framework and then, by specializing some components of the hybrid program, verifying instances of the framework while treating the untrusted component as a black box. This paper presents the application of this formalization to a selection of Unmanned Aircraft Systems (UAS) operations. The formal verification process offers the benefit of design time verification of relevant safety properties to the system, and it also gives requirements on the sample rate of sensors that determine the time interval in which the ‘switch’ property of the RTA framework is checked.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    A Verification Framework for Runtime Assurance of Autonomous UAS


    Contributors:


    Publication date :

    2024-09-29


    Size :

    463973 byte





    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Runtime Assurance for Autonomous Aerospace Systems

    Schierman, John D. / DeVore, Michael D. / Richards, Nathan D. et al. | AIAA | 2020


    Runtime Assurance for Autonomous Driving with Neural Reachability

    Bogomolov, Sergiy / Hekal, Abdelrahman / Hoxha, Bardh et al. | IEEE | 2022


    Runtime verification for autonomous spacecraft software

    Goldberg, A. / Havelund, K. / McGann, C. | Tema Archive | 2005


    Runtime Verification for Autonomous Spacecraft Software

    Goldberg, A. / Havelund, K. / McGann, C. et al. | British Library Conference Proceedings | 2005


    Runtime Verification

    Alwyn E Goodloe | NTRS