OREGON STATE UNIVERSITY

You are here

Putting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving

TitlePutting Flight Software Through the Paces with Testing, Model Checking, and Constraint-Solving
Publication TypeConference Paper
Year of Publication2008
AuthorsGroce, A., G. J. Holzmann, R. Joshi, and R-G. Xu
Conference NameIn Workshop on Constraints in Formal Verification
Pagination1--15
Date Published08/2008
Conference Location Sydney, Australia
Abstract

In this paper we discuss the application of a range of techniques to the verification of mission critical flight software for a JPL mission. It is clear that for this type of application we want to achieve a higher level of confidence than can be achieved through standard software testing. Unfortunately, given the current state of the art, especially if one has to comply with the tight deadlines and resource limitations of a flight project, it is not feasible to produce a rigorous formal proof of correctness of a flight file system. This means that we must look for a practical alternative in the gray area between traditional testing and proof, trying to optimize rigor and coverage as much as possible. The approach that we describe here is based on a combination of random testing, model checking, and static source code analysis. The results we have obtained are encouraging, and suggest that for more complex properties of programs with complex data structures, it is possibly more beneficial to use constraint solvers to guide execution (i.e., testing, even if performed by a model checking tool) than to translate the program and property into a set of constraints, as in abstraction-based and bounded model checkers.