A January 2014 ACM Journal has an interesting article on software verification at NASA JPL for the Mars Curiosity Rover at the link provided. A few things that I found interesting:
- Their standard for flight software is ISO-C99.
- The coding standard at JPL (http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf) is risk-based and has 6 “levels of compliance”. LOC-5 and LOC-6 are for safety-critical and human-rated software and include all MISRA rules.
- They state that there is “compelling evidence that higher assertion densities correlate with lower residual defect densities”, and therefore they specify a minimum assertion density of 2%.
- Assertions are left active in production code and if one triggers the system goes to a safe state.***
- They use four static analyzers: Coverity, Codesonar, Semmle, and Uno.
- They have an in-house tool called Scrub that combines the output of all four static analyzers plus human review comments into one unified system.
- Multi-threading issues including race conditions are a big concern. To mitigate that they use a free logic model checker called Spin.
Several years ago while I watched the mission control video of the Curiosity lander, I overheard one of the technicians saying not to worry about an error that they received from the craft during the landing since the software was in “battle-short mode”. So apparently there are times when the “safe-state” is overridden.
The article can be accessed here.