EDF Assesses Nuclear Plant Software Safety with Formal Methods Using Polyspace
This Approach Ensures Compliance with International Standards While Minimizing Software-Related Risks
“Polyspace analysis builds confidence, providing strong, robust evidence that the code will be free from run-time issues. We also used it to help with safety justification in our existing fleet of power stations where obsolete hardware instruments needed to be replaced by software-based instruments. Our use of Polyspace tools underpins reducing independent test efforts. For example, software robustness can be demonstrated in Polyspace Bug Finder using stricter checks and proven with Polyspace Code Prover, allowing the testing to focus on functional properties of the software.”
Key Outcomes
- Polyspace tools helped prove the absence of run-time errors and vulnerabilities in supplier software
- Polyspace Code Prover and Polyspace Bug Finder enabled EDF to meet the nuclear industry’s stringent qualification framework
- Polyspace tools helped demonstrate defect density down to 0.07 defects per 1,000 lines of code
EDF uses Polyspace products to meet a stringent qualification framework for nuclear energy, building independent confidence in safety-critical code.
EDF is the United Kingdom’s largest provider of carbon-free energy. To ensure consistent software quality in its latest generation of nuclear power plants, EDF uses Polyspace® tools to independently assess the software safety of supplier-provided code.
Operators in the United Kingdom’s civil nuclear industry must adhere to a stringent qualification framework to demonstrate that software-related risks in safety systems are minimized. Enforcing coding rules and using static code analysis based on formal methods to prove the absence of certain types of errors and vulnerabilities provide strong evidence that this goal is being achieved.
The qualification framework rests on two independent columns under NS-TAST-GD-046: Production Excellence (PE) and Independent Confidence Building Measures (ICBM). PE requires that software satisfies relevant international standards such as IEC 61508, IEC 62138, and IEC 60880, while ICBM consists of additional tests and analyses conducted independently from the supplier. While static code analysis is expected as part of the ICBMs at safety Class 2, it is mandatory for ICBMs at safety Class 1. Moreover, using formal methods to prove the absence of run-time errors and vulnerabilities provides strong evidence that risks from software in their safety systems are reduced.
During the PE process, EDF uses Polyspace products for checking vulnerabilities and enforcing MISRA™ coding compliance. For ICBM, Polyspace Bug Finder™ is typically used for Class 2 applications to detect safety and security vulnerabilities, which are then assessed by the analyst to determine the impact on the system’s safety. For Class 1 applications, Polyspace Code Prover™ is additionally used to prove the absence of run-time errors.
Using these checks, EDF can help prove that certain run-time errors are minimized, providing a solid base for approval and ensuring excellence throughout the supply chain. In a recent project, the EDF team demonstrated a very low defect density of 0.07 defects per 1,000 lines of code. With those benefits, Polyspace tools have also been used to help with safety justification in EDF’s existing fleet of power stations, supporting planned instrument obsolescence where hardware-based instruments are no longer available and software-based replacements must be justified.
