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.
A Verification Framework for Runtime Assurance of Autonomous UAS
2024-09-29
463973 byte
Conference paper
Electronic Resource
English
Runtime Assurance for Autonomous Aerospace Systems
AIAA | 2020
|Runtime verification for autonomous spacecraft software
Tema Archive | 2005
|Runtime Verification for Autonomous Spacecraft Software
British Library Conference Proceedings | 2005
|NTRS
|