A Semantics-Based Verification Toolset for UAS Embedded Software

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).

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.

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.

This is early/mid-stage (TRL 4) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

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.