NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
A Verification Framework for Runtime Assurance of Autonomous UASRuntime 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 hand control of the overall system to a trusted controller when an untrusted one 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. 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.

In the simplex RTA framework, a system has an advanced controller (AC) and a reversionary controller (RC). The system is allowed to operate with the AC until a runtime monitor detects that some property has been violated and then the RC takes over. Assuming that the sample rate of the monitor will detect improper functioning with enough time for the RC to correct the impending problem, and that the RC is trusted, the system will operate as intended. This use of the simplex RTA framework can allow for the integration of untrusted, but possibly more performant, controllers in a safe way.

This paper presents a formalization of a simplex RTA framework in the Prototype Verification System (PVS) theorem prover using an embedding of differential dynamic logic (DDL) called Plaidypvs. A novel feature of this framework is that it can be instantiated at different levels of abstraction. This feature allows for the formal verification of a system with an untrusted black box component, such as an AI/ML controller.

This paper does not address the many difficulties in deploying RTA in an industrial-level system. Instead, the focus is on the formal verification of the simplex RTA framework in the language of hybrid programs. 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.

A selection of Unmanned Aircraft Systems (UAS) operations are shown as instances of the general RTA framework in PVS. This 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.
Document ID
20240007986
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
J Tanner Slagel
(Langley Research Center Hampton, United States)
Lauren M. White
(Langley Research Center Hampton, United States)
Aaron Dutle
(Langley Research Center Hampton, United States)
Cesar A. Munoz
(Langley Research Center Hampton, United States)
Nicolas Crespo
(LaRC Governor's School)
Date Acquired
June 24, 2024
Subject Category
Mathematical and Computer Sciences (General)
Meeting Information
Meeting: 43rd Digital Avionics Systems Conference
Location: San Diego, CA
Country: US
Start Date: September 29, 2024
End Date: October 3, 2024
Sponsors: American Institute of Aeronautics and Astronautics
Funding Number(s)
WBS: 340428.02.60.07.01
Distribution Limits
Public
Copyright
Portions of document may include copyright protected material.
Technical Review
NASA Peer Committee
Keywords
PVS
Runtime Assurnace
Hybrid Programs
Plaidypvs
No Preview Available