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

Clean draft: strip all split/DAS comments, keep oldt/newt tracked changes for review

Browse Source
This commit is contained in:
Split 2026-03-16 14:10:36 -04:00
parent 6901dc8276
commit 70d1874ca4
8 changed files with 81 additions and 248 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
1-goals-and-outcomes/goals.tex
View File

@ -1,20 +1,15 @@
\section{Goals and Outcomes}
\dasinline{Research statement is very similar to GO
because that's what I had when I prepared it.
If it's going to be an executive summary, it
should talk more about the other sections rather
than just being a slightly different GO section.}
% 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.\splitnote{Clear thesis statement. Gets right to it.}
behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service
interruptions, or radiological
release.\splitnote{Stakes established immediately — good hook.}
release.
% Known information
Currently, nuclear plant operations rely on extensively trained human
operators who follow detailed written procedures and strict regulatory
@ -47,8 +42,7 @@ 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.\splitnote{Excellent setup of the gap — shows why neither approach
alone is sufficient.}
decisions.
% Hypothesis
By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can
@ -56,7 +50,7 @@ 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.\splitnote{Hypothesis is clear and testable.}
defects.
% Pay-off
\oldt{This approach will enable autonomous control in nuclear power plants
while maintaining the high safety standards required by the industry.
@ -91,8 +85,7 @@ If this research is successful, we will be able to do the following:
expertise, lowering the barrier to high-assurance control systems.}
\newt{This will lower the barrier to high-assurance control systems by
generating verified mode-switching controllers directly from regulatory
procedures.}\dasinline{Same comment as in executive summary. Might not be
true and is not the point.}
procedures.}
% OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.}
@ -116,8 +109,7 @@ If this research is successful, we will be able to do the following:
reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power
operation.\splitnote{``cold shutdown through criticality to power
operation'' — concrete and impressive scope.}
operation.
% Outcome
We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward
@ -128,7 +120,7 @@ If this research is successful, we will be able to do the following:
% IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid
systems.\splitnote{Clear ``what's new'' statement.}
systems.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior.
@ -143,5 +135,4 @@ provide the tools to achieve that autonomy while maintaining the exceptional
safety record the nuclear industry requires.} \newt{This research will
provide the tools to achieve that autonomy while maintaining the exceptional
safety record the nuclear industry
requires.}\dasinline{This paragraph is literally the same as the rest of the
GO. Does not belong here and feels very redundant.}
requires.}

25
1-goals-and-outcomes/research-statement.tex
View File

