Combining unit-level symbolic execution and system-level concrete execution for testing nasa software

TLDR

Testing safety‑critical software demands thorough methods, and this work is relevant beyond the NASA project context. The study proposes a testing approach that combines unit‑level symbolic execution with system‑level concrete execution to generate test cases meeting user‑specified criteria. They built Symbolic Java PathFinder, a symbolic execution framework atop Java PathFinder that propagates symbolic data via attributes, and leveraged system‑level concrete executions to refine unit‑level test generation, applying the approach to a NASA flight software component. The analysis uncovered a serious bug, prompting design changes to the software.

Abstract

We describe an approach to testing complex safety critical software that combines unit-level symbolic execution and system-level concrete execution for generating test cases that satisfy user-specified testing criteria. We have developed Symbolic Java PathFinder, a symbolic execution framework that implements a non-standard bytecode interpreter on top of the Java PathFinder model checking tool. The framework propagates the symbolic information via attributes associated with the program data. Furthermore, we use two techniques that leverage system-level concrete program executions to gather information about a unit's input to improve the precision of the unit-level test case generation. We applied our approach to testing a prototype NASA flight software component. Our analysis helped discover a serious bug that resulted in design changes to the software. Although we give our presentation in the context of a NASA project, we believe that our work is relevant for other critical systems that require thorough testing.