Engineering Papers⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20240006522

A Formal Verification Framework for Runtime Assurance

J. Tanner Slagel·Lauren M. White·Aaron Dutle·Cesar A. Munoz·Nicolas Crespo
View original source ↗Export metadata ↓

Abstract

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Explore related subjects

Runtime assuranceHybrid programsTheorem Proving

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

J. Tanner Slagel, Lauren M. White, Aaron Dutle, Cesar A. Munoz, Nicolas Crespo. A Formal Verification Framework for Runtime Assurance. https://ntrs.nasa.gov/citations/20240006522

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2023

Runtime Assurance of Aeronautical Products: Preliminary Recommendations

Runtime assurance (RTA) affords an operational layer of protection against safety hazards to aeronautical products that may include less trusted or untrusted functions. However, any RTA scheme must itself be trusted before it can be deployed into use: i.e., it must be fit for its intended purpose, and it must not itself introduce safety hazards. This report contains preliminary recommendations on the application and integration of RTA into aeronautical products intended for use in civil aviation. The main purpose of these recommendations is to inform regulatory guidance and consensus standards that may be used to meet the safety intent of the applicable regulations.

Runtime assurance↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