@ -2,10 +2,7 @@
The goal of this research is to develop a methodology for creating autonomous
\oldt{control systems with event-driven control laws that have guarantees of
safe and correct behavior.} \newt{hybrid control systems with mathematical
guarantees of safe and correct behavior.}\splitnote{Strong, direct opening.
Sets scope immediately.}
\dasinline{Title needs updated to High Assurance Hybrid
Control Systems. Maybe removal of `formal'?}
guarantees of safe and correct behavior.}
% INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed
@ -17,7 +14,7 @@ between control objectives.
\oldt{But, reliance} \newt{This 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.\dasinline{Obvious but source required.} Autonomous
conventional plants.Autonomous
control systems \oldt{are needed that can} \newt{must} safely manage complex
operational sequences with the same assurance as human-operated systems, but
without constant supervision.
@ -34,7 +31,7 @@ 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.\splitnote{Nice parallel structure showing the gap.}
correctness.
% Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will
@ -46,21 +43,18 @@ identify conflicts and ambiguities in procedures before implementation.}
\newt{FRET structures requirements into scope, condition, component, timing,
and response elements, enabling realizability checking that identifies
conflicts and ambiguities in procedures before implementation.}
\dasinline{Had to read this twice.}
Second, we will synthesize discrete mode switching logic using reactive
synthesis \oldt{to generate deterministic automata that are provably correct
by construction.} \newt{to produce deterministic automata that are correct by
construction.}\dasinline{Also had to read this twice. A lot of
jargon. Check topic stress.}
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 \oldt{, and then employ
assume-guarantee contracts and barrier certificates to prove that mode
transitions occur safely and as defined by the deterministic automata.}
\newt{and verify safe mode transitions using barrier certificates and
reachability analysis.}\dasinline{I don't think I ever mention this phrase
again specifically. Might be a dogwhistle to other work unintentionally. Must
be careful.}
reachability analysis.}
This compositional approach enables local verification of continuous modes
without requiring global trajectory analysis across the entire hybrid system.
@ -68,7 +62,6 @@ without requiring global trajectory analysis across the entire hybrid system.
\newt{We will validate this methodology through hardware-in-the-loop testing
on an Emerson Ovation distributed control system, made possible through the
University of Pittsburgh Cyber Energy Center's industry partnership.}
\dasinline{Where did this come from? Needs context.}
% Pay-off
This approach \oldt{will demonstrate autonomous control can be used for}
@ -90,7 +83,7 @@ If this research is successful, we will be able to do the following:
expertise, reducing barriers to high-assurance control systems.}
\newt{This will reduce barriers to high-assurance control systems by
generating verified mode-switching controllers directly from regulatory
procedures.}\dasinline{This may not be true, and perhaps does not belong.}
procedures.}
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions.}
@ -114,8 +107,6 @@ If this research is successful, we will be able to do the following:
high-assurance autonomous controls on industrial platforms they already
use.} \newt{Without retraining costs or new equipment, control engineers
will be able to implement high-assurance autonomous controls on industrial
platforms they already use.}\dasinline{Flip the clauses. Put retraining
and new equipment before the comma, end with building HAHACs with control
hardware they already use. That's the more important part.}
platforms they already use.}
\end{enumerate}

79
2-state-of-the-art/state-of-art.tex
View File

@ -10,10 +10,7 @@ current formal methods approaches to reactor control systems.}
nuclear reactors are operated today. This section examines reactor operating
procedures, investigates limitations of human-based operation, and reviews
current formal methods approaches to reactor control
systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
state of the art of nuclear reactor control, blah, and blah, are discussed
in this section.''}
systems.}
\subsection{Current Reactor Procedures and Operation}
@ -29,9 +26,7 @@ Procedures (EOPs) for design-basis accidents and Severe Accident Management
Guidelines (SAMGs) for beyond-design-basis events. These procedures exist
because reactor operation requires deterministic responses to a wide range
of plant conditions, from routine power changes to catastrophic
failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
describing different types of procedures? WHO CARES? Need a sentence after
saying why we have these procedures.} These procedures must comply with 10
failures.}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 development relies
fundamentally on expert judgment and simulator validation rather than formal
@ -41,9 +36,7 @@ Procedures undergo technical evaluation, simulator validation testing, and
biennial review as part of operator requalification under 10 CFR
55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
\oldt{formal verification of key safety properties.} \newt{exhaustive
verification of key safety properties.}\dasinline{Does the audience know
what formal verification is at this point? Probably, but should say
differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
verification of key safety properties.}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.
@ -58,9 +51,7 @@ application, and even computer-based procedure systems lack the formal
guarantees that automated reasoning could provide.} \newt{Paper-based
procedures cannot ensure correct application, and even computer-based
procedure systems lack the guarantees that automated reasoning could
provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
sentence almost verbatim from the paragraph above. Either cut it from the
paragraph or from the LIMITATION box.}
provide.}
Nuclear plants operate with multiple control modes: automatic control, where
the reactor control system maintains target parameters through continuous
@ -88,11 +79,7 @@ actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
operators retain control of everything else: power level changes,
startup/shutdown sequences, mode transitions, and procedure
implementation.}\dasinline{After reading the next sentence, ``key safety''
can honestly just be a semicolon.}\dasinline{Not sure what the challenge
actually is as this paragraph is written. What's the
point?}\splitnote{This is the key insight — the hybrid nature is already
there, just not formally verified.}
implementation.}
\subsection{Human Factors in Nuclear Accidents}
@ -107,20 +94,17 @@ operator requires several years of training.} \newt{Nuclear plant staffing
requires at least two Reactor Operators (ROs) and one Senior Reactor
Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several
years of training and NRC licensing under 10 CFR Part
55~\cite{10CFR55}.}\dasinline{Why is this here? Should this be in broader
impacts about running out of ROs? As it is here I have no idea why this is
here.}
55~\cite{10CFR55}.}
The persistent role of human error in nuclear safety incidents---despite
decades of improvements in training and procedures---provides the most
compelling motivation for formal automated control with mathematical safety
guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
guarantees.Operators hold
legal authority under 10 CFR Part 55 to make critical
decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
decisions~\cite{10CFR55},including departing from normal
regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
\newt{This authority itself introduces risk. The Three Mile Island (TMI)
accident}\dasinline{Needs a connector here. Like ``But this can in and of
itself prime plants for an accident.'' Then continue.} demonstrated how a
accident}demonstrated how a
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
@ -129,9 +113,7 @@ responsibility for safe power plant operations on the licensee without
formal verification that operators can fulfill this responsibility does not
guarantee safety. This tension between operational flexibility and safety
assurance remains unresolved: the person responsible for reactor safety is
often the root cause of failures.\splitnote{``the person responsible for
reactor safety is often the root cause of failures'' — devastating summary.
Very effective.}
often the root cause of failures.
Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus
@ -144,16 +126,13 @@ 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.\splitnote{Strong empirical grounding. The Chinese plant data is a
nice addition — shows this isn't just a Western regulatory perspective.}
failure.
\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 a remediable part of
human-driven control.\splitnote{Well-stated. The ``four decades'' point
drives it home.}
human-driven control.
\subsection{Formal Methods}
\subsubsection{HARDENS}
@ -164,7 +143,7 @@ nuclear reactor control systems to date~\cite{Kiniry2024}.
HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear
control rooms rely on analog technologies from the
1950s--60s.\dasinline{Source?} This technology is obsolete compared to
1950s--60s.This technology is obsolete compared to
modern control systems and incurs significant risk and cost. The NRC
contracted Galois, a formal methods firm, to demonstrate that Model-Based
Systems Engineering and formal methods could design, verify, and implement a
@ -173,15 +152,12 @@ typical cost. The project delivered a Reactor Trip System (RTS)
implementation with full traceability from \oldt{NRC Request for Proposals
and IEEE standards through formal architecture specifications to verified
software.} \newt{regulatory requirements through formal architecture
specifications to verified software.}\dasinline{Wordsmith this to remove the
RFP and IEEE standards language. Should just say requirements.}
specifications to verified software.}
\oldt{HARDENS employed formal methods tools and techniques across the
verification hierarchy.} \newt{HARDENS employed formal methods tools at
every level of system development, from high-level requirements through
executable models to generated code.}\dasinline{Zero discussion about what
the verification hierarchy is. What is a specification or a requirement to
someone who hasn't heard of one before?} High-level specifications used
executable models to generated code.}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
@ -192,7 +168,7 @@ 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.\splitnote{Good technical depth on HARDENS toolchain.}
arise.
\oldt{Despite its accomplishments, HARDENS has a fundamental limitation
directly relevant to hybrid control synthesis: the project addressed only
@ -212,9 +188,7 @@ did not model or verify continuous reactor dynamics. Real reactor safety
depends on the interaction between continuous processes---temperature,
pressure, neutron flux---evolving in response to discrete control decisions.
HARDENS verified the discrete controller in isolation but not the
closed-loop hybrid system behavior.}\dasinline{Edit these to more clearly
separate the context from the limit. The limitation should be in the
limitation.}\splitnote{Clear articulation of the gap your work fills.}
closed-loop hybrid system behavior.}
\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
without continuous dynamics or hybrid system verification.} Verifying
@ -230,8 +204,7 @@ 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.''\dasinline{Check this quote. Absolutely damning for HARDENS if true
and hilarious Galois said this.} The project did not include deployment in
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, NRC licensing review, or human
@ -249,20 +222,19 @@ evidence.} \newt{The gap between formal verification and actual system
deployment remains wide: integration with legacy systems, long-term
reliability under harsh environments, human-system interaction, and
regulatory acceptance of formal methods as primary assurance
evidence.}\dasinline{Same as before. Separate limit from context better.}
evidence.}
\subsubsection{Sequent Calculus and Differential Dynamic Logic}
\oldt{There has been additional work to do verification of hybrid systems by
extending the temporal logics directly.} \newt{A separate line of work
extends temporal logics to verify hybrid systems
directly.}\dasinline{Need to introduce temporal logic and FRET here first.}
directly.}
The result has been the field of differential dynamic logic (dL). 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 \oldt{ivariant} \newt{invariant} being
enforced for the system.\splitfix{Typo: ``ivariant'' should be
``invariant''} The second operator, the diamond operator
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.
@ -280,8 +252,7 @@ proofs using dL is state space explosion and non-terminating solutions.
Approaches have been made to alleviate these issues for nuclear power
contexts using contract and decomposition based methods, \oldt{but are far
from a complete methodology to design systems with.} \newt{but do not yet
constitute a complete design methodology.}\splitpolish{``but are far from a
complete methodology to design systems with'' — awkward ending preposition.}
constitute 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.
@ -296,8 +267,4 @@ post-hoc analysis of existing systems, not for the constructive design of
autonomous controllers.} Current dL-based approaches verify systems that
have already been designed, requiring expert knowledge to construct proofs.
They have not been applied to the synthesis of new controllers from
operational requirements.\splitinline{Your comment here is spot-on. You
should add a LIMITATION box: \textit{Differential dynamic logic has been
used for post-hoc analysis of existing systems, not for the constructive
design of autonomous controllers.} This is exactly the gap you're filling —
you're doing synthesis, not just verification.}
operational requirements.

172
3-research-approach/approach.tex
View File

@ -27,24 +27,17 @@ control-theoretic verification, formalizing reactor operations using the
framework of hybrid automata.} \newt{HAHACS bridges the gap between discrete
and continuous verification by composing formal methods from computer science
with control-theoretic verification, formalizing reactor operations using the
framework of hybrid automata.}\dasinline{Honestly just get rid of this whole
paragraph.}
framework of hybrid automata.}
The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the
\oldt{governing} \newt{active}\dasinline{Governing what? People? Whos in
Whoville?} vector field, creating discontinuities in the system's behavior.
\oldt{governing} \newt{active}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.\splitpolish{Missing space before ``Our}\dasinline{This whole
paragraph should just be after the definition of the tuple. First sentence
can stay, but all this explanation should move.} Our methodology addresses
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.\splitsuggest{Compositional verification
claim needs citation. See assume-guarantee literature (Henzinger, Alur).
None of the NEEDS\_REVIEWED papers directly prove this composition is sound
for your specific approach.} This two-layer approach mirrors the structure of
about the complete hybrid system.This two-layer approach mirrors the structure of
reactor operations themselves: discrete supervisory logic determines which
control mode is active, while continuous controllers govern plant behavior
within each mode.
@ -91,12 +84,10 @@ control system is satisfied by its actual
implementation.\oldt{}\newt{ In concrete terms, this means producing a
discrete automaton whose transitions are provably correct, continuous
controllers whose behavior is verified against transition requirements, and
formal evidence linking the two.}\dasinline{Add a sentence explaining what
this actually means.} This approach is tractable now because the
formal evidence linking the two.}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.\splitnote{This is your key insight --- the novelty is compositional,
not component-level.} By defining entry, exit, and safety conditions at the
them.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 rather than on the full
@ -153,8 +144,7 @@ operations.
\node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};
\end{tikzpicture}
\dasinline{Figure dynamics show control inputs u, but these systems are
autonomous. What's up with that?}
\caption{Simplified hybrid automaton for reactor startup. Each discrete
state $q_i$ has associated continuous dynamics $f_i$. Guard conditions
on transitions (e.g., $T_{avg} > T_{min}$) are predicates over
@ -186,14 +176,12 @@ chemistry. Tactical control has already been somewhat automated in nuclear
power plants today, and is generally considered ``automatic control'' when
autonomous. These controls are almost always continuous systems with a direct
impact on the physical state of the
plant.\dasinline{This should be written to be clear this isn't an exhaustive
list.} Tactical control objectives include\oldt{}\newt{, but are not limited
plant.Tactical control objectives include\oldt{}\newt{, but are not limited
to,} maintaining pressurizer level, maintaining core temperature, or
adjusting reactivity with a chemical shim.
The level of control \oldt{linking} \newt{linking
these two extremes of}\dasinline{Linking of these two extremes. Don't even
say control here.} \oldt{these two extremes is the} operational control
these two extremes of}\oldt{these two extremes is the} operational control
scope. Operational control is the primary responsibility of human operators
today. Operational control takes the current strategic objective and
implements tactical control objectives to drive the plant towards strategic
@ -202,7 +190,7 @@ goal may be to perform refueling at a certain time, while the tactical level
of the plant is currently focused on maintaining a certain core temperature.
The operational level issues the shutdown procedure, using several smaller
tactical goals along the way to achieve this \oldt{objective.}
\newt{strategic objective.}\dasinline{This STRATEGIC objective.} Thus, the
\newt{strategic objective.}Thus, the
combination of the operational and tactical levels fundamentally forms a
hybrid controller. The tactical level is the continuous evolution of the
plant according to the control input and control law, while the operational
@ -211,7 +199,6 @@ law to apply.
%Say something about autonomous control systems near here?
\begin{figure}
\centering
\begin{tikzpicture}[scale=0.8]
@ -252,7 +239,6 @@ law to apply.
\label{fig:strat_op_tact}
\end{figure}
\oldt{This operational control level is the main reason for the requirement
of human operators in nuclear control today. The hybrid nature of this
control system makes it difficult to prove that a controller will perform
@ -264,17 +250,12 @@ nature of this control problem is the reason human operators remain
essential. Because unified infrastructure for building and verifying hybrid
systems does not currently exist, the operational layer has relied on human
general intelligence to manage the interaction between discrete decisions and
continuous dynamics.}\dasinline{This operational control level is the main
reason\ldots Add a sentence why. Because the hybrid dynamics have previously
been `unknowable', it's been assumed that a human operator could figure it
out on the fly. Or similar.} \oldt{But these operators use prescriptive
continuous dynamics.}\oldt{But these operators use prescriptive
operating manuals to perform their control with strict procedures on what
control to implement at a given time.} \newt{However, human factors research
has sought to minimize the need for general human reasoning by creating
extremely prescriptive operating manuals with strict procedures dictating
what control to implement at a given time.}\dasinline{Say but human factors
has been seeking to eliminate the need for general human behavior by creating
extremely prescriptive operating manuals. This is our leverage.} These
what control to implement at a given time.}These
procedures are the key to the operational control scope.
The method of constructing a HAHACS in this proposal leverages two key
@ -289,7 +270,7 @@ sources including regulatory mandates, design basis analyses, and operating
procedures. The challenge is formalizing these requirements with sufficient
precision that they can serve as the foundation for autonomous control system
synthesis and verification. We can build these requirements using temporal
logic.\dasinline{We definitely need some temporal logic juice in the SOTA.}
logic.
Temporal logic is a powerful set of semantics for building systems with
complex but deterministic behavior. Temporal logic extends classical
@ -317,9 +298,7 @@ safe operating boundaries has already been done by generations of nuclear
engineers.
Linear temporal logic (LTL) is particularly well-suited
for\dasinline{Some of this could be in SOTA vs here. Examples in nuclear
space should be in RA, but the general idea of temporal logic and where it
came from in the context of computers could be in SOTA.} specifying reactive
forspecifying reactive
systems. LTL formulas are built from atomic propositions (our discrete
predicates) using Boolean connectives and temporal operators. The key
temporal operators are:
@ -335,10 +314,6 @@ enters an unsafe configuration''), liveness properties (``the system
eventually reaches operating temperature''), and response properties (``if
coolant pressure drops, the system initiates shutdown within bounded
time'').%
\splitsuggest{CAUTION: Katis 2022 (Table 1, p.2) notes FRET realizability
checking does NOT support liveness properties. Your ``eventually reaches
operating temperature'' example may need alternative verification approach.}
To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool,
@ -359,11 +334,7 @@ First, it allows us to draw a direct link from design documentation to
digital system implementation. Second, it clearly demonstrates where natural
language documents are insufficient. These procedures may still be used by
human operators, so any room for interpretation is a weakness that must be
addressed.\splitnote{FRET has been validated: Katis 2022 (pp.1-2, Section
0.3) demonstrates FRET's FRETish template system with 160 distinct patterns;
Pressburger 2023 (pp.17, Section 1) shows successful application to
Lift+Cruise case study with 53 requirements formalized and iteratively
refined---strong evidence your approach is feasible.}
addressed.
(Some examples of where FRET has been used and why it will be successful
here)
@ -396,12 +367,7 @@ $\varphi$. If such a strategy exists, the specification is called
correct-by-construction controller or reports that no such controller can
exist. This realizability check is itself valuable: an unrealizable
specification indicates conflicting or impossible requirements in the
original procedures.\splitnote{Realizability is proven valuable: Katis 2022
(pp.7-10) shows FRET diagnosis found 8 minimal unrealizable cores in
infusion pump case; Pressburger 2023 (pp.19-21) shows unrealizability
revealed under-specification (missing stay requirements in LPC aircraft),
driving iterative refinement---this suggests your synthesis approach will
help engineers catch requirement errors early.}
original procedures.
The main advantage of reactive synthesis is that at no point in the
production of the discrete automaton is human engineering of the
@ -425,30 +391,12 @@ originating requirement, providing a clear liability and justification chain.
Second, by defining system behavior in temporal logic and synthesizing the
controller using deterministic algorithms, discrete control decisions become
provably consistent with operating
procedures.}\dasinline{Some goofy issue-point stuff going on in this
paragraph.}\splitnote{Strix (Luttenberger 2020, pp.1-3) is a practical
reactive synthesis tool winning SYNTCOMP competitions; handles LTL specs for
systems with large state spaces. Strix uses parity games and
forward-explorative construction (pp.7-8) to
scale---recommend as your synthesis backend for nuclear
procedures.}\splitsuggest{Consider discussing scalability: Strix handles
large alphabets better (v19.07 update, p.30), but still struggles with very
large specifications. Document expected spec size for SmAHTR startup
procedures to set expectations.}
procedures.}
(Talk about how one would go from a discrete automaton to actual
code)\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable
LTL subset for synthesis: wins SYNTCOMP competitions (p.13). Luttenberger
2020 (Strix tool, pp.1-3) handles full LTL via parity games, achieving
4000+ state specs efficiently (p.5). Your nuclear procedures should fit
GR(1) since they're reactive (environment inputs = plant state, outputs =
mode transitions). This suggests synthesis will be practical for SmAHTR
scale.}
code)
(Examples of reactive synthesis in the wild)\splitfix{Need to verify your
LTL specs fit GR(1) or full LTL needed---if full LTL required, computational
cost grows but Strix may handle it (confirm scalability claim with specific
spec size estimates for startup/shutdown procedures).}
(Examples of reactive synthesis in the wild)
%%% NOTES (Section 3):
% - Mention computational complexity of synthesis (doubly exponential worst
@ -470,7 +418,7 @@ 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 of this methodology with respect to continuous controller
design. This work \oldt{verifies} \newt{will
verify}\dasinline{Verb tense: ``will verify''.} continuous controllers; it
verify}continuous controllers; it
does not synthesize them. The distinction parallels model checking in
software verification: model checking does not tell engineers how to write
correct software, but it verifies whether a given implementation satisfies
@ -509,23 +457,14 @@ continuous controller design:
These are derived from invariants \(Inv\).
\end{enumerate}
These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control.\dasinline{This SOUNDS like
assume-guarantee stuff. Maybe make that connection formal and cite it?} The
precise objectives for continuous control.The
continuous controller for mode $q_i$ must drive the system from any state in
$\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while
remaining within
$\mathcal{X}_{safe,i}$.\splitnote{This compositional approach is formalized
in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential
cuts reduce state-space (DC rule, p.20), then system proof composes via
differential invariants (DI rule, pp.22-24). Kapuria proves SmAHTR safety by
verifying 6 components in isolation then system---your three-mode structure
maps perfectly to this decomposition, reducing verification complexity from
curse of dimensionality.}
$\mathcal{X}_{safe,i}$.
We classify continuous controllers into three types based on their
objectives: transitory, stabilizing, and expulsory.\splitnote{This
three-mode taxonomy is elegant --- maps verification tools to control
objectives cleanly.} Each type has distinct verification requirements that
objectives: transitory, stabilizing, and expulsory.Each type has distinct verification requirements that
determine which formal methods tools are appropriate.
%%% NOTES (Section 4):
@ -589,18 +528,7 @@ polyhedral or ellipsoidal reachability computations. Nonlinear systems
require more conservative over-approximations using techniques such as Taylor
models or polynomial zonotopes. For this work, we will select tools
appropriate to the fidelity of the reactor models
available.\splitnote{Your toolset is well-justified: SpaceEx (Frehse 2011,
pp.3-6) handles hybrid automata via support functions; Flow* (Chen 2013)
uses Taylor models for nonlinear dynamics; JuliaReach (Bogomolov 2019,
pp.1-2) offers flexible set representations (zonotopes, boxes). Kapuria 2025
(pp.11-12, Section 2.2) uses Flow* successfully for SmAHTR reachability with
reactor models showing state-space constraints (e.g., temp
673--677\textdegree{}C, Figures 6, 16--20). This validates your tool choices
for nuclear systems.}\splitnote{Critical finding from Kapuria 2025:
decomposition-based verification (pp.17-24, Section 2.4) proves component
safety in isolation using reachability, THEN composes to system proof via
differential invariants---your three-mode taxonomy maps cleanly to component
verification, reducing complexity from monolithic analysis.}
available.
%%% NOTES (Section 4.1):
% - Add timing constraints discussion: what if the transition takes too long?
@ -616,8 +544,7 @@ verification, reducing complexity from monolithic analysis.}
Stabilizing modes are continuous controllers with an objective of maintaining
a particular discrete state indefinitely. Rather than driving the system
toward an exit \oldt{condition,} \newt{state,}\dasinline{``mode'' ---
``condition'' here sounds goofy.} they keep the system within a safe
toward an exit \oldt{condition,} \newt{state,}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 suitable approach to validation. Instead, we
@ -632,8 +559,7 @@ safe set. The idea is analogous to Lyapunov functions for stability: rather
than computing trajectories explicitly, we find a certificate function whose
properties guarantee the desired behavior. For a safe set $\mathcal{C} =
\{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$,
the\dasinline{Should clarify that the safe set C is not the entire
continuous region. It's just the boundary of the region.} barrier certificate
thebarrier certificate
condition requires:
\[
\forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x))
@ -663,16 +589,7 @@ result satisfies the required invariants. This also allows for the checking
of control modes with different models than they are designed for. For
example, a lower fidelity model can be used for controller design, but a
higher fidelity model can be used for the actual validation of that
stabilizing controller.\splitnote{SOS methods proven effective:
Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier certificate
optimization via SOS constraints---tool integrates with MATLAB. Borrmann
2015 (pp.4-8) demonstrates control barrier certificates for multi-agent
systems, showing how discrete boundaries (mode guards) can inform barrier
design. Your claim that discrete specs eliminate barrier search is novel and
well-supported by these foundations.}\splitnote{Hauswirth 2024 (pp.1-3)
shows optimization-based robust feedback controllers can serve as
alternative verification method---suggests barrier certificates +
reachability provide complementary guarantees for your stabilizing modes.}
stabilizing controller.
%%% NOTES (Section 4.2):
% - Clarify relationship between barrier certificates and Lyapunov stability
@ -699,8 +616,7 @@ We know our controller cannot be incorrect for the nominal plant model, so
if an invariant is violated, we know the plant dynamics have
changed. \oldt{The HAHACS can identify that a fault occurred because a
discrete boundary condition was violated by the continuous physical
controller.} \newt{}\dasinline{This says the same thing as the sentence
right before it.} This is a direct consequence of having verified the
controller.} \newt{}This is a direct consequence of having verified the
nominal continuous control modes: unexpected behavior implies off-nominal
conditions.
@ -714,12 +630,7 @@ modes:
\dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure}
\]
where $\Theta_{failure}$ captures the range of possible degraded plant%
\splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address
reachability with parametric uncertainty for failure mode analysis. SpaceEx
handles nondeterministic inputs (Frehse 2011, p.4) but not parametric plant
uncertainty. Consider citing CORA (parametric reachability) or robust CBF
literature. This may require additional references beyond current
collection.}
behaviors identified through failure mode and effects analysis (FMEA) or
traditional safety analysis.
@ -741,18 +652,7 @@ accident analysis identify credible failure scenarios and their effects on
plant dynamics. The expulsory mode must handle the worst-case dynamics within
this envelope. This is where conservative controller design is appropriate as
safety margins will matter more than performance during emergency
shutdown.\splitnote{Parametric uncertainty approach validated: Kapuria 2025
(pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with
uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine
flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on
$\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory
mode approach is sound for nuclear failures. Shows safety can be proven even
when controller deviates from nominal (pp.85-107, UCA 1
analysis).}\splitsuggest{Kapuria 2025 reveals practical challenge:
determining $\Theta_{\text{failure}}$ bounds is non-trivial. Recommend
documenting failure mode selection process (FMEA $\rightarrow$ parametric
bounds) to make expulsory mode design repeatable for other reactor
sequences.}
shutdown.
%%% NOTES (Section 4.3):
% - Discuss sensor failures vs actual plant failures
@ -779,7 +679,7 @@ synthesis will be compiled to run on Ovation controllers, with verification
that the implemented behavior matches the synthesized specification exactly.
For the continuous dynamics, we will use a small modular reactor
simulation.\dasinline{Are we REALLY going to do this? Maybe not.} The SmAHTR
simulation.The SmAHTR
(Small modular Advanced High Temperature Reactor) model provides a relevant
testbed for startup and shutdown procedures. The ARCADE (Advanced Reactor
Control Architecture Development Environment) interface will establish
@ -801,15 +701,7 @@ of how our research outcomes can align best with customer needs.}
system experts at Emerson ensures that implementation details of the Ovation
platform are handled correctly. Direct industry collaboration provides an
immediate pathway for technology transfer and alignment with practical
deployment requirements.}\splitnote{Kapuria 2025 validates hybrid control on
SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved
safe PHX maintenance scenario, then Simulink demo confirmed (pp.70-72). This
two-tier approach (formal proof + simulation validation) strengthens your
Emerson demo plan for credibility.}\splitsuggest{Consider documenting
integration points: ARCADE interface must guarantee formal synthesis outputs
map 1:1 to Ovation code. Pressburger 2023 (pp.22-23) notes manual
integration risks---automate code generation from formal specs to minimize
this gap.}
deployment requirements.}
%%% NOTES (Section 5):
% - Get specific details on ARCADE interface from Emerson collaboration

