diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index 4ff3bdac4..d8f80e8ac 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -4,7 +4,7 @@ \maketitle \input{goals-and-outcomes/v6} -\input{state-of-the-art/v4} +\input{state-of-the-art/v5} \input{research-approach/v3} \input{broader-impacts/v1} \input{metrics-of-success/v1} diff --git a/Writing/ERLM/state-of-the-art/v5.tex b/Writing/ERLM/state-of-the-art/v5.tex index 90cf17cb5..9c6430b51 100644 --- a/Writing/ERLM/state-of-the-art/v5.tex +++ b/Writing/ERLM/state-of-the-art/v5.tex @@ -1,21 +1,357 @@ \section{State of the Art and Limits of Current Practice} +The principal aim of this research is to create autonomous reactor control +systems that are tractably safe. But, to understand what exactly is being +automated, it is important to understand how nuclear reactors are operated +today. First, the reactor operator themselves is discussed. Then, operating +procedures that we aim to leverage later are examined. Next, limitations of +human-based operation are investigated, while finally we discuss current formal +methods based approaches to building reactor control systems. + \subsection{Current Reactor Procedures and Operation} -%How are operating procedures made and why do they exist -%what are different kinds of operating procedures +Current generation nuclear power plants employ 3,600+ active NRC-licensed +reactor operators in the United States. These operators are divided into Reactor +Operators (ROs) who manipulate reactor controls and Senior Reactor Operators +(SROs) who direct plant operations and serve as shift +supervisors~\cite{10CFR55}. Staffing typically requires 2+ ROs with at least one +SRO for current generation units. To become a reactor operator, an individual +might spend up to six years to pass required training~\cite{princeton}. -%NUREG 0899 +The role of human operators is paradoxically both critical and +problematic. Operators hold legal authority under 10 CFR Part 55 to make +critical decisions including departing from normal regulations during +emergencies. The Three Mile Island (TMI) accident demonstrated how +``combination of personnel error, design deficiencies, and component +failures'' led to partial meltdown when operators ``misread confusing +and contradictory readings and shut off the emergency water +system''~\cite{Kemeny1979}. The President's Commission on TMI identified +a fundamental ambiguity: placing ``responsibility and accountability for +safe power plant operations...on the licensee in all circumstances'' +without formal verification that operators can fulfill this +responsibility under all conditions~\cite{Kemeny1979}. This tension +between operational flexibility and safety assurance remains unresolved +in current practice. -%Whos in the control room +Nuclear plant procedures exist in a hierarchy: normal operating procedures for +routine operations, abnormal operating procedures for off-normal conditions, +Emergency Operating Procedures (EOPs) for design-basis accidents, Severe +Accident Management Guidelines (SAMGs) for beyond-design-basis events, and +Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage +scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are +developed using guidance from NUREG-0899~\cite{NUREG-0899}, but their +development process relies fundamentally on expert judgment and simulator +validation rather than formal verification. Procedures undergo technical +evaluation, simulator validation testing, and biennial review as part of +operator requalification under 10 CFR 55.59~\cite{10CFR55}. Despite these +rigorous development processes, procedures fundamentally lack formal +verification of key safety properties. There is no mathematical proof that +procedures cover all possible plant states, that required actions can be +completed within available timeframes under all scenarios, or that transitions +between procedure sets maintain safety invariants. -%how are reactor operators trained +\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness +and completeness.} Current procedure development relies on expert judgment and +simulator validation. No mathematical proof exists that procedures cover all +possible plant states, that required actions can be completed within available +timeframes, or that transitions between procedure sets maintain safety +invariants. Paper-based procedures cannot ensure correct application, and even +computer-based procedure systems lack the formal guarantees that automated +reasoning could provide. -%how are procedures tested +Nuclear plants operate with multiple control modes: automatic control where the +reactor control system maintains target parameters through continuous rod +adjustment, manual control where operators directly manipulate control rods, and +various intermediate modes. In typical pressurized water reactor operation, the +reactor control system automatically maintains a floating average temperature, +compensating for changes in power demand with reactivity feedback loops alone. +Safety systems instead operate with implemented automation. Reactor +Protection Systems trip automatically on safety signals with millisecond +response times, and engineered safety features actuate automatically on accident +signals without operator action required. -%Automation already is used for emergency systems +The current division between automated and human-controlled functions +reveals the fundamental challenge of hybrid control. Highly +automated systems handle reactor protection like automatic trips on safety +parameters, emergency core cooling actuation, containment isolation, +and basic process control. Human operators, however, retain control of +strategic decision-making such as power level changes, startup/shutdown +sequences, mode transitions, and procedure implementation. %%%NEED MORE + +\textbf{LIMITATION:} \textit{Current practice treats continuous plant +dynamics and discrete control logic separately.} No application of +hybrid control theory exists that could provide mathematical guarantees +across mode transitions, verify timing properties formally, or optimize +the automation-human interaction trade-off with provable safety bounds. \subsection{Human Factors in Nuclear Accidents} +The persistent role of human error in nuclear safety incidents, despite +decades of improvements in training and procedures, provides perhaps the +most compelling motivation for formal automated control with +mathematical safety guarantees. +Multiple independent analyses converge on a striking statistic: \textbf{70--80\% +of all nuclear power plant events are attributed to human error} versus +approximately 20\% to equipment failures~\cite{DOE-HDBK-1028-2009,WNA2020}. More +significantly, the International Atomic Energy Agency concluded that ``human +error was the root cause of all severe accidents at nuclear power plants''---a +categorical statement spanning Three Mile Island, Chernobyl, and Fukushima +Daiichi~\cite{IAEA-severe-accidents}. A detailed analysis of 190 events at +Chinese nuclear power plants from 2007--2020~\cite{Wang2025} found that 53\% of +events involved active errors while 92\% were associated with latent errors +(organizational and systemic weaknesses that create conditions for failure). The +persistence of this 70--80\% human error contribution despite four decades of +continuous improvements in operator training, control room design, procedures, +and human factors engineering. This suggests fundamental cognitive limitations +rather than remediable deficiencies. + +The Three Mile Island Unit 2 accident on March 28, 1979 remains the definitive +case study in human factors failures in nuclear operations. The accident began +at 4:00 AM with a routine feedwater pump trip, escalating when a +pressure-operated relief valve (PORV) stuck open---draining reactor +coolant---but control room instrumentation showed only whether the valve had +been commanded to close, not whether it actually closed. When Emergency Core +Cooling System pumps automatically activated as designed, operators made the +fateful decision to shut them down based on their incorrect assessment of plant +conditions. The result was a massive loss of coolant accident and the core +quickly began to overheat. During the emergency, operators faced more than 100 +simultaneous alarms, overwhelming their cognitive capacity~\cite{Kemeny1979}. +The core suffered partial meltdown with \textbf{44\% of the fuel melting} before +the situation was stabilized. + +Quantitative risk analysis revealed the magnitude of failure in existing +safety assessment methods: the actual core damage probability was +approximately 5\% per year while Probabilistic Risk Assessment +had predicted 0.01\% per year---a \textbf{500-fold underestimation}. +This dramatic failure demonstrated that human reliability could not be +adequately assessed through expert judgment and historical data alone. +%%%SOURCE??? Human Reliability Analysis (HRA) methods developed over four decades +quantify human error probabilities and performance shaping factors. The +SPAR-H method represents current best practice, +providing nominal Human Error Probabilities (HEPs) of \textbf{0.01 (1\%) +for diagnosis tasks} and \textbf{0.001 (0.1\%) for action tasks} under +optimal conditions~\cite{NUREG-CR-6883}. + +However, these nominal error rates degrade dramatically under realistic +accident conditions: inadequate available time increases HEP by +\textbf{10-fold}, extreme stress by \textbf{5-fold}, high complexity by +\textbf{5-fold}, missing procedures by \textbf{50-fold}, and poor +ergonomics by \textbf{50-fold}. Under combined adverse conditions +typical of severe accidents, human error probabilities can approach +\textbf{0.1 to 1.0 (10\% to 100\%)}---essentially guaranteed failure for +complex diagnosis tasks~\cite{NUREG-2114}. + +Rasmussen's influential 1983 taxonomy~\cite{Rasmussen1983} divides human errors +into skill-based (highly practiced responses, HEP $10^{-3}$ to $10^{-4}$), +rule-based (following procedures, HEP $10^{-2}$ to $10^{-1}$), and +knowledge-based (novel problem solving, HEP $10^{-1}$ to 1). Severe accidents +inherently require knowledge-based responses where human reliability is lowest. +Miller's classic 1956 finding~\cite{Miller1956} that working memory capacity is +limited to 7$\pm$2 chunks explains why Three Mile Island's 100+ +%WHAT IS A CHUNK? +simultaneous alarms exceeded operators' processing capacity. + +\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability +limits that cannot be overcome through training alone.} Response time +limitations constrain human effectiveness---reactor protection systems +must respond in milliseconds, 100--1000 times faster than human +operators. Cognitive biases systematically distort judgment: +confirmation bias, overconfidence, and anchoring bias are inherent +features of human cognition, not individual failings~\cite{Reason1990}. +The persistent 70--80\% human error contribution despite four decades of +improvements demonstrates that these limitations are fundamental +rather than remediable. \subsection{HARDENS and Formal Methods} + +The High Assurance Rigorous Digital Engineering for Nuclear Safety +(HARDENS) project, completed by Galois, Inc. for the U.S. Nuclear +Regulatory Commission in 2022, represents the most advanced application +of formal methods to nuclear reactor control systems to +date---and simultaneously reveals the critical gaps that remain. + +\subsubsection{Rigorous Digital Engineering Demonstrated Feasibility} + +HARDENS aimed to address the nuclear industry's fundamental dilemma: +existing U.S. nuclear control rooms rely on analog technologies from the +1950s--60s, making construction costs exceed \$500 million and timelines +stretch to decades. The NRC contracted Galois to demonstrate that +Model-Based Systems Engineering and formal methods could design, verify, +and implement a complex protection system meeting regulatory criteria at +a fraction of typical cost. + +The project delivered far beyond its scope, creating what Galois +describes as ``the world's most advanced, high-assurance protection +system demonstrator.'' Completed in \textbf{nine months at a tiny +fraction of typical control system costs}~\cite{Kiniry2022}, the project +produced a complete Reactor Trip System (RTS) implementation with full +traceability from NRC Request for Proposals and IEEE standards through +formal architecture specifications to formally verified binaries and +hardware running on FPGA demonstrator boards. + +Principal Investigator Joseph Kiniry led the team in applying Galois's +Rigorous Digital Engineering methodology combining model-based +engineering, digital twins with measurable fidelity, and applied formal +methods. The approach integrates multiple abstraction levels---from +semi-formal natural language requirements through formal specifications +to verified implementations---all maintained as integrated artifacts +rather than separate documentation prone to divergence. + +\subsubsection{Comprehensive Formal Methods Toolkit Provided Verification} + +HARDENS employed an impressive array of formal methods tools and +techniques across the verification hierarchy. High-level specifications +used Lando, SysMLv2, and FRET (NASA JPL's Formal Requirements +Elicitation Tool) to capture stakeholder requirements, domain +engineering, certification requirements, and safety requirements. +Requirements were formally analyzed for \textbf{consistency, +completeness, and realizability} using SAT and SMT solvers---verification +that current procedure development methods lack. + +Executable formal models employed Cryptol to create an executable +behavioral model of the entire RTS including all subsystems, components, +and formal digital twin models of sensors, actuators, and compute +infrastructure. Automatic code synthesis generated formally verifiable C +implementations and System Verilog hardware implementations directly +from Cryptol models---eliminating the traditional gap between +specification and implementation where errors commonly arise. + +Formal verification tools included SAW (Software Analysis Workbench) for +proving equivalence between models and implementations, Frama-C for C +code verification, and Yosys for hardware verification. HARDENS verified +both automatically synthesized and hand-written implementations against +their models and against each other, providing redundant assurance +paths. + +This multi-layered verification approach represents a quantum leap +beyond current nuclear I\&C verification practices, which rely primarily +on testing and simulation. HARDENS demonstrated that \textbf{complete +formal verification from requirements to implementation is technically +feasible} for safety-critical nuclear control systems. + +\subsubsection{Critical Limitation: Discrete Control Logic Only} + +Despite its impressive accomplishments, HARDENS has a fundamental +limitation directly relevant to hybrid control synthesis: \textbf{the +project addressed only discrete digital control logic without modeling +or verifying continuous reactor dynamics}. The Reactor Trip System +specification and formal verification covered discrete state transitions +(trip/no-trip decisions), digital sensor input processing through +discrete logic, and discrete actuation outputs (reactor trip commands). +The system correctly implements the digital control logic for reactor +protection with mathematical guarantees. + +However, the project did not address continuous dynamics of nuclear +reactor physics including neutron kinetics, thermal-hydraulics, xenon +oscillations, fuel temperature feedback, coolant flow dynamics, and heat +transfer---all governed by continuous differential equations. Real +reactor safety depends on the interaction between continuous processes +(temperature, pressure, neutron flux evolving according to differential +equations) and discrete control decisions (trip/no-trip, valve +open/close, pump on/off). HARDENS verified the discrete controller in +isolation but not the closed-loop hybrid system behavior. + +\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic +without continuous dynamics or hybrid system verification.} Hybrid +automata, differential dynamic logic, or similar hybrid systems +formalisms would be required to specify and verify properties like ``the +controller maintains core temperature below safety limits under all +possible disturbances''---a property that inherently spans continuous and +discrete dynamics. Verifying discrete control logic alone provides no +guarantee that the closed-loop system exhibits desired continuous +behavior such as stability, convergence to setpoints, or maintained +safety margins. + +\subsubsection{Experimental Validation Gap Limits Technology Readiness} + +The second critical limitation is \textbf{absence of experimental +validation} in actual nuclear facilities or realistic operational +environments. HARDENS produced a demonstrator system at Technology +Readiness Level 3--4 (analytical proof of concept with laboratory +breadboard validation) rather than a deployment-ready system validated +through extended operational testing. The NRC Final Report explicitly +notes~\cite{Kiniry2022}: ``All material is considered in development and +not a finalized product'' and ``The demonstration of its technical +soundness was to be at a level consistent with satisfaction of the +current regulatory criteria, although with no explicit demonstration of +how regulatory requirements are met.'' + +The project did not include deployment in actual nuclear facilities, +testing with real reactor systems under operational conditions, +side-by-side validation with operational analog RTS systems, systematic +failure mode testing (radiation effects, electromagnetic interference, +temperature extremes), actual NRC licensing review, or human factors +validation with licensed nuclear operators in realistic control room +scenarios. + +\textbf{LIMITATION:} \textit{HARDENS achieved TRL 3--4 without experimental +validation.} While formal verification provides mathematical correctness +guarantees for the implemented discrete logic, the gap between formal +verification and actual system deployment involves myriad practical +considerations: integration with legacy systems, long-term reliability +under harsh environments, human-system interaction in realistic +operational contexts, and regulatory acceptance of formal methods as +primary assurance evidence. + +\subsection{Research Imperative: Formal Hybrid Control Synthesis} + +Three converging lines of evidence establish an urgent research +imperative for formal hybrid control synthesis applied to nuclear +reactor systems. + +\textbf{Current reactor control practices} reveal fundamental gaps in +verification. Procedures lack mathematical proofs of completeness or +timing adequacy. Mode transitions preserve safety properties only +informally. Operator decision-making relies on training rather than +verified algorithms. The divide between continuous plant dynamics and +discrete control logic has never been bridged with formal methods. +Despite extensive regulatory frameworks developed over six decades, +\textbf{no mathematical guarantees exist} that current control approaches +maintain safety under all possible scenarios. + +\textbf{Human factors in nuclear accidents} demonstrate that human error +contributes to 70--80\% of nuclear incidents despite four decades of +systematic improvements. The IAEA's categorical statement that ``human +error was the root cause of all severe accidents'' reveals fundamental +cognitive limitations: working memory capacity of 7$\pm$2 chunks, +response times of seconds to minutes versus milliseconds required, +cognitive biases immune to training, stress-induced performance +degradation. Human Reliability Analysis methods document error +probabilities of 0.001--0.01 under optimal conditions degrading to +0.1--1.0 under realistic accident conditions. These limitations +\textbf{cannot be overcome through human factors improvements alone}. + +\textbf{The HARDENS project} proved that formal verification is +technically feasible and economically viable for nuclear control +systems, achieving complete verification from requirements to +implementation in nine months at a fraction of typical costs. However, +HARDENS addressed only discrete control logic without considering +continuous reactor dynamics or hybrid system verification, and the +demonstrator achieved only TRL 3--4 without experimental validation in +realistic nuclear environments. These limitations directly define the +research frontier: \textbf{formal synthesis of hybrid controllers that +provide mathematical safety guarantees across both continuous plant +dynamics and discrete control logic}. + +The research opportunity is clear. Nuclear reactors are quintessential +hybrid cyber-physical systems where continuous neutron kinetics, +thermal-hydraulics, and heat transfer interact with discrete control +mode decisions, trip logic, and valve states. Current practice treats +these domains separately---reactor physics analyzed with simulation, +control logic verified through testing, human operators expected to +integrate everything through procedures. \textbf{Hybrid control +synthesis offers the possibility of unified formal treatment} where +controllers are automatically generated from high-level safety +specifications with mathematical proofs that guarantee safe operation +across all modes, all plant states, and all credible disturbances. + +Recent advances in hybrid systems theory---including reachability +analysis, barrier certificates, counterexample-guided inductive +synthesis, and satisfiability modulo theories for hybrid systems---provide +the theoretical foundation. Computational advances enable verification of +systems with continuous state spaces that were intractable a decade ago. +The confluence of mature formal methods, powerful verification tools +demonstrated by HARDENS, urgent safety imperatives documented by +persistent human error statistics, and fundamental gaps in current +hybrid dynamics treatment creates a compelling and timely research +opportunity.