Dane Sabo
54cc24e2f9
D Writing/ERLM/:w A Writing/ERLM/biblatex.sty M Writing/ERLM/dane_proposal_format.cls M Writing/ERLM/main.aux M Writing/ERLM/main.bbl M Writing/ERLM/main.blg M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls
209 lines
13 KiB
TeX
209 lines
13 KiB
TeX
\newpage
|
|
\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}
|
|
|
|
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-0900~\cite{NUREG-0899, 10CFR50.34}, 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.59}. 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.
|
|
|
|
\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.
|
|
|
|
Nuclear plants operate with multiple control modes: automatic control where the
|
|
reactor control system maintains target parameters through continuous reactivity
|
|
adjustment, manual control where operators directly manipulate the reactor, and
|
|
various intermediate modes. In typical pressurized water reactor operation, the
|
|
reactor control system automatically maintains a floating average temperature
|
|
and compensates 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.
|
|
|
|
% \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.
|
|
%
|
|
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~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
|
|
however, retain control of strategic decision-making such as power level
|
|
changes, startup/shutdown sequences, mode transitions, and procedure
|
|
implementation. %%%NEED MORE
|
|
|
|
|
|
\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.
|
|
|
|
Current generation nuclear power plants employ 3,600+ active NRC-licensed
|
|
reactor operators in the United States~\cite{operator_statistics}. 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~\cite{10CFR50.54}. To become
|
|
a reactor operator, an individual spends several years to pass completed
|
|
training.
|
|
|
|
The role of these 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 does not guarantee safety. This tension
|
|
between operational flexibility and safety assurance remains unresolved in
|
|
current practice as the person responsible for reactor safety simultaneously is
|
|
usually the root cause of a failure.
|
|
|
|
Multiple independent analyses converge on a striking statistic: 70--80\% of all
|
|
nuclear power plant events are attributed to human error versus approximately
|
|
20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
|
|
all severe accidents at nuclear power plants such as those at Three Mile Island,
|
|
Chernobyl, and Fukushima Daiichi, has been identified as poor safety management
|
|
and poor safety culture--primarily human factors~\cite{hogberg_root_2013}. A
|
|
detailed analysis of 190 events at Chinese nuclear power plants from
|
|
2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
|
|
errors while 92\% were associated with latent errors (organizational and
|
|
systemic weaknesses that create conditions for failure).
|
|
|
|
%%%%% This seems like a bad paragraph. Doesn't really connect with the idea of
|
|
%%%%% autonomy. Seems more like a design issue for the control room. With more
|
|
%%%%% time it could be explained how doing things this way with requirements to
|
|
%%%%% logic would catch that no indicator of actual valve position is a problem.
|
|
% 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 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 500-fold underestimation. This
|
|
% dramatic failure demonstrated that human reliability could not be adequately
|
|
% assessed through expert judgment and historical data alone.
|
|
% % how does autonomy fix these issues exactly? This seems like
|
|
|
|
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
|
|
that cannot be overcome through training alone.} The persistent human
|
|
error contribution despite four decades of improvements demonstrates that these
|
|
limitations are fundamental rather than remediable part of human-driven control.
|
|
|
|
\subsection{HARDENS and Formal Methods}
|
|
|
|
The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
|
|
project represents the most advanced application of formal methods to nuclear
|
|
reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address the nuclear industry's
|
|
fundamental dilemma: existing U.S. nuclear control rooms rely on analog
|
|
technologies from the 1950s--60s. This technology is woefully out of date
|
|
compared to modern control technologies, and incurs significant risk and cost to
|
|
plant operation. The NRC contracted Galois, a company of formal methods experts,
|
|
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 a Reactor Trip
|
|
System (RTS) implementation with full traceability from NRC Request for
|
|
Proposals and IEEE standards through formal architecture specifications to
|
|
formally verified software.
|
|
%%% did it actually do an FPGA demonstration? Dubious.
|
|
|
|
HARDENS employed an array of formal methods tools and techniques across the
|
|
verification hierarchy. High-level specifications used Lando, SysMLv2, and FRET
|
|
(NASA Formal Requirements Elicitation Tool) to capture stakeholder
|
|
requirements, domain engineering, certification requirements, and safety
|
|
requirements. % this sentence is long af
|
|
Requirements were formally analyzed for consistency, completeness,
|
|
and realizability using SAT and SMT solvers. Executable formal models employed
|
|
Cryptol to create an executable behavioral model of the entire RTS including all
|
|
subsystems, components, and limited 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.
|
|
|
|
Despite its accomplishments, HARDENS has a fundamental limitation directly
|
|
relevant to hybrid control synthesis: 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 such as trip/no-trip decisions, digital sensor input
|
|
processing through discrete logic, and discrete actuation outputs such as
|
|
reactor trip commands. However, the project did not address continuous dynamics
|
|
of nuclear reactor physics. Real reactor safety depends on the interaction
|
|
between continuous processes such as temperature, pressure, neutron flux
|
|
evolving due to discrete control decisions. 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.} 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.
|
|
|
|
HARDENS produced a demonstrator system at Technology Readiness Level 2--3
|
|
(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{Kiniry2024} that 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 2--3 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.
|