Argument-Driven Application of Formal Methods

This proposal, in response to SBIR topic A2.02, develops low-cost, high-assurance UAS autonomy through argument-driven application of formal methods to runtime assurance. Autonomous UAS operations promise lower cost hardware and a reduction in labor force compared to conventionally piloted aircraft. While loss of a UAS may not be catastrophic, the possibility of catastrophic collateral damage exists. UAS software is therefore safety critical, and safety-critical software remains expensive to build and certify. The full economic benefit of autonomous UAS operations cannot be realized until the cost of autonomous UAS software can be reduced without negatively impacting safety. Software architectures providing software fault tolerance through reconfiguration to a trusted backup, such as runtime assurance, offer fixed-cost assurance for autonomous software. They obviate traditional V&V by shifting the assurance burden from the autonomous software to the architecture. Traditional V&V approaches focus on rigorous testing, but providing the level of assurance required to enable UAS autonomy through testing remains infeasible. Formal methods offer an alternative, but comprehensive application of formal methods remains too costly. Application must be targeted at elements of the architecture for which assurance is most critical. Determining where formal methods should be targeted is a challenge. Rigorous safety arguments link safety claims to evidence gathered and not only provide justifiable assurance of safety, but also enable developers and certifiers to identify the most critical elements of the system. Rigorous safety arguments can identify where formal methods should be applied. Argument-driven application of formal methods to runtime assurance therefore provides high assurance of safety while reducing development cost. This circumvents traditional V&V of autonomous UAS software without sacrificing system safety, enabling low-cost high-assurance UAS autonomy.

Argument-driven application of formal methods is applicable to all NASA safety-critical systems. Safeguard represents a current NASA project that provides runtime assurance. Currently, Safeguard is being developed following NASA software safety practices and will be undergoing a rigorous test and evaluation phase as it seeks to transition to a commercial system. Safeguard will benefit significantly from the argument-driven application of formal methods that will be developed under this effort: the application of the technology will result in a safety argument for Safeguard and an alternative set of high-assurance artifacts developed using formal methods. UAS and increasing autonomy for UAS are significant focus areas for NASA. The application of an argument-driven application of formal methods to runtime assurance represents a particularly appealing approach to addressing the risks posed by autonomy as well as enabling low-cost UAS operations. In addition to increasing confidence in autonomous UAS in a reduced-cost manner, this approach provides an argument that can be leveraged to demonstrate compliance with appropriate regulations. Argument-driven application of formal methods to runtime assurance can also be applied to autonomous spacecraft, whether operating in Earth orbit, on Mars, or in the Kuiper belt. This approach can provide the requisite very high levels of assurance that such missions require at reduced costs.

UAS and UAS autonomy represent areas of significant interest for other government agencies, in particular the DoD. AFRL, for example, is beginning a major development project named Loyal Wingman, in which an autonomous UAS will operate with a manned aircraft to conduct military operations. Runtime assurance backed by argument-driven application of formal methods would enable a high degree of autonomy for the UAS while ensuring that critical safety properties ? such as minimum distance to the manned aircraft ? cannot be violated during operations. AFRL is specifically interested in runtime assurance and has sponsored its development and application over the past 15 years. Argument-driven application of formal methods to runtime assurance provides high assurance and reduced cost for commercial UAS. The rigorous argument combined with formal method evidence will help commercial users with certification, providing a path to demonstrating conformance to standards. Customers for this technology include companies that want to use autonomous UAS for delivery, and companies that use autonomous UAS for surveillance. While autonomous cars are tested in a wide range of environments, runtime assurance can be used to handle unexpected situations. As standards are developed for autonomous cars, rigorous arguments can be used to demonstrate conformance to these standards. Potential customers for this technology include all companies developing autonomous automobiles.

This is early/mid-stage (TRL 3) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.