Firm:

          

Runtime Verification, Inc.

          

   

Address:

          

102 East Main Street, Suite 500, Urbana, IL 61801

          

   

Phone:

          

(217) 550-1558                                                                                                                                                                                

          

   

Name:

          

Ralph Johnson

          

   

E-mail:

          

ralph.johnson@runtimeverification.com

          

   

Address:

          

102 East Main Street, Suite 500, IL 61801 - 2744

          

   

Phone:

          

(217) 621-3038                                                                                                                                                                                

          

   

Name:

          

Patrick MacKay

          

   

E-mail:

          

patrick.mackay@runtimeverification.com

          

   

Address:

          

102 East Main Street, Suite 500, IL 61801 - 2744

          

   

Phone:

          

(217) 550-1558                                                                                                                                                                                

          

   

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