Join us on:

Scrub and Spin: Stealth Use of Formal Methods in Software Development

Gerard Holzmann, JPL Fellow / Adjunct Faculty Caltech CS

Gerard J. Holzmann is Senior Research Scientist and Fellow at the Jet Propulsion Laboratory in Pasadena, California. He received his PhD in 1979 from the Delft University of Technology in The Netherlands. From 1979 to 2003, he worked in the Bell Labs Computing Science Research Center in Murray Hill, New Jersey. Since 2003 he leads the Laboratory for Reliable Software at JPL in California.

Dr. Holzmann is best known for designing and building one of the most widely used formal verification systems for multi-threaded systems software: the Spin model checker, for which he was awarded the 2001 ACM Software Systems award. It may also explain his mysterious election to the National Academy of Engineering in 2005. He has published four books and numerous technical papers.

There is something roundly unsatisfactory about the way in which we normally develop software systems, especially large systems. Try as we might, bugs tend to get into the development cycle and they can prove to be very hard to eliminate. We have learned to live with statistics that say that we should expect roughly one residual defect for every one thousand lines of delivered code, post testing. Meanwhile, code sizes for typical applications continue to grow. The control software for a spacecraft, for instance, has grown in the last few decades from a few thousand to a few million lines of code. Do we know any better today than thirty years ago how to write such code reliably?

Although truly rigorous formal software verification techniques will probably remain out of reach for large-scale software development for a while longer, I will show that some very practical uses of formal methods have quietly reached the point where they can be used routinely. My example with be the use of two light-weight tools, Scrub and Spin, in the development of mission critical software at JPL.

Please email any questions to . This e-mail address is being protected from spambots. You need JavaScript enabled to view it