Runtime Verification, Inc. — National Aeronautics and Space Administration SBIR Phase I: A2

Description

We propose a new verification method for software intended to be flown onnbsp;unmanned aircraft systems that is both automatic and inexpensive.nbsp;In Phase 1 we will focus on a class of errors in C programs called ldquo;undefined behaviorrdquo; (UB) because this makes the method both easy to use and easy to compare with existing static analysis tools.nbsp; But in subsequent phases we plan to extend it to arbitrary program specifications, including those using temporal logic.nbsp;This verification method has been used for non-real-time software, we will extend it to real-time embedded systems.nbsp; 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;nbsp; (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).