Software bugs are inevitable but must be uncovered early to ensure the most reliable software at the lowest cost. It is estimated that about half of software development costs are attributed to making sure the coding is correct. Considering the price of a space mission, the cost of an error could range from thousands during development to millions once a mission is under way.

NASA's 2003 Mars Exploration Rover (MER) Mission is twin rovers sampling Martian rocks, soils, and the atmosphere for at least 90 days.

At $400 million a rover, a coding error that shuts down a rover overnight would in effect be a $4.4 million mistake, not to mention a loss of valuable exploration time on the planet.

To catch such problems in the software code that flies during missions, a software verification and validation technique being developed at Ames is finding flaws automatically, faster, and more precisely than before.

"We detect what can interrupt the program, what can cause the program to crash," says researcher Guillaume Brat.

Software systems driving missions such as MER contain hundreds of thousands of lines of code that NASA developers currently test manually by writing test drivers and running tests as they write the code. The task is time consuming and cumbersome. Furthermore, NASA's large systems with real-time decision capability are difficult to develop and validate because the possibilities for outcomes are so vast.

Brat is part of a team of two developing C Global Surveyor (CGS), a software program based on a technique pioneered in the 1970s that hides all the data except what is necessary for finding errors. The software detects errors automatically, covering all possible execution paths without ever executing the program. Using a tool like CGS can save developers countless hours debugging code, says researcher Arnaud Venet. "You make the computer work for you instead of spending hours doing it."

With CGS, Brat says, "we can reason about all the behaviors with the program at once without having to go through each one of them."

Since its inception, just a few researchers have worked with abstract interpretation, trying to prove that the technique is practical. At present, just 20 or so people in the world might be working to develop efficient algorithms for the technique.

The CGS team started its research with tests using a commercial software tool that uses algorithms for abstract interpretation, to evaluate its effectiveness and to generate interest in a validation and verification tool.

Between the summers of 2002 and 2003 the team processed modules from NASA's Deep Space 1, a spacecraft that in 1999 flight-tested technologies for future missions, and parts of the 1997 Mars Pathfinder (MPF) mission and MER.

During a test with MPF code the commercial tool returned 80 to 85 precision, leaving 15 to 20 percent of the code to be checked manually. "In a mission, that's still a lot of things you have to verify," Brat says.

Six months later, in June 2003, the team applied CGS to the same code, dropping the processing time dramatically, from 40 hours to 35 minutes—and boosting precision to 90 to 95 percent. Early in July the team ran another test. The program completed the job in about 25 minutes.

Currently, CGS is built to look for runtime errors in C code, the coding language for the current Mars mission. Next the group will target C++, the programming language that will be adopted for future missions.

The Mars Technology Program has invested in CGS, and is studying its use for the 2009 Mars Science Laboratory mission. During the next few years the CGS team will customize and test the tool in the MSL software system environment.