Despite a few spectacular failures, NASA is one of the top organizations worldwide in systems and software engineering. The Mars rover Opportunity recently celebrated 10 years of operation on Mars, and the newer Curiosity has been operating since August 2012, after a landing maneuver of unprecedented complexity. This is quite a feat, considering the fact that the nearest repair technician is over 30 million miles away, and the communications delay is about 15 minutes on average. How do they do it?

This article gives a rare glimpse into the process used in programming the Mars rovers. It focuses on three methods used to reduce the risk of failure. An important feature of all three methods is the use of automation. The first consists of a set of risk-related coding rules, based on actual risks observed in previous missions. For example, one rule requires the code to pass compilation and static analyzer checks without any warnings. Another requires the code to have a minimum assertion density of two percent. The assertions are enabled not only for testing, but also during the mission, when violations place the rover into a safe mode, during which failures can be diagnosed and fixed. All of the rules are checked automatically when the code is compiled.

The second method consists of tool-based code review. Four different static-analysis tools are used, with an automated system to manage the interaction between developers and reviewers in response to tool warnings. In over 80 percent of the cases, developers agreed with the warnings and fixed the code without reviewer intervention. An interesting observation Holzmann makes is that there was surprisingly little overlap between the warnings issued by the four tools.

The third and strongest method is the use of a model-checking tool for race conditions, one of the most difficult types of bugs to discover. This cannot be done for the whole code base, but was used extensively in the Curiosity mission to verify critical multithreaded algorithms. In some cases, the tool works directly from the C source code. For larger subsystems, input models have to be prepared manually in the language of the model checker; this can reduce the input size by over one order of magnitude.

The challenges faced by NASA are obviously unique, and are very different from those involved in cloud-based mobile applications, to use a popular example. There are many papers and books describing methodologies for developing such systems. However, developing safety-critical systems for cars and aircraft, medical devices, and power grids, or financial systems that must be resilient to faults and deliberate attacks, requires reliability levels similar to those of NASA. For developers of such systems, articles such as Holzmann’s should be required reading.