12
4-metrics-of-success/metrics.tex
View File

@ -4,8 +4,7 @@ This research will be measured by advancement through Technology Readiness
Levels, progressing from fundamental concepts to validated prototype
demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
system components operate successfully in a relevant laboratory
environment.\splitnote{TRL as primary metric is smart — speaks industry
language.}
environment.
This section explains why TRL advancement provides the most appropriate
success metric and defines the specific criteria required to achieve TRL 5.
@ -19,8 +18,7 @@ simultaneously.} \newt{TRLs measure the gap between academic
proof-of-concept and practical deployment, which is precisely what this work
aims to bridge. Academic metrics alone cannot capture practical feasibility,
and empirical metrics alone cannot demonstrate theoretical rigor. TRLs
measure both simultaneously.}\dasinline{Chop. No likey.}\splitnote{Good
framing — explains why other metrics are insufficient.} Advancing from TRL 3
measure both simultaneously.}Advancing from TRL 3
to TRL 5 requires maintaining theoretical rigor while progressively
demonstrating practical feasibility. Formal verification must remain valid as
the system moves from individual components to integrated hardware testing.
@ -80,8 +78,7 @@ activate SCRAM procedures as specified. Graded responses to minor
disturbances are outside this work's scope\oldt{.}\newt{, as they require
runtime optimization under uncertainty that extends beyond the
correct-by-construction verification framework presented
here.}\splitsuggest{Consider noting why graded responses are out of scope —
is it time, complexity, or scope creep? Brief justification helps.} Formal
here.}Formal
verification results must remain valid, with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable
@ -99,5 +96,4 @@ operating on industrial control hardware through hardware-in-the-loop
testing in a relevant laboratory environment. This establishes both
theoretical validity and practical feasibility, proving that the methodology
produces verified controllers and that implementation is achievable with
current technology.\splitnote{Clear success criteria. Committee will know
exactly what ``done'' looks like.}
current technology.

