Dane Sabo
448feaf542
A Writing/ERLM/Sabo_Whitepaper.pdf M Writing/ERLM/dane_proposal_format.cls M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf M Writing/ERLM/main.synctex.gz
423 lines
23 KiB
TeX
423 lines
23 KiB
TeX
|
|
% PROJECT SUMMARY
|
|
\section*{Project Summary}
|
|
|
|
\subsection*{Overview}
|
|
|
|
This research will develop a methodology for creating autonomous hybrid control
|
|
systems with mathematical guarantees of safe and correct behavior. Nuclear power
|
|
plants require the highest levels of control system reliability, where failures
|
|
can result in significant economic losses or radiological release. Currently,
|
|
nuclear operations rely on extensively trained human operators who follow
|
|
detailed written procedures to manage reactor control. However, reliance on
|
|
human operators prevents introduction of autonomous control capabilities and
|
|
creates fundamental economic challenges for next-generation reactor designs.
|
|
Without introducing automation, emerging technologies like small modular
|
|
reactors face significantly higher per-megawatt staffing costs than conventional
|
|
plants, threatening their economic viability.
|
|
|
|
To address this need, we will combine formal methods from computer science
|
|
with control theory to build hybrid control systems that are correct by
|
|
construction. Hybrid systems use discrete logic to switch between continuous
|
|
control modes, similar to how operators change control strategies. Existing
|
|
formal methods can generate provably correct switching logic from written
|
|
requirements, but they cannot handle the continuous dynamics that occur during
|
|
transitions between modes. Meanwhile, traditional control theory can verify
|
|
continuous behavior but lacks tools for proving correctness of discrete
|
|
switching decisions. By synthesizing discrete mode transitions directly from
|
|
written operating procedures and verifying continuous behavior between
|
|
transitions, we can create hybrid control systems with end-to-end correctness
|
|
guarantees.
|
|
|
|
\subsection*{Intellectual Merit}
|
|
|
|
The intellectual merit lies in unifying discrete synthesis and continuous
|
|
verification to enable end-to-end correctness guarantees for hybrid systems.
|
|
This research will advance knowledge by developing a systematic,
|
|
tool-supported methodology for translating written procedures into temporal
|
|
logic, synthesizing provably correct discrete switching logic, and developing
|
|
verified continuous controllers. The approach addresses a fundamental gap in
|
|
hybrid system design by bridging formal methods from computer science and
|
|
control theory.
|
|
|
|
\subsection*{Broader Impacts}
|
|
|
|
This research directly addresses the multi-billion dollar operations and
|
|
maintenance cost challenge facing nuclear power deployment. By synthesizing
|
|
provably correct hybrid controllers, we can automate routine operational
|
|
sequences that currently require constant human oversight, enabling a shift
|
|
from direct operator control to supervisory monitoring. Beyond nuclear
|
|
applications, this research will establish a generalizable framework for
|
|
autonomous control of safety-critical systems including chemical process
|
|
control, aerospace systems, and autonomous transportation.
|
|
|
|
\newpage
|
|
|
|
% RESEARCH DESCRIPTION
|
|
\section*{Research Description}
|
|
|
|
\section{Objectives}
|
|
% GOAL PARAGRAPH
|
|
The goal of this research is to develop a methodology for creating autonomous
|
|
control systems with event-driven control laws that have guarantees of safe and
|
|
correct behavior.
|
|
|
|
% INTRODUCTORY PARAGRAPH Hook
|
|
Nuclear power relies on extensively trained operators who follow detailed
|
|
written procedures to manage reactor control. Based on these procedures and
|
|
operators' interpretation of plant conditions, operators make critical decisions
|
|
about when to switch between control objectives.
|
|
% Gap
|
|
While human operators have maintained the nuclear industry's exceptional safety
|
|
record, reliance on human operators has created an economic challenge for
|
|
next-generation nuclear power plants. Small modular reactors face significantly
|
|
higher per-megawatt staffing costs than conventional plants, threatening their
|
|
economic viability. Autonomous control systems are needed that can safely manage
|
|
complex operational sequences with the same assurance as human-operated systems,
|
|
but without constant supervision.
|
|
|
|
% APPROACH PARAGRAPH Solution
|
|
To address this need, we will combine formal methods from computer science with
|
|
control theory to build hybrid control systems that are correct by construction.
|
|
% Rationale
|
|
Hybrid systems use discrete logic to switch between continuous control modes,
|
|
similar to how operators change control strategies. Existing formal methods
|
|
generate provably correct switching logic but cannot handle continuous dynamics
|
|
during transitions, while traditional control theory verifies continuous
|
|
behavior but lacks tools for proving discrete switching correctness.
|
|
% Hypothesis and Technical Approach
|
|
We will bridge this gap through a three-stage methodology. First, we will
|
|
translate written operating procedures into temporal logic specifications using
|
|
NASA's Formal Requirements Elicitation Tool (FRET), which structures
|
|
requirements into scope, condition, component, timing, and response elements.
|
|
This structured approach enables realizability checking to identify conflicts
|
|
and ambiguities in procedures before implementation. Second, we will synthesize
|
|
discrete mode switching logic from these specifications using reactive synthesis
|
|
tools such as Strix, which generates deterministic automata that are provably
|
|
correct by construction. Third, we will develop and verify continuous
|
|
controllers for each discrete mode using standard control theory and
|
|
reachability analysis. We will classify continuous modes based on their
|
|
transition objectives, and then employ assume-guarantee contracts and barrier
|
|
certificates to prove that mode transitions occur safely and as defined by the
|
|
deterministic automata. This compositional approach enables local verification
|
|
of continuous modes without requiring global trajectory analysis across the
|
|
entire hybrid system. We will demonstrate this methodology by developing an
|
|
autonomous startup controller for a Small Modular Advanced High Temperature
|
|
Reactor (SmAHTR) and implementing it on an Emerson Ovation control system using
|
|
the ARCADE hardware-in-the-loop platform.
|
|
% Pay-off
|
|
This approach will demonstrate autonomous control can be used for complex
|
|
nuclear power operations while maintaining safety guarantees.
|
|
|
|
\vspace{11pt}
|
|
|
|
% OUTCOMES PARAGRAPHS
|
|
If this research is successful, we will be able to do the following:
|
|
\begin{enumerate}
|
|
% OUTCOME 1 Title
|
|
\item \textit{Synthesize written procedures into verified control logic.}
|
|
% Strategy
|
|
We will develop a methodology for converting written operating procedures
|
|
into formal specifications. These specifications will be synthesized into
|
|
discrete control logic using reactive synthesis tools. This process uses
|
|
structured intermediate representations to bridge natural language and
|
|
mathematical logic.
|
|
% Outcome
|
|
Control engineers will be able to generate mode-switching controllers from
|
|
regulatory procedures with little formal methods expertise, reducing
|
|
barriers to high-assurance control systems.
|
|
|
|
% OUTCOME 2 Title
|
|
\item \textit{Verify continuous control behavior across mode transitions. }
|
|
% Strategy
|
|
We will develop methods using reachability analysis to ensure continuous control modes
|
|
satisfy discrete transition requirements.
|
|
% Outcome
|
|
Engineers will be able to design continuous controllers using standard
|
|
practices while ensuring system correctness and proving mode transitions
|
|
occur safely at the right times.
|
|
|
|
% OUTCOME 3 Title
|
|
\item \textit{Demonstrate autonomous reactor startup control with safety
|
|
guarantees. }
|
|
% Strategy
|
|
We will implement this methodology on a small modular reactor simulation
|
|
using industry-standard control hardware. This trial will include multiple
|
|
coordinated control modes from cold shutdown through criticality to power
|
|
operation on a SmAHTR reactor simulation in a hardware-in-the-loop
|
|
experiment.
|
|
% Outcome
|
|
Control engineers will be able to implement high-assurance autonomous
|
|
controls on industrial platforms they already use, enabling users to
|
|
achieve autonomy without retraining costs or developing new equipment.
|
|
|
|
\end{enumerate}
|
|
\section{State of the Art and Limits of Current Practice}
|
|
|
|
Automation of some nuclear power operations is already performed today. Highly
|
|
automated systems handle reactor protection and emergency core cooling, while
|
|
human operators retain strategic decision-making. Autonomous systems are trusted
|
|
to handle emergency situations that are considered terminal operations, but
|
|
otherwise introduce too much risk to reactor operations. Contrary to this notion
|
|
is the fact that 70--80\% of all nuclear power plant events are attributed to
|
|
human error rather than equipment failures. The persistence of this ratio despite
|
|
four decades of improvements to procedures and control rooms suggests
|
|
fundamental cognitive limitations rather than remediable deficiencies.
|
|
|
|
The Nuclear Regulatory Commission has recognized that introducing automation
|
|
into the control room is the only way forward. Recent efforts to apply formal
|
|
methods to nuclear control have shown both promise and remaining gaps. The High
|
|
Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project
|
|
represents the most advanced application to date. HARDENS produced a complete
|
|
Reactor Trip System with full traceability from NRC requirements through formal
|
|
specifications to verified binaries of a controller implementation. The project
|
|
employed formal methods along the control design stack. This comprehensive
|
|
approach demonstrated that formal methods may be technically feasible and
|
|
economically viable for nuclear protection systems.
|
|
|
|
But despite these accomplishments, HARDENS has a fundamental limitation directly
|
|
relevant to our work. The project addressed only discrete digital control logic
|
|
without modeling or verifying continuous reactor dynamics. Real reactor safety
|
|
depends on interaction between continuous processes and discrete control
|
|
decisions. HARDENS verified the discrete controller in isolation but not the
|
|
closed-loop hybrid system behavior.
|
|
|
|
\section{Research Approach}
|
|
|
|
This research will overcome the identified limitations by combining formal
|
|
methods from computer science with control theory to build hybrid control
|
|
systems that are correct by construction. We accomplish this through three
|
|
main thrusts:
|
|
|
|
\begin{enumerate}
|
|
|
|
\item We will translate natural language procedures and
|
|
requirements into temporal logic specifications using the Formal Requirements
|
|
Elicitation Tool (FRET).
|
|
|
|
\item We will synthesize these temporal logic
|
|
specifications into the discrete component of the hybrid controller using
|
|
reactive synthesis.
|
|
|
|
\item We will build continuous control modes that satisfy discrete controller
|
|
transition requirements.
|
|
|
|
\end{enumerate}
|
|
|
|
Commercial nuclear power operations remain manually controlled despite
|
|
significant advances in control systems. The key insight is that procedures
|
|
performed by human operators are highly prescriptive and well-documented. To
|
|
formalize these procedures, we will use temporal logic, which captures system
|
|
behaviors through temporal relations. Linear Temporal Logic provides four
|
|
fundamental operators: next ($X$), eventually ($F$), globally ($G$), and until
|
|
($U$). These operators enable precise specification of time-dependent
|
|
requirements. The most efficient path to accomplish this translation is through
|
|
NASA's Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a
|
|
specialized requirements language that restricts requirements to easily
|
|
understood components while eliminating ambiguity. FRET enforces structure by
|
|
requiring all requirements to contain six components: Scope, Condition,
|
|
Component, Shall, Timing, and Response.
|
|
|
|
FRET provides functionality to check realizability of a system. Realizability
|
|
analysis determines whether written requirements are complete by examining the
|
|
six structural components. Complete requirements neither conflict with one
|
|
another nor leave any behavior undefined. Systems that are not realizable
|
|
contain behavioral inconsistencies that represent the physical equivalent of
|
|
software bugs. Using FRET during autonomous controller development allows us
|
|
to identify and resolve these errors systematically. FRET exports requirements
|
|
in temporal logic format compatible with reactive synthesis tools, enabling
|
|
the second thrust of our approach.
|
|
|
|
Reactive synthesis is an active research field focused on generating discrete
|
|
controllers from temporal logic specifications. The term reactive indicates
|
|
that the system responds to environmental inputs to produce control outputs.
|
|
These synthesized systems are finite in size, where each node represents a
|
|
unique discrete state. The connections between nodes, called state
|
|
transitions, specify the conditions under which the discrete controller moves
|
|
from state to state. This complete mapping constitutes a discrete automaton.
|
|
|
|
We will employ reactive synthesis tools which translate linear temporal logic
|
|
specifications into deterministic automata automatically while maximizing
|
|
generated automata quality. Once constructed, the automaton can be
|
|
straightforwardly implemented using standard programming control flow
|
|
constructs. The discrete automata representation yields an important theoretical
|
|
guarantee. Because the discrete automaton is synthesized entirely through
|
|
automated tools from design requirements and operating procedures, we can
|
|
prove that the automaton---and therefore our hybrid switching behavior---is
|
|
correct by construction.
|
|
|
|
This correctness guarantee is paramount. Mode switching represents the primary
|
|
responsibility of human operators in control rooms today. Human operators
|
|
possess the advantage of real-time judgment. When mistakes occur, they can
|
|
correct them dynamically. Autonomous control lacks this adaptive advantage. By
|
|
synthesizing controllers from logical specifications with guaranteed
|
|
correctness, we eliminate the possibility of switching errors.
|
|
|
|
While discrete system components will be synthesized with correctness
|
|
guarantees, they represent only half of the complete system. The continuous
|
|
modes will be developed after discrete automaton construction, leveraging the
|
|
automaton structure and transitions to design multiple smaller, specialized
|
|
continuous controllers.
|
|
|
|
The discrete automaton transitions mark decision points for switching between
|
|
continuous control modes and define their strategic objectives. We will
|
|
classify three types of high-level continuous controller objectives:
|
|
Stabilizing modes maintain the hybrid system within its current discrete mode,
|
|
corresponding to steady-state normal operating modes like full-power
|
|
load-following control. Transitory modes have the primary goal of
|
|
transitioning the hybrid system from one discrete state to another, such as
|
|
controlled warm-up procedures. Expulsory modes are specialized transitory
|
|
modes with additional safety constraints that ensure the system is directed to
|
|
a safe stabilizing mode during failure conditions, such as reactor SCRAM.
|
|
|
|
Building continuous modes after constructing discrete automata enables local
|
|
controller design focused on satisfying discrete transitions. The primary
|
|
challenge in hybrid system verification is ensuring global stability across
|
|
transitions. Current techniques struggle with this problem because dynamic
|
|
discontinuities complicate verification. This work alleviates these problems
|
|
by designing continuous controllers specifically with transitions in mind. By
|
|
decomposing continuous modes according to their required behavior at
|
|
transition points, we avoid solving trajectories through the entire hybrid
|
|
system.
|
|
|
|
To ensure continuous modes satisfy their requirements, we will employ three
|
|
complementary techniques. Reachability analysis computes the reachable set of
|
|
states for a given input set. We will use reachability when continuous
|
|
state ranges at discrete transition boundaries are defined and verify that
|
|
continuous modes only can reach such defined ranges. Otherwise, assume-guarantee contracts will be
|
|
employed when continuous state boundaries are not explicitly defined. For any
|
|
given mode, the input range for reachability analysis is defined by the output
|
|
ranges of discrete modes that transition to it. This compositional approach
|
|
ensures each continuous controller is prepared for its possible input range.
|
|
Finally, barrier certificates will prove that mode transitions are satisfied. Control
|
|
barrier functions provide a method to certify safety by establishing
|
|
differential inequality conditions that guarantee forward invariance of safe
|
|
sets.
|
|
|
|
Combining these three techniques will enable us to prove that continuous
|
|
components satisfy discrete requirements and thus complete system behavior. To
|
|
demonstrate this methodology, we will develop an autonomous startup controller
|
|
for a Small Modular Advanced High Temperature Reactor (SmAHTR). SmAHTR
|
|
represents an ideal test case with well-documented startup procedures that
|
|
must transition through multiple distinct operational modes: initial cold
|
|
conditions, controlled heating to operating temperature, approach to
|
|
criticality, low-power physics testing, and power ascension to full operating
|
|
capacity. We have access to an already developed high-fidelity SmAHTR model in Simulink that
|
|
captures the thermal-hydraulic and neutron kinetics behavior.
|
|
|
|
The synthesized hybrid controller will be implemented on an Emerson Ovation
|
|
control system platform, which is representative of industry-standard control
|
|
hardware. This control system will be used in a hardware-in-the-loop simulation,
|
|
where the Advanced Reactor Cyber Analysis and Development Environment
|
|
(ARCADE) suite will serve as the integration layer. This
|
|
hardware-in-the-loop configuration enables validation of the controller
|
|
implementation on actual industrial control equipment.
|
|
|
|
\section{Metrics of Success}
|
|
|
|
This research will be measured by advancement through Technology Readiness
|
|
Levels, progressing from fundamental concepts to validated prototype
|
|
demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where system
|
|
components operate successfully in a relevant laboratory environment. TRLs
|
|
provide the ideal success metric because they explicitly measure the gap between
|
|
academic proof-of-concept and practical deployment. This gap is precisely what
|
|
our work aims to bridge. TRLs capture both theoretical rigor and practical
|
|
feasibility simultaneously. The nuclear industry already uses TRLs for
|
|
technology assessment, making this metric directly relevant to potential
|
|
adopters.
|
|
|
|
Moving from current state (TRL 2--3) to target (TRL 5) requires progressing
|
|
through component isolation, system integration, and hardware validation. By
|
|
reaching TRL 5, we will have demonstrated a complete autonomous hybrid
|
|
controller operating on industrial control hardware through hardware-in-the-loop
|
|
testing. Achieving TRL 5 establishes both theoretical validity and practical
|
|
feasibility, proving that the methodology produces verified controllers
|
|
implementable with current technology and providing a clear pathway for nuclear
|
|
industry adoption and broader application to safety-critical autonomous systems.
|
|
|
|
\section{Broader Impacts}
|
|
|
|
Nuclear power presents both a compelling application domain and an urgent
|
|
economic challenge. Recent interest in powering artificial intelligence
|
|
infrastructure has renewed focus on small modular reactors for hyperscale
|
|
datacenters. According to the U.S. Energy Information Administration, advanced
|
|
nuclear power entering service in 2027 is projected to cost \$88.24 per
|
|
megawatt-hour. With datacenter electricity demand projected to reach 1,050
|
|
terawatt-hours annually by 2030, operations and maintenance costs represent
|
|
approximately 23--30\% of total levelized cost, translating to \$21--28
|
|
billion annually for projected datacenter demand.
|
|
|
|
This research directly addresses the multi-billion dollar O\&M cost challenge.
|
|
Current nuclear operations require full control room staffing for each reactor.
|
|
These staffing requirements drive high O\&M costs, particularly for smaller
|
|
reactor designs where the same overhead must be spread across lower power
|
|
output. The economic burden threatens the viability of next-generation nuclear
|
|
technologies. But, by synthesizing provably correct hybrid controllers, we can
|
|
automate routine operational sequences that currently require constant human
|
|
oversight. This enables a change from direct operator control to
|
|
supervisory monitoring where operators oversee multiple autonomous reactors
|
|
rather than manually controlling individual units. The transition fundamentally
|
|
changes the economics of nuclear operations.
|
|
|
|
The correct-by-construction methodology is critical for this transition.
|
|
Traditional automation approaches cannot provide sufficient safety guarantees
|
|
for nuclear applications where regulatory requirements and public safety
|
|
concerns demand the highest levels of assurance. By formally verifying both
|
|
discrete mode-switching logic and continuous control behavior, this research
|
|
will produce controllers with mathematical proofs of correctness. These
|
|
guarantees enable automation to safely handle routine operations that
|
|
currently require human operators to follow written procedures.
|
|
|
|
Beyond nuclear applications, this research will establish a generalizable
|
|
framework for autonomous control of safety-critical systems. The methodology of
|
|
translating operational procedures into formal specifications, synthesizing
|
|
discrete switching logic, and verifying continuous mode behavior applies to any
|
|
hybrid system with documented operational requirements. Potential applications
|
|
include chemical process control, aerospace systems, and autonomous
|
|
transportation. These domains share similar economic and safety considerations
|
|
that favor increased autonomy with provable correctness guarantees. By
|
|
demonstrating this approach in nuclear power this research will establish both
|
|
technical feasibility and regulatory pathways for broader adoption across
|
|
critical infrastructure.
|
|
|
|
\newpage
|
|
|
|
% REFERENCES CITED
|
|
|
|
\begin{thebibliography}{99}
|
|
|
|
\bibitem{10CFR55}
|
|
U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.''
|
|
\textit{Code of Federal Regulations}, 2024.
|
|
|
|
\bibitem{Kemeny1979}
|
|
J. G. Kemeny et al. ``Report of the President's Commission on the Accident
|
|
at Three Mile Island.'' U.S. Government Printing Office, October 1979.
|
|
|
|
\bibitem{NUREG-0899}
|
|
U.S. Nuclear Regulatory Commission. ``Guidelines for the Preparation of
|
|
Emergency Operating Procedures.'' NUREG-0899, August 1982.
|
|
|
|
\bibitem{DOE-HDBK-1028-2009}
|
|
U.S. Department of Energy. ``Human Performance Improvement Handbook.''
|
|
DOE-HDBK-1028-2009, June 2009.
|
|
|
|
\bibitem{WNA2020}
|
|
World Nuclear Association. ``Safety of Nuclear Power Reactors.''
|
|
\textit{World Nuclear Association Information Library}, 2020.
|
|
|
|
\bibitem{Kiniry2022}
|
|
J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear
|
|
Safety (HARDENS).'' NRC Final Technical Report ML22326A307, October 2022.
|
|
|
|
\bibitem{eia_lcoe_2022}
|
|
U.S. Energy Information Administration. ``Levelized Costs of New Generation
|
|
Resources in the Annual Energy Outlook 2022.'' Report, March 2022.
|
|
|
|
\bibitem{eesi_datacenter_2024}
|
|
Environmental and Energy Study Institute. ``Data Center Energy Needs are
|
|
Upending Power Grids and Threatening the Climate.'' Web article, 2024.
|
|
|
|
\end{thebibliography}
|
|
|