Communications of the ACM
Developing Software For the Outer Space
Gerard Holzmann was a keynote speaker at OOPSLA today. Gerard is a fellow at NASA's Jet Propulsion Laboratory (JPL) in Pasadena, California, and has done a great deal of software development for spacecrafts. It is indeed very interesting to see how NASA makes sure that their multi-million dollar space missions are not jeopardized due to programming glitches.
Gerard pointed out some interesting statistics on spacecraft software. The first moon lander in 1969 had a system equivalent to about 10,000 lines of code. By the estimates, the next Lunar mission to come in 2019 would have about 10 million lines of code! We would surely have the necessary hardware technologies to handle such a system, but it is inevitable that the number of defects also increase with such a large system. In Gerard's own words "the human brain is not going to get bigger that soon" and at current rate about two residual defects are found per 1000 lines of code. Geralds guiding principle is "if we don't learn to use computers to analyze our programs, we are in a losing battle."
JPL uses a number of automated code analyzing tools, both to verify the design and the code. Spin, an opensource formal verification tool, is one of NASA's work horses. As Gerard pointed out, the improvements and optimization in algorithms and the advances in the hardware allows model checking to be performed extremely quickly now (in the order of seconds) and it does not make sense not to do it, especially when millions of dollars are at stake. Verifying code is harder. Gerard explained the JPL solution for code verification, suitably named "scrub." Scrub is a hybrid system that has an automated verifier and also human reviewers that detect deviations from the coding guidelines. The effort that is taken to keep the complex spacecraft software working absolutely correct is indeed remarkable.
The lessons from JPL are equally applicable to today's software development processes. The cost of formal verification, both in terms of time and effort, have come down and at the same time failures are becoming costlier than ever. Perhaps it's time for us to take a lesson from NASA?
Comments
Ronald Woan
I think Gerard said they only use Spin on a very small part of the codebase whereas a portfolio of commercial tools like Coverity and GrammaTech in particular along with Gerard's own Uno and a battery of shell scripts are run on everything every night.
Ajith Ranabahu
Thanks Ron for pointing that out. I've modified the blog to indicate that SPIN is not the only tool.
Displaying all 2 comments