NASA SBIR 2017 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 171 A2.02-9024
SUBTOPIC TITLE: Unmanned Aircraft Systems Technology
PROPOSAL TITLE: Argument-Driven Application of Formal Methods

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Dependable Computing LLC
2120 North Pantops Drive
Charlottesville, VA 22911 - 8648
(434) 293-8358

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Dr. Ashlie Benjamin Hocking
ben.hocking@dependablecomputing.com
2120 North Pantops Drive
Charlottesville, VA 22911 - 8648
(434) 981-4975

CORPORATE/BUSINESS OFFICIAL (Name, E-mail, Mail Address, City/State/Zip, Phone)
Ms. Virginia Knight 2938358
office@dependablecomputing.com
2120 North Pantops Drive
Charlottesville, VA 22911 - 8648
(434) 293-8358

Estimated Technology Readiness Level (TRL) at beginning and end of contract:
Begin: 1
End: 3

Technology Available (TAV) Subtopics
Unmanned Aircraft Systems Technology is a Technology Available (TAV) subtopic that includes NASA Intellectual Property (IP). Do you plan to use the NASA IP under the award?
No

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
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.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
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.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
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.

TECHNOLOGY TAXONOMY MAPPING (NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.)
Analytical Methods
Data Fusion
Project Management
Quality/Reliability
Software Tools (Analysis, Design)
Verification/Validation Tools

Form Generated on 04-19-17 12:59