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

Benefits: 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.