Who's Who at NASA
NTB: You are probably best known in the field of software verification for inventing the SPIN (Simple Promela Interpreter) model checker for distributed software systems back in the 1980s. That tool is still in widespread use today. What sets SPIN apart from other verification systems, and to what do you attribute its incredible longevity?

Holzmann: I would also not have predicted that SPIN would last so long. In the best tradition of Bell Labs, it was meant to be simple to use, efficient, and based on good theory. A lot of work went into making the performance of that tool as good as it could be. The dictum at Bell Labs used to be, “Theory into tools and tools into practice.” SPIN sort of illustrates that trend. Of course, I developed it with a lot of help from my Bell Labs colleagues. There were some really, really good programmers there, people who developed Unix and C and C++, so I really benefited from that. A lot of the tool’s performance comes from their insights.

What amused me in the beginning was that a lot of people thought and said it was unfair to compare their verification tools to SPIN because the difference in performance was so large. I always found that amusing. Meanwhile, the field has become a lot richer. Today there are many more tools to choose from, so I am also surprised that SPIN can still hold its own and still perform as well as, if not better, than many of the tools that were developed by people that weren’t even born yet when SPIN was created. That’s very rewarding.

NTB: That has to give you a tremendous amount of pride.

Holzmann: Yes. That is very nice to see. At some point it will end, but I’m still waiting for that to happen.

NTB: Shortly after joining the Jet Propulsion Laboratory in 2003, the Research and Development Council of New Jersey awarded you a Thomas Alva Edison patent award in the information technology category for another invention you came up with at Bell labs called “Method and Apparatus for Testing Event Driven Software.” Tell us about that invention and how it was applied to the Mars Pathfinder, Deep Space 1, and Deep Impact missions.

Holzmann: Excellent question. In the late 1990s we had an opportunity to work with the people who were designing a new switch for Lucent Technologies. That’s something that doesn’t happen a lot because basically the technology that goes into telephone switches is fairly stable. There’s not a lot of renewal. So, they were starting a new development and they invited me to participate by trying to do formal verification on the software.

That patent covered a method that we came up with to convert ordinary C code into SPIN verification models that we could then mechanically analyze. I think that was the first time that anyone had dared to try to automate the verification process end to end: starting with implementation level code (rather than a formal design model of an algorithm), through a mechanical verification process, back to error scenarios that can trace an execution back at source level. We’ve applied some of the same techniques to recent space missions, but we also want to push the technology further and also make the conversion step unnecessary. Within LaRS we’re developing what we call a ‘model-driven’ verification technique where we use the compiled executable from an application, and drive it from a test harness that is controlled by the SPIN model checker. We’re getting very good results with this approach. The results are very encouraging.

NTB: In 2005, the Laboratory for Reliable Software, together with collaborators from NASA Ames, Kestrel, Northrop-Grumman, Princeton University, and your alma mater, Bell Labs, conducted a research project called Reliable Software Systems Development (RSSD). Tell us a little about that project and what it was designed to accomplish.

Holzmann: That was a very ambitious attempt to redesign the software development process from beginning to end. It was part of the Code-T funding stream. We participated in a fairly large competition with a proposal to basically redefine the software development lifecycle. It started with the observation that in every phase of the software development process — requirements capture, high-level design, low-level design, coding, testing, and operations — mistakes can be made. By developing the right tools, one can reduce the number of mistakes made, and improve the early detection of others. The plan was to develop a strong tool-based process to reduce the current reliance on much less rigorous human-based manual inspection processes.

« Start Prev 1 2 3 4 5 Next End»

The U.S. Government does not endorse any commercial product, process, or activity identified on this web site.