NASA SBIR 2020-I Solicitation

Proposal Summary


PROPOSAL NUMBER:
 20-1- A2.02-6033
SUBTOPIC TITLE:
 Unmanned Aircraft Systems (UAS) Technologies
PROPOSAL TITLE:
 A Semantics-Based Verification Toolset for UAS Embedded Software
SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Runtime Verification, Inc.
102 East Main Street, Suite 500
Urbana, IL 61801
(217) 550-1558

Principal Investigator (Name, E-mail, Mail Address, City/State/Zip, Phone)

Name:
Ralph Johnson
E-mail:
ralph.johnson@runtimeverification.com
Address:
102 East Main Street, Suite 500 Urbana, IL 61801 - 2744
Phone:
(217) 621-3038

Business Official (Name, E-mail, Mail Address, City/State/Zip, Phone)

Name:
Mr. Patrick MacKay
E-mail:
patrick.mackay@runtimeverification.com
Address:
102 East Main Street, Suite 500 Urbana, IL 61801 - 2744
Phone:
(217) 550-1558
Estimated Technology Readiness Level (TRL) :
Begin: 3
End: 4
Technical Abstract (Limit 2000 characters, approximately 200 words)

We propose a new verification method for software intended to be flown on unmanned aircraft systems that is both automatic and inexpensive. In Phase 1 we will focus on a class of errors in C programs called “undefined behavior” (UB) because this makes the method both easy to use and easy to compare with existing static analysis tools.  But in subsequent phases we plan to extend it to arbitrary program specifications, including those using temporal logic. This verification method has been used for non-real-time software, we will extend it to real-time embedded systems.  We propose (1) to extend RV-Match, our semantics-based C dynamic analysis tool, to target one of the real-time operating systems that NASA uses for running UAS embedded software;  (2) to produce a symbolic bounded model checker for C based on the most complete operational semantics of the language (exactly the same semantics as used by our dynamic analysis tool); and (3) to evaluate our dynamic analysis tool and model checker by using them to analyze real NASA flight software, such as the NASA core Flight System (cFS).

Potential NASA Applications (Limit 1500 characters, approximately 150 words)

The analysis of NASA flight software produced as a result of this project should be directly useful to developers of that software.  The analysis tools produced should be useful for verifying and debugging any NASA software developed in C. 

Potential Non-NASA Applications (Limit 1500 characters, approximately 150 words)

Boeing, which develops a lot of embedded systems software, has demonstrated interest in our technology.   Embedded systems in the automotive industry are another likely application for our tools.   More generally, the verification of debugging of any safety- or mission-critical software in C would benefit from development of the technology in our proposal.

Duration: 6

Form Generated on 06/29/2020 21:07:57