A Semantics-Based Verification Toolset for UAS Embedded Software

Develop bounded model checker for C programs that detects undefined behavior. Convert prototype developed in Phase I into a robust tool capable of analyzing Airliner, a drone autopilot developed by Windhover under contract from NASA. The bounded model checker and a C interpreter that detects undefined behavior in unit tests are both generated from the same formal semantics of C. Both the tools will be integrated into the build system of Airliner, and used to analyze Airliner and applications built from Airliner.

Much satellite software is written in C. For example, NASA's "core Flight Software" is written in C. Software for unmanned aircraft systems tends to be written in C. For example, Airliner is a drone autopilot.

C is the most widely used programming language for embedded systems, and is used in the automotive industry, in telecommunications, in robotics. It is used for the infrastructure of the internet. It is the main language used for Linux. Our tools can be applied to any software written in C.

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.