NASA Software Verification Article and Key Points

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.

Schedule Discussion with John F. Murray, Jr.

John is currently providing telephone and face-to-face meetings to discuss:  Cybersecurity, Part 11, 483 Response, design controls expectations for software documentation, and other topics.

Leave a message and we will contact you to schedule:

Corporate Office

+1-781-721-2921
Partners located in the US (CA, FL, MA, MN, TN) and Italy.