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.