Certified compilation improves nuclear safety instrument software reliability
Certified Compilation in the TELEPERM XS Nuclear Safety I&C Platform
Software Engineering
Summary
Nuclear power plants rely on special computer systems to keep reactors safe. The paper explains how a highly trusted software compiler helps ensure these systems work correctly by producing verified code. The authors also found and fixed a performance problem in the compiled code, making the software faster and even more reliable. This work strengthens the safety of nuclear control systems beyond just maintaining it.
What this means in practice
- •For nuclear control engineers: Use formally certified compilers to build safer and more reliable control software for nuclear power plants.
- •For real-time embedded software developers: Improve performance and trustworthiness of safety-critical embedded software by integrating verified compilation techniques.
Authors
Alexandre Berard, Richard B. Kreckel
Abstract
The large safety instrumentation & control (I&C) systems in civil nuclear power plants (NPPs) are mainly safe-shutdown systems (reactor protection) or limitation and control systems. Framatome's established TELEPERM XS (TXS Core) product family is a digital I&C system platform to cover all these applications. We illustrate the role of verification in the different stages of the software production toolchain, focus on the formal compilation process, and discuss the contribution of the CompCert certified compiler to the safety case of the product. Scrutinizing the object code produced by this compiler has exhibited suboptimal run-time performance in a certain simple but recurring generated code pattern. We explain how formal methods allow us to address this issue in the compiler while simultaneously reducing its trusted computing base (TCB), thereby strengthening the safety case rather than merely preserving it.