Dr. Gerard Holzmann, Senior Research Scientist at the Laboratory for Reliable Software, NASA’s Jet Propulsion Laboratory

After a 23 year career at Bell Labs, Dr. Gerard Holzmann joined NASA’s Jet Propulsion Laboratory in 2003 to help create the Laboratory for Reliable Software (LaRS), which he currently manages. Dr. Holzmann is credited with inventing the SPIN model checker for distributed software systems and a Method and Apparatus for Testing Event Driven Software, as well as authoring The Power of 10: Rules for Developing Safety Critical Code, and the groundbreaking book Beyond Photography – The Digital Darkroom.

NASA Tech Briefs: After completing your education at Delft University of Technology in the Netherlands, you spent the first 20-plus years of your career at Bell Labs working in their Computing Science Research Center. What made you decide to leave Bell Labs in 2003 and work for NASA?

Dr. Gerard Holzmann: That’s a good question. I consider myself fortunate to have spent such a long time at Bell Labs during what many people call “the golden days of research at Bell Labs.”

NTB: It was arguably one of the most famous think tanks in the world.

Holzmann: Yes, that’s right. A lot of really important inventions came out of that lab. Also, at that time – the 1980s and 90s – Bell Labs had a lot of really talented people working there. The company that owned Bell Labs, which was AT&T at that time, was quite powerful and rich, so it was a very special research environment with almost no restrictions and virtually complete freedom for researchers.
But 23 years is a very long time and life is too short to spend it all in one place. When many of my colleagues started leaving Bell Labs around 2001 and 2002, I also started looking. In some sense, most of us tried to find a research environment as close as possible to the old Bell Labs. Many of my friends – about 20 of my colleagues from the Computer Science Research Center – found it in the somewhat unconventional culture at Google, which indeed is very similar to Bell Labs in the early eighties. I was more attracted to the passion that I saw in the scientists and engineers working on space missions at JPL. I’d had a lot of interaction with JPL, working on software verification problems, so that really attracted me to JPL. I was sort of partially recreating that spark from the early eighties of being part of a research agenda that people really felt passionate about, like the exploration of the solar system and the universe. I’m really happy I made that change.

NTB: You currently head-up NASA/JPL’s Laboratory for Reliable Software. What is the Laboratory for Reliable Software, and what types of projects does it typically get involved with?

Holzmann: We started LaRS more or less as an experiment, to see if we could help figure out some of the more difficult software related problems that can complicate the execution of ever more complex space missions. We’ve seen our share of anomalies on missions that we’ve flown in the past, some of them caused by software malfunctions. If you look at the trends, the amount of software that we use to control spacecraft is increasing very rapidly. The next mission to Mars, for instance, — the Mars Science Laboratory (MSL) mission — will fly more code than all earlier missions to Mars combined. We want to make sure that this software is as robust as it can be. We want to avoid having to debug a crashed computer that sits on the surface of another planet, a few million miles away.
As one first step in this process, we introduced new static source code analysis tools at JPL, and they are now pretty much a standard part of the software development life cycle here. We also introduced a strong new coding standard that has meanwhile become the JPL Institutional Standard for flight code. Within LaRS we hired some strong researchers in software verification and testing techniques, and their influence is starting to show. We’re working closely with missions such as MSL to help figure out ways to reduce risk and to improve the tools we use in developing really robust software.