Formal Verification Methods in Critical Systems
An overview of using model checking and automated theorem proving to guarantee software correctness in nuclear control-command systems.
Introduction
In critical systems such as the instrumentation and control (I&C) of nuclear power plants, software failure is not an option. Traditional testing methods—dynamic testing and simulation—are necessary but insufficient to guarantee the absence of faults.
Model Checking
Model checking is an automated technique that, given a finite-state model of a system and a formal property, systematically checks whether this property holds for (a given state in) that model.
Benefits
- Exhaustive coverage: Checks all possible states.
- Counter-examples: Provides a trace when a property is violated.
// Example of a simple state invariant
function invariant(temperature: number, pressure: number) {
assert(temperature < MAX_TEMP && pressure < MAX_PRESSURE);
}
Abstract Interpretation
Abstract interpretation formalizes the approximation of semantics of computer programs. It allows us to build static analyzers that can soundly evaluate programs to find potential runtime errors without executing them.
Conclusion
Combining these methods provides a robust defense against software defects, moving us from "testing to show presence of bugs" to "proving the absence of bugs".