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.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    A Verification Framework for Runtime Assurance of Autonomous UAS


    Beteiligte:
    Slagel, J Tanner (Autor:in) / White, Lauren M. (Autor:in) / Dutle, Aaron (Autor:in) / Munoz, Cesar A. (Autor:in) / Crespo, Nicolas (Autor:in)


    Erscheinungsdatum :

    29.09.2024


    Format / Umfang :

    463973 byte





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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 Archiv | 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