Safety-Critical Software

NASA lays out a set of rules in the paper “The Power of 10 Rules” that, when followed, help increase confidence in the correctness of software. This aids the development of safety-critical software systems by reducing ambiguity and complexity as much as possible. The rules are designed to make the software easier to understand, analyse, and verify safety-critical applications where failures can have severe consequences.

Rules

1. All code must be restricted to a simple control flow that never includes goto statements, setjmp or longjmp constructs, or direct or indirect recursion.
2. All loops must have a fixed upper bound on the number of iterations, regardless of the input data, making it trivially possible to prove statically that the loop cannot exceed a preset upper bound.
3. Dynamic memory allocation is never allowed after initialization.
4. No function should be longer than can be printed on a single sheet of paper, using one line per statement and declaration.
5. Code assertion density should average at least two assertions per function. Assertions must check for anomalous conditions that should never occur during normal execution. All assertions must be side-effect-free and defined as Boolean tests. When an assertion fails, an explicit recovery action must be taken, such as returning an error condition to the caller. Any assertion that a static checking tool can prove can never fail or can never hold violates this rule.
6. Declare all data objects at the smallest possible level of scope.
7. A calling function must always check the return value of non-void functions, and all called functions must check the validity of all parameters provided by the caller.
8. The use of the preprocessor must be limited to the inclusion of header files and simple macro definitions. Token pasting, variable argument lists (ellipses), and recursive macro calls are never allowed. All macros must expand into complete syntactic units. The use of conditional compilation directives must be kept to a minimum.
9. The use of pointers must be restricted. Specifically, no more than one level of dereference should be used. Pointer dereference operations may not be hidden in macro definitions or inside typedef declarations. Function pointers are never permitted.
10. All code must be compiled, from the first day of development, with all compiler warnings enabled in the most pedantic mode available. All code must compile without warnings. A daily check of all code with a static source code analyser must be performed, and all analyses must pass with zero warnings.