Program Model Checking Using Design-for-Verification: NASA Flight Software Case Study

Model checking is a verification technique developed in the 1980s that has a history of industrial application in hardware verification and verification of communications protocol specifications. Program model checking is a technique for model checking software in which the program itself is the model to be checked. Program model checking has shown potential for detecting software defects that are extremely difficult to detect through traditional testing. The technique has been the subject of research and relatively small-scale applications but faces several barriers to wider deployment. This paper is a report on continuing work applying Java PathFinder (JPF), a program model checker developed at NASA Ames Research Center, to the shuttle abort flight management system, a situational awareness application originally developed for the space shuttle. The paper provides background on the model checking tools that were used and the target application, and then focuses on the application of a "design for verification" (D4V) principle and its effect on model checking. The case study helps validate the applicability of program model checking technology to real NASA flight software. A related conclusion is that application of D4V principles can increase the efficiency of model checking in detecting subtle software defects. The paper is oriented toward software engineering technology transfer personnel and software practitioners considering introducing program model checking technology into their organizations.