USA flag logo/image

An Official Website of the United States Government

A Scalable Semantics-Based Verification System for Flight Critical Software

Award Information

Agency:
National Aeronautics and Space Administration
Branch:
N/A
Award ID:
Program Year/Program:
2013 / SBIR
Agency Tracking Number:
124989
Solicitation Year:
2012
Solicitation Topic Code:
A1.06
Solicitation Number:
Small Business Information
Runtime Verification Inc
2506 Lakewood Drive Champaign, IL 61822-7527
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 2013
Title: A Scalable Semantics-Based Verification System for Flight Critical Software
Agency: NASA
Contract: NNX13CL53P
Award Amount: $124,400.00
 

Abstract:

Modern flight-critical systems include hundreds of thousands to millions of lines of code. The Boeing 777, for instance, includes over 2 million lines of code. Future projects will only feature an increasing amount of source code, mostly written in the C programming language. The only way to completely ensure the safety of flight critical systems is through static, formal program verification. In order to effectively verify such large programs written in the C programming language, we propose a scaleable system for the verification of program written in C based on matching logic, or program verification logic. Matching logic has the benefit of being more scaleable than traditional Hoare/seperation logic verifiers because they build a large first order logic proof goal for entire functions at a time, while matching logic proceeds in program order, proving goals incrementally. Additionally, matching logic verifiers are based on operational semantics of the programming language in question. Operational semantics offer the benefit of being fully executable, so that one may increase belief that they are correct by testing typical compiler test suite programs, such as the GCC torture tests for the C language. Ultimately, our proposed research will result in a verifier that is both more scalable and more trustworthy than the competition.

Principal Investigator:

Patrick Meredith
Principal Investigator
2174180418
pmeredit@gmail.com

Business Contact:

Patrick Meredith
Business Official
2174180418
pmeredit@gmail.com
Small Business Information at Submission:

Runtime Verification Inc
2506 Lakewood Drive Champaign, IL 61822-7527

EIN/Tax ID: 271593403
DUNS: N/A
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No