Jpl Program Cleans Mars Mission Code

Every programmer knows the need for software code review and verification. Bugs inevitably creep into the development cycle, potentially compromising quality. And the process of verification isn’t getting any easier as application code becomes larger and more complex.

While rigorous formal software verification techniques remain out of reach for large-scale development, two new tools—Scrub and Spin—have reached the point where they can be used routinely for verification, according to Gerard Holzmann, senior research scientist and fellow at the Jet Propulsion Laboratory in Pasadena, CA.

"Software is designed and developed by human beings who are not perfect; we all occasionally make mistakes," Holzmann says.

Formal verification techniques help prevent, detect and isolate the effect of code defects, Holzmann says. He introduced verification techniques at JPL to develop a tool-based process "where we move towards the use of machine readable and formally verifiable design artifacts at every stage of the development process: starting with requirements, through design, into coding and testing."

Holzmann says JPL is making good progress in introducing these techniques into flight software development for robotic space exploration.

"The Spin model checker was one of the first tools to support direct verification of implementation level C code, using a model extraction technique that we pioneered at Bell Labs in 1998," Holzmann says. The method uses a standard compiler front-end to parse code, then converts it into the format that’s recognized by the model checker.

Spin has a range of verification options that allow it to handle even very large applications, Holzmann says. "Recent extensions also allow it to take advantage of multi-core and grid computers, and a separate pre-processor called Swarm can allow it to perform very large runs in short amounts of time in the ‘cloud’ by using hundreds or thousands of small and independently executing CPUs or CPU cores," he says.

Both Spin and Swarm are generally available and can be downloaded either precompiled or in source form. Spin is available at http://spinroot.com/spin/Man/README.html, and Swarm at http://ftp.swarm.org/pub/swarm/.

Scrub-a-Dub

Scrub is a code review tool that reduces the reliance on human eyes when large amounts of source code must be reviewed in relatively short amounts of time. JPL uses Scrub to review the millions of lines of flight code for the Mars Science Laboratory robotic exploration mission, Holzmann says.

Scrub uses five different background tools to scan code and look for different types of defects. The tool "runs its analysis over all software in a code base every night and makes its results available to all developers immediately," Holzmann says. "We believe that the use of a tool like Scrub can reduce the number of undetected defects in a code base significantly, which translates into greater reliability and we hope a significantly reduced risk during mission operations."

Scrub is scheduled to become the main code review tool for all mission software at JPL, but is not yet released for general public distribution.