NASA SBIR 2020-II Solicitation

Proposal Summary

Proposal Information

Proposal Number:
20-2- A2.02-6033
Phase 1 Contract #:
80NSSC20C0497
Subtopic Title:
Unmanned Aircraft Systems (UAS) Technologies
Proposal Title:
A Semantics-Based Verification Toolset for UAS Embedded Software

Small Business Concern

   
Firm:
          
Runtime Verification, Inc.
          
   
Address:
          
102 East Main Street, Suite 500, Urbana, IL 61801
          
   
Phone:
          
(217) 550-1558                                                                                                                                                                                
          

Principal Investigator:

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

Business Official:

   
Name:
          
Patrick MacKay
          
   
E-mail:
          
patrick.mackay@runtimeverification.com
          
   
Address:
          
102 East Main Street, Suite 500, IL 61801 - 2744
          
   
Phone:
          
(217) 550-1558                                                                                                                                                                                
          

Summary Details:

   
Estimated Technology Readiness Level (TRL) :                                                                                                                                                          
Begin: 4
End: 7
          
          
     
Technical Abstract (Limit 2000 characters, approximately 200 words):

Develop bounded model checker for C programs that detects undefined behavior.  Convert prototype developed in Phase I into a robust tool capable of analyzing Airliner, a drone autopilot developed by Windhover under contract from NASA.

The bounded model checker and a C interpreter that detects undefined behavior in unit tests are both generated from the same formal semantics of C.

Both the tools will be integrated into the build system of Airliner, and used to analyze Airliner and applications built from Airliner.

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

Much satellite software is written in C.   For example, NASA's "core Flight Software" is written in C.

Software for unmanned aircraft systems tends to be written in C.   For example, Airliner is a drone autopilot.

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

C is the most widely used programming language for embedded systems, and is used in the automotive industry, in telecommunications, in robotics.   It is used for the infrastructure of the internet.  It is the main language used for Linux.  Our tools can be applied to any software written in C.

          
          
     
Duration:     24
          
          

Form Generated on 05/13/2021 14:44:38