A Scalable Semantics-Based Verification System for Flight Critical Software

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.

Our matching logic verification system for the C programming language will lower the time to develop, and reduce the number of bugs in NASA software. Our verification will be one of the most comprehensive available, able to prove very difficult algorithms correct. It will be particularly useful in mission-critical and safety-critical systems, flights systems in particular, where bugs cannot be tolerated. This work is equally useful to any government agency, which produces software, but, in particular, to those with mission or safety critical code. We also believe that the term rewriter developed in this project will have uses as a faster replacement for Maude in some specific cases (e.g., no associative or commutative matching and where builtin data structures are desirable).

We plan to market our completed tool to software companies, such as Microsoft and Google. Additionally, we have written confirmation from Dr. Shin'ichi Shirashi of Toyota-ITC that they would like to apply our tool in the automative industry, should this project be funded. We believe, especially with the movement to multicore architectures, multi-threaded systems being harder to verify, that all software companies, and potentially even students, can benefit from our work. We plan to allow a relatively cheap single user license download of the system, with a free license for open source projects. We believe that such a licensing structure allows for risk-free adaptation of our technology. From video games, to media players, to business applications, to Mars rover control programs, all may benefit from the increased ability to guarantee the operation of software components provided by our system.

This is a mature technology (TRL 7) — the realistic path in is usually NASA's Technology Transfer Program: licensing an existing NASA patent, or a Space Act Agreement to use NASA facilities/expertise directly. NASA also runs a startup licensing program with no upfront fee for companies formed to commercialize a specific NASA technology.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.