danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Editorial pass: tactical, operational, and strategic improvements

Browse Source 
Tactical (sentence-level):
- Strengthened weak verbs and passive constructions
- Improved issue-point positioning (old info first, new info in stress position)
- Removed unnecessary hedging phrases
- Fixed active/passive voice for clarity

Operational (paragraph/section):
- Added transition sentences between major subsections
- Strengthened flow between State of the Art and Research Approach
- Added connecting tissue between continuous controller types
- Improved coherence within outcomes section

Strategic (document-level):
- Made 'what's new' explicit with highlighted innovation statement
- Added summary paragraph to State of the Art defining the verification gap
- Strengthened connections between sections for Heilmeier alignment
- Clarified how the three-layer approach unifies existing tools
This commit is contained in:
Split 2026-03-09 12:07:07 -04:00
parent edfbb20cbe
commit 751a25780f
5 changed files with 170 additions and 125 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

101
1-goals-and-outcomes/research_statement_v1.tex
View File

@ -1,49 +1,47 @@
% 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.
This research develops a methodology for creating autonomous control systems
with event-driven control laws that guarantee 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.
written procedures to manage reactor control. Operators interpret plant
conditions and make critical decisions about when to switch between control
objectives.
% Gap
But, 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. Autonomous control
systems are needed that can safely manage complex operational sequences with the
same assurance as human-operated systems, but without constant supervision.
This reliance on human operators creates an economic challenge for
next-generation nuclear power plants. Small modular reactors face per-megawatt
staffing costs that significantly exceed those of conventional plants. These
economic constraints demand autonomous control systems that 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.
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
mirroring 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.
during transitions. 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 using reactive synthesis
to generate deterministic automata that are provably
correct by construction. Third, we will develop 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 on an Emerson Ovation control system.
A three-stage methodology will bridge this gap. First, we translate written
operating procedures into temporal logic specifications using NASA's Formal
Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
condition, component, timing, and response elements, enabling realizability
checking that identifies conflicts and ambiguities before implementation.
Second, we synthesize discrete mode switching logic using reactive synthesis to
generate deterministic automata that are provably correct by construction.
Third, we develop continuous controllers for each discrete mode using standard
control theory and reachability analysis. We classify continuous modes based on
their transition objectives, then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely and as the
deterministic automata specify. Local verification of continuous modes becomes
possible without global trajectory analysis across the entire hybrid system. An
Emerson Ovation control system will demonstrate this methodology.
% Pay-off
This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety guarantees.
This approach demonstrates that autonomous control can manage complex nuclear
power operations while maintaining safety guarantees.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
@ -52,31 +50,32 @@ If this research is successful, we will be able to do the following:
\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.
into formal specifications. Reactive synthesis tools will then generate
discrete control logic from these specifications.
% 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.
Control engineers will generate mode-switching controllers from regulatory
procedures with minimal formal methods expertise, reducing barriers to
high-assurance control systems.
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions. }
\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.
Reachability analysis will 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.
Engineers will design continuous controllers using standard practices while
ensuring system correctness, proving that mode transitions occur safely at
the right times.
% OUTCOME 3 Title
\item \textit{Demonstrate autonomous reactor startup control with safety
guarantees. }
guarantees.}
% Strategy
We will implement this methodology on a small modular reactor simulation
using industry-standard control hardware. % 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.
A small modular reactor simulation using industry-standard control hardware
will implement this methodology.
% Outcome
Control engineers will implement high-assurance autonomous controls on
industrial platforms they already use, enabling autonomy without retraining
costs or developing new equipment.
\end{enumerate}

58
1-goals-and-outcomes/v1.tex
View File

