Thesis/2-state-of-the-art/v2.tex

\section{State of the Art and Limits of Current Practice}

\textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 

No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify either discrete or continuous behavior—never both simultaneously. 

Three subsections structure this analysis. The first examines reactor operators and their operating procedures. The second addresses fundamental limitations of human-based operation. The third analyzes formal methods approaches that verify discrete logic or continuous dynamics—but not both together.

Section 3 addresses the verification gap these limits create.

\subsection{Current Reactor Procedures and Operation}

Current practice rests on two critical components: procedures and operators. Procedures define what must be done. Operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The next subsection examines operators—their reliability limits and contribution to accidents.

Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, while Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 

Procedure development rests on expert judgment and simulator validation—not formal verification. Regulations mandate rigorous assessment. 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof confirms that required actions complete within available time. No proof guarantees that transitions between procedure sets maintain safety invariants.

\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
and completeness.} No proof exists that procedures cover all
possible plant states. No proof confirms that required actions complete within available
timeframes. No proof guarantees that transitions between procedure sets maintain safety
invariants. Paper-based procedures cannot ensure correct application. Computer-based procedure systems similarly lack the formal guarantees that automated reasoning
could provide.

Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature, compensating for power demand changes through reactivity feedback loops alone. 

Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. 

Highly automated systems already handle reactor protection: automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators retain control of strategic decision-making—power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure forms the basis for autonomous hybrid control systems. It combines discrete human decisions with continuous automated control.

\subsection{Human Factors in Nuclear Accidents}

The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when executed imperfectly.

Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Operators determine when and how to act. This discretion introduces persistent failure modes that training cannot eliminate.

Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United States~\cite{operator_statistics}. These
operators divide 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 at least two ROs
and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
operator requires several years of training.

Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. 

Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combine to cause disaster. Operators misread confusing and contradictory indications, then shut off the emergency water system~\cite{Kemeny1979}. 

The President's Commission on TMI identified a fundamental ambiguity. Placing responsibility for safe power plant operations on the licensee does not guarantee safety—not without formally verifying that operators can fulfill this responsibility. This tension between operational flexibility and safety assurance remains unresolved. The person responsible for reactor safety often becomes the root cause of failure.

Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events~\cite{WNA2020}. Equipment failures account for only 20\%. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
of 190 events at Chinese nuclear power plants from
2007--2020~\cite{zhang_analysis_2025} found that active
errors appeared in 53\% of events, while latent errors—organizational and
systemic weaknesses that create conditions for failure—appeared in 92\%.


\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
that training alone cannot overcome.} Four decades of improvements have failed to eliminate human
error—these
limitations are fundamental to human-driven control, not remediable defects.

\subsection{Formal Methods}

The previous subsections established two fundamental limitations. First, procedures lack formal verification. Second, human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.

Formal methods could eliminate these limitations by providing mathematical guarantees of correctness. Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.

This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods. Each reveals the verification gap this research addresses.

\subsubsection{HARDENS: Formal Methods in Nuclear Control}

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 addressed a fundamental dilemma: existing U.S. nuclear control rooms rely on analog technologies from the 1950s--60s. These technologies incur significant risk and cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, 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. This traceability spans from NRC Request for Proposals and IEEE standards through formal architecture specifications to verified software.

HARDENS employed 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. Requirements
were analyzed for consistency, completeness, and realizability using SAT and SMT
solvers. Executable formal models used Cryptol to create a 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 verifiable C implementations and SystemVerilog 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 for hybrid control synthesis: the project addressed only discrete digital control logic. Continuous reactor dynamics remained unmodeled and unverified.
The Reactor Trip System specification and verification covered discrete state transitions (trip/no-trip decisions), digital sensor input processing through discrete logic, and discrete actuation outputs (reactor trip commands). Continuous reactor physics remained unaddressed. Real reactor safety depends on interactions between continuous processes—temperature, pressure, neutron flux—evolving in response to discrete control decisions. HARDENS verified the discrete controller in isolation, leaving the closed-loop hybrid system behavior unverified.

\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 also faced deployment maturity constraints beyond the technical limitation of omitting continuous dynamics. The project 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, not a finalized product, and that ``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), NRC licensing review, or human factors
validation with licensed 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.

\subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}

HARDENS verified discrete control logic without continuous dynamics—leaving half the hybrid system unverified.

Other researchers have attacked the problem from the opposite direction, extending temporal logics to handle hybrid systems directly. This complementary approach produced differential dynamic logic (dL). dL addresses continuous dynamics but encounters different limitations. dL introduces two additional operators
into temporal logic: the box operator and the diamond operator. The box operator
\([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
\(\alpha\) always remains within that region. In this way, it is a safety
invariant being enforced for the system. The second operator, the diamond
operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
one trajectory of \(\alpha\) that enters that region. This is a declaration of a
liveness property. 

%source: https://symbolaris.com/logic/dL.html

While dL allows for the specification of these liveness and safety properties,
actually proving them for a given hybrid system is difficult. Automated proof
assistants such as KeYmaera X exist to help develop proofs of systems using dL,
but fail for reasonably complex hybrid systems. State space explosion and
non-terminating solutions prevent creating system proofs using dL. 
%Source: that one satellite tracking paper that has the problem with the
%gyroscopes overloding and needing to dump speed all the time
Approaches have been made to alleviate
these issues for nuclear power contexts using contract and decomposition based
methods, but fall far short of a complete design methodology.
%source: Manyu's thesis. 
Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs. 

\textbf{LIMITATION:} \textit{Logic-based hybrid system verification has not
scaled to system design.} While dL and related approaches can verify hybrid
systems post-hoc, they require expert knowledge and have been applied only to
systems designed a priori. State space explosion prevents their use in the
design loop for complex systems like nuclear reactor startup procedures.

\subsection{Summary: The Verification Gap}

This section addressed two Heilmeier questions: What has been done? What are the limits of current practice?

\textbf{What has been done?} Three approaches currently exist. Each has fundamental limitations. First, human operators provide operational flexibility but introduce persistent reliability constraints that training cannot eliminate. Second, HARDENS verified discrete logic but omitted continuous dynamics. Third, differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.

\textbf{What are the limits of current practice?} A clear verification gap emerges. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.

The verification gap is clear. No existing methodology synthesizes provably correct hybrid controllers from operational procedures. Economic pressures demand autonomous control. Technical maturity now enables it. 

Section 3 addresses the next two Heilmeier questions. What is new? Why will it succeed? It presents the technical approach that closes this gap.