ML24115A066
| ML24115A066 | |
| Person / Time | |
|---|---|
| Issue date: | 04/23/2024 |
| From: | Basturescu S, Sushil Birla, Norbert Carte, Mauricio Gutierrez, Derek Halverson NRC/RES/DE |
| To: | |
| Sushil Birla 3014152311 | |
| Shared Package | |
| ML24115A064 | List: |
| References | |
| Download: ML24115A066 (1) | |
Text
Workshop on Mathematically Formalized Assurance for National Security (MFANS) Workshop, April 29, 2024, Collaborative Computing Center (C3), 955 MK Simpson Boulevard, Idaho Falls, ID 83415 Correct-by-Construction Reactor Protection Systems Authors: {Sushil Birla, Norbert Carte, Derek Halverson, Sergiu Basturescu, Mauricio Guitierrez}, U.S. Nuclear Regulatory Commission (NRC)
Nuclear Power Plant (NPP) operators in the USA have a long-standing concern that regulatory review &
approval of digital systems to protect large light water nuclear reactors takes too long, costs too much, and entails regulatory uncertainty; and the regulatory guidance is too prescriptive (esp. in the guidance concerning diversity in design). Industry desires a risk-informed performance-based approach.
In the risk-informing aspect, the industry attempts to show in the NPP-level risk analysis that the risk of a failed reactor protection system (RPS) is not particularly great; therefore, the regulator should lower the targeted level of its assurance. Diversity and defense in depth (D3) is used internationally to cover for the residual uncertainty a topic of ongoing discussion between the NRC and the Electric Power Research Institute (EPRI) risk analysts. A decrease in the extent of D3 would require a commensurate decrease in the residual uncertainty and thus, increase in the quality of the risk analysis. This could be a long road.
In the performance-based aspect, the NRC is pursuing a research portfolio which aspires to validate the premise that the requisite level of assurance at a lower cost, in less time, and with less uncertainty is feasible contrary to popular belief. The technical aspect of the premise is based on (a) a correct-by-construction (CbyC) approach, in which evidence is generated through analytical methods as the design progresses and (b) the RPS application logic is simple. The economics aspect is based, in part, on studies of historic data in non-nuclear application sectors, where those studies have shown that it is much more costly to fix defects discovered later in the engineering process the cost grows exponentially.
The CbyC evidence-generation approach is based on NRCs earlier proof-of-concept demonstration of an RPS design; the results are available at https://github.com/GaloisInc/HARDENS. To assure verifiability, the design is constrained with the Refinement principle. The design constraint approach seems to be aligned with the 2015 paper Digital system robustness via design constraints: The lesson of formal methods by Mayo Jackson et al, Sandia National Labs. Without such a preventative approach, it is exceedingly difficult to ensure that a design is safe, because the potential space of engineering deficiencies is large. Traditional hazard analysis techniques such as failure modes and effects analysis (FMEA), fault tree analysis (FTA), and their combination have not been effective at identifying hazard-contributing engineering deficiencies completely. The NPP industry sees promise in the MIT-developed STAMP/STPA technique. However, in workshops with experts and in our own case study, we have learned that the technique, by itself, cannot assure completeness of hazard identification. The results are strongly dependent upon the competence of the performer. Mauricio Gutierrez will be presenting our experience with STPA in the DICE Conference.
To understand how the evaluation of C-by-C evidence could be systematized for consistent results, one of the research teams in the DARPA/ARCOS project organized evidence from the NRCs HARDENS project in the form of a safety assurance case (SAC). This exercise helped identify some gaps (mostly in secondary or supporting evidence). The research-performer behind HARDENS was pleased with the results, which Prof. Robin Bloomfield will be presenting in the DICE Conference. NRC research is underway to fill the evidentiary gaps and demonstrate the resulting SAC.
The C-by-C engineering approach uses analytical methods whose accessibility and usability may be challenging to practitioners in the NPP industry. We hope that the DARPA PROVERS project will alleviate this issue. Two of the research teams plan to include HARDENS-based small case studies. We look forward to learning from the research performers and assessors in the PROVERS project.