@ -1,9 +1,8 @@
\section{Goals and Outcomes}
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct
behavior.
This research develops a methodology for creating autonomous hybrid control
systems with mathematical guarantees of safe and correct behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability,
@ -22,26 +21,27 @@ Small modular reactors, in particular, face per-megawatt staffing costs far
exceeding those of conventional plants and threaten their economic viability.
% Critical Need
What is needed is a method to create autonomous control systems that safely
manage complex operational sequences with the same assurance as human-operated
systems, but without constant human supervision.
The nuclear industry needs autonomous control systems that safely manage complex
operational sequences with the same assurance as human-operated systems, but
without constant human supervision.
% APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction.
We will combine formal methods 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,
mirroring 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.
mirroring how operators change control strategies. Existing formal methods
generate provably correct switching logic from written requirements but cannot
handle the continuous dynamics that occur during transitions between modes.
Traditional control theory verifies continuous behavior but lacks tools for
proving correctness of discrete switching decisions. This gap between discrete
and continuous verification prevents end-to-end correctness guarantees.
% Hypothesis
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. If existing
procedures can be formalized into logical specifications and continuous dynamics
verified against transition requirements, then autonomous controllers can be
built that are provably free from design defects.
Our approach closes this gap by synthesizing discrete mode transitions directly
from written operating procedures and verifying continuous behavior between
transitions. If existing procedures can be formalized into logical
specifications and continuous dynamics verified against transition requirements,
then autonomous controllers can be built that are provably free from design
defects.
% Pay-off
This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry.
@ -74,10 +74,10 @@ If this research is successful, we will be able to do the following:
\item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy
We will establish methods for analyzing continuous control modes to ensure
they satisfy discrete transition requirements. Using classical control
theory for linear systems and reachability analysis for nonlinear dynamics,
we will verify that each continuous mode safely reaches its intended
transitions.
they satisfy discrete transition requirements. Classical control theory for
linear systems and reachability analysis for nonlinear dynamics will verify
that each continuous mode safely reaches its intended transitions.
% Outcome
Engineers will design continuous controllers using standard practices while
iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times.
@ -99,8 +99,18 @@ If this research is successful, we will be able to do the following:
\end{enumerate}
% IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous
These three outcomes—procedure translation, continuous verification, and
hardware demonstration—together establish a complete methodology from regulatory
documents to deployed systems.
\textbf{The key innovation} unifies discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems.
While formal methods can verify discrete logic and control theory can verify
continuous dynamics, no existing methodology bridges both with compositional
guarantees. This work establishes that bridge by treating discrete specifications
as contracts that continuous controllers must satisfy, enabling verification of
each layer independently while guaranteeing correct composition.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance

67
2-state-of-the-art/v2.tex
View File

@ -1,11 +1,11 @@
\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. To understand what is being automated, we must
first understand how nuclear reactors are operated today. This section examines
reactor operators and the operating procedures we aim to leverage, then
investigates limitations of human-based operation, and concludes with current
formal methods approaches to reactor control systems.
This research aims to create autonomous reactor control systems that are
tractably safe. Understanding what we automate requires first understanding how
nuclear reactors operate today. This section examines reactor operators and the
operating procedures we leverage, investigates limitations of human-based
operation, and concludes with current formal methods approaches to reactor
control systems.
\subsection{Current Reactor Procedures and Operation}
@ -14,8 +14,8 @@ 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, 10CFR50.34}, but their
scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899
provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but this
development 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
@ -30,9 +30,9 @@ 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.
invariants. Paper-based procedures cannot ensure correct application. Even
computer-based procedure systems lack the formal guarantees automated reasoning
could provide.
Nuclear plants operate with multiple control modes: automatic control, where the
reactor control system maintains target parameters through continuous reactivity
@ -55,8 +55,11 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
\subsection{Human Factors in Nuclear Accidents}
Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United States~\cite{operator_statistics}. These
Having established how nuclear plants currently operate through written
procedures and human operators, we now examine why this human-centered approach
poses fundamental limitations. 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
@ -96,6 +99,12 @@ error contribution despite four decades of improvements demonstrates that these
limitations are fundamental rather than a remediable part of human-driven control.
\subsection{Formal Methods}
The persistent human error problem motivates exploration of formal methods to
provide mathematical guarantees of correctness that human-centered approaches
cannot achieve. This subsection examines recent formal methods work in nuclear
control and identifies their limitations for autonomous hybrid systems.
\subsubsection{HARDENS}
The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
@ -180,11 +189,11 @@ 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 quite difficult. Automated
proof assistants such as KeYmaera X exist to help develop proofs of systems
using dL, but so far have been insufficient for reasonably complex hybrid
systems. The main issue behind creating system proofs using dL is state space
explosion and non-terminating solutions.
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 have been insufficient for reasonably complex hybrid systems. The main issue
behind creating system proofs using dL is state space explosion and
non-terminating solutions.
%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
@ -194,7 +203,21 @@ methods, but are far from a complete methodology to design systems with.
Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs.
%Maybe a limitation here? Something about dL doesn't scale or help in design
%very much, so the limitation is that logic based hybrid system approaches have
%not been used in the DESIGN of autonomous controllers, only in the analysis of
%systems that already exist.
\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}
Current practice reveals a fundamental gap: human operators provide operational
flexibility but introduce persistent reliability limitations, while formal
methods provide correctness guarantees but have not scaled to complete hybrid
control design. HARDENS verified discrete logic without continuous dynamics.
Differential dynamic logic can express hybrid properties but requires
post-design expert analysis. No existing methodology synthesizes provably
correct hybrid controllers from operational procedures with verification
integrated into the design process. This gap—between discrete-only formal
methods and post-hoc hybrid verification—defines the challenge this research
addresses.

63
3-research-approach/v3.tex
View File

@ -15,22 +15,21 @@
% ----------------------------------------------------------------------------
% 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
% ----------------------------------------------------------------------------
Previous approaches to autonomous control have verified
discrete switching logic or continuous control behavior, but not both
simultaneously. Validation of continuous controllers today consists of
extensive simulation trials. Discrete switching logic for routine operation
has been driven by human operators, whose evaluation includes simulated
control room testing and human factors research. Neither method, despite
being extremely resource intensive, provides rigorous guarantees of control
system behavior. HAHACS bridges this gap by composing formal methods from
computer science with control-theoretic verification, formalizing reactor
operations using the framework of hybrid automata.
Previous approaches to autonomous control verified discrete switching logic or
continuous control behavior, but not both simultaneously. Today's continuous
controller validation consists of extensive simulation trials. Human operators
drive discrete switching logic for routine operation; their evaluation includes
simulated control room testing and human factors research. Neither method
provides rigorous guarantees of control system behavior, despite being
extremely resource intensive. HAHACS bridges this gap by composing formal
methods from computer science with control-theoretic verification, formalizing
reactor operations using the framework of hybrid automata.
The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the governing
vector field, creating discontinuities in the system's behavior. Traditional
verification techniques designed for purely discrete or purely continuous
systems cannot handle this interaction directly.Our methodology addresses this
systems cannot handle this interaction directly. Our methodology addresses this
challenge through decomposition. We verify discrete switching logic and
continuous mode behavior separately, then compose these guarantees to reason
about the complete hybrid system. This two-layer approach mirrors the structure
@ -38,10 +37,10 @@ of reactor operations themselves: discrete supervisory logic determines which
control mode is active, while continuous controllers govern plant behavior
within each mode.
To build a high-assurance hybrid autonomous control system (HAHACS), we must
first establish a mathematical description of the system. This work draws on
Building a high-assurance hybrid autonomous control system (HAHACS) requires
first establishing a mathematical description of the system. This work draws on
automata theory, temporal logic, and control theory. A hybrid system is a
dynamical system that has both continuous and discrete states. The specific type
dynamical system with both continuous and discrete states. The specific type
of system discussed in this proposal is a continuous autonomous hybrid system.
This means that the system does not have external input and that continuous
states do not change instantaneously when discrete states change. For our
@ -73,9 +72,13 @@ where:
The creation of a HAHACS amounts to the construction of such a tuple together
with proof artifacts demonstrating that the intended behavior of the control
system is satisfied by its actual implementation. This approach is tractable now
because the infrastructure for each component has matured. The novelty is not in
the individual pieces, but in the architecture that connects them. By defining
system is satisfied by its actual implementation.
\textbf{What is new:} This approach is tractable now because the infrastructure
for each component has matured, but no existing work composes them for
end-to-end hybrid system verification. The novelty lies in the architecture that
connects discrete synthesis with continuous verification through well-defined
interfaces. By defining
entry, exit, and safety conditions at the discrete level first, we transform the
intractable problem of global hybrid verification into a collection of local
verification problems with clear interfaces. Verification is performed per mode
@ -145,8 +148,14 @@ complex reactor operations.
% ----------------------------------------------------------------------------
\subsection{System Requirements, Specifications, and Discrete Controllers}
Human control of nuclear power can be divided into three different scopes:
strategic, operational, and tactical. Strategic control is high-level and
Having defined the hybrid system mathematical framework, we now establish how to
construct such systems from existing operational knowledge. The key insight is
that nuclear operations already have a natural hybrid structure that maps
directly to the automaton formalism.
Human control of nuclear power divides into three scopes: strategic,
operational, and tactical. Strategic control is high-level and
long-term decision making for the plant. This level has objectives that are
complex and economic in scale, such as managing labor needs and supply chains to
optimize scheduled maintenance and downtime. The time scale at this level is
@ -355,8 +364,9 @@ according to operating procedures.
\subsection{Continuous Control Modes}
The synthesis of the discrete operational controller is only half of an
autonomous controller. These control systems are hybrid, with both discrete and
With the discrete controller synthesized and provably correct, we turn to the
continuous dynamics that execute within each discrete mode. The synthesis of the
discrete operational controller is only half of an autonomous controller. These control systems are hybrid, with both discrete and
continuous components. This section describes the continuous control modes that
execute within each discrete state, and how we verify that they satisfy the
requirements imposed by the discrete layer. It is important to clarify the scope
@ -478,8 +488,10 @@ appropriate to the fidelity of the reactor models available.
\subsubsection{Stabilizing Modes}
Stabilizing modes are continuous controllers with an objective of maintaining a
particular discrete state indefinitely. Rather than driving the system toward an
While transitory modes drive the system toward exit conditions, stabilizing
modes maintain the system within a desired operating region. Stabilizing modes
are continuous controllers with an objective of maintaining a particular
discrete state indefinitely. Rather than driving the system toward an
exit condition, they keep the system within a safe operating region. Examples
include steady-state power operation, hot standby, and load-following at
constant power level. Reachability analysis for stabilizing modes may not be a
@ -535,8 +547,9 @@ controller.
\subsubsection{Expulsory Modes}
Expulsory modes are continuous controllers responsible for
ensuring safety when failures occur. They are designed for robustness rather
Transitory and stabilizing modes handle nominal operations. When the plant
deviates from expected behavior, expulsory modes take over. Expulsory modes are
continuous controllers responsible for ensuring safety when failures occur. They are designed for robustness rather
than optimality. The control objective is to drive the plant to a safe shutdown
state from potentially anywhere in the state space, under degraded or uncertain
dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and

6
6-broader-impacts/v1.tex
View File

@ -22,9 +22,9 @@ approximately 23--30\% of the total levelized cost of electricity, translating
to \$21--28 billion annually for projected datacenter demand.
This research directly addresses the multi-billion-dollar O\&M cost challenge
through high-assurance autonomous control. Current nuclear operations require
full control room staffing for each reactor, whether large conventional units or
small modular designs. These staffing requirements drive the high O\&M costs
through the high-assurance autonomous control methodology developed in this
work. Current nuclear operations require full control room staffing for each
reactor, whether large conventional units or small modular designs. These staffing requirements drive the high O\&M costs
that make nuclear power economically challenging, particularly for smaller
reactor designs where the same staffing overhead must be spread across lower
power output. Synthesizing provably correct hybrid controllers from formal