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.
More »