Mars Code by Gerald Holzmann, JPL Laboratory for Reliable Software.
Abstract:
On August 5 at 10:18 p.m. PDT, a large rover named Curiosity made a soft landing on the surface of Mars. Given the one-way light-time to Mars, the controllers on Earth learned about the successful touchdown 14 minutes later, at 10:32 p.m. PDT. As can be expected, all functions on the rover, and on the spacecraft that brought it to Mars, are controlled by software. In this talk we review the process that was followed to secure the reliability of this code.
Gerard Holzmann is a senior research scientist and a fellow at NASA’s Jet Propulsion Laboratory, the lab responsible for the design of the Mars Science Laboratory Mission to Mars and its Curiosity Rover. He is best known for designing the Logic Model Checker Spin, a broadly used tool for the logic verification of multi-threaded software systems. Holzmann is a fellow of the ACM and a member of the National Academy of Engineering.
Timemark 8:50 starts the discussion of software environments for testing.
The first slide about software reads:
3.8 million lines
~ 60,000 pages
~ 100 really large books120 Parallel Threads
2 CPUs (1 spare, not parallel, hardware backup)
5 years development time, with a team of 40 software engineers, < 10 lines of code per hour
1 customer, 1 use: it must work the first time
So how do you make sure you get it right?
Steps they took to make the software right:
- adopted a risk-based Coding Standard with tool-based compliance checks (very few rules and every rule had a mission that failed because the rule wasn’t followed)
- provided training & Certification for software developers
- conducted daily builds integrated with Static Source Code Analysis (with penalities for breaking the build)
- used a tool-based Code Review process
- thorough unit- and (daily) integration testing
- did Logic Verification of critical subsystems with a model checker
Continues to examine each these areas in detail. Be forewarned, the first level of conformance is compiling with all warnings on and having 0 warnings. The bare minimum.
BTW, there are a number of resources online at the JPL Laboratory for Reliable Software (LaRS).
Share this post with anyone who claims it is too hard to write secure software. It may be, for them, but not for everyone.