8
5-risks-and-contingencies/risks.tex
View File

@ -2,8 +2,7 @@
This research relies on several critical assumptions that, if invalidated,
would require scope adjustment or methodological
revision.\splitnote{Honest acknowledgment of risks with clear contingencies
— committee will appreciate this.} The primary risks to successful
revision.The primary risks to successful
completion fall into four categories: computational tractability of synthesis
and verification, complexity of the discrete-continuous interface,
completeness of procedure formalization, and hardware-in-the-loop integration
@ -32,8 +31,7 @@ would suggest complete procedures are intractable. Generated automata
containing more than 1,000 discrete states would indicate the discrete state
space is too large for efficient verification. Specifications flagged as
unrealizable by \oldt{FRET or Strix} \newt{realizability checking
tools}\dasinline{Strix may not be the reactive synth tool anymore. Be more
general.} would reveal fundamental conflicts in the formalized procedures.
tools}would reveal fundamental conflicts in the formalized procedures.
Reachability analysis failing to converge within reasonable time bounds would
show that continuous mode verification cannot be completed with available
computational resources.
@ -60,7 +58,7 @@ requires reasoning about differential equations and reachable sets.
boolean abstraction, making synthesis intractable.} \newt{Some guard
conditions may require complex nonlinear predicates that cannot be cleanly
expressed as boolean combinations of simple threshold checks, making
synthesis intractable.}\dasinline{What does this mean?} Continuous safety
synthesis intractable.}Continuous safety
regions that cannot be expressed as conjunctions of verifiable constraints
would similarly create insurmountable verification challenges. The risk
extends beyond static interface definition to dynamic behavior across

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

@ -24,8 +24,7 @@ translating to \$21--28 billion annually for projected datacenter demand.}
\newt{[DANE: Verify these figures are current. Check EIA Annual Energy
Outlook 2024/2025 for updated LCOE projections. The \$88.24/MWh,
\$16.15/MWh O\&M, and datacenter demand projections may have newer
sources.]}\dasinline{Check all of this math and update if newer sources
exist.}
sources.]}
This research directly addresses the multi-billion-dollar O\&M cost challenge
through high-assurance autonomous control. Current nuclear operations require
@ -76,6 +75,5 @@ control, aerospace systems, and autonomous transportation, where similar
economic and safety considerations favor increased autonomy with provable
correctness guarantees. Demonstrating this approach in nuclear power---one of
the most regulated and safety-critical
domains\splitnote{``If it works here, it works anywhere — strong closing
argument.}---will establish both the technical feasibility and regulatory
domains---will establish both the technical feasibility and regulatory
pathway for broader adoption across critical infrastructure.

2
8-schedule/schedule.tex
View File

@ -93,4 +93,4 @@ methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
implementability on industrial hardware. This milestone delivers a conference
paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
experimental validation. M6 (Month 24) completes the dissertation documenting
the entire methodology, experimental results, and research contributions.\splitnote{Clear timeline with publication targets — shows you have a plan.}
the entire methodology, experimental results, and research contributions.