\section{Research Approach} % ============================================================================ % STRUCTURE (maps to Thesis.RA tasks): % 1. Introduction + Hybrid Systems Definition (Task 34) % 2. System Requirements and Specifications (Task 35) % 3. Discrete Controller Synthesis (Task 36) % 4. Continuous Controllers Overview (Task 37) % 4.1 Transitory Modes (Task 38) % 4.2 Stabilizing Modes (Task 39) % 4.3 Expulsory Modes (Task 40) % 5. Industrial Implementation (Task 41) % ============================================================================ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. Despite consuming enormous resources, neither method 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 hybrid automata. Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode. Building a high-assurance hybrid autonomous control system (HAHACS) requires a mathematical description of the system. This work draws on automata theory, temporal logic, and control theory. A hybrid system is a dynamical system with both continuous and discrete states. This proposal discusses continuous autonomous hybrid systems specifically—systems with no external input where continuous states do not change instantaneously when discrete states change. These continuous states are physical quantities that remain Lipschitz continuous. We follow the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience: \begin{equation} H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv) \end{equation} where: \begin{itemize} \item $\mathcal{Q}$: the set of discrete states (modes) of the system \item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space \item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow \mathbb{R}^n$: vector fields defining the continuous dynamics for each discrete mode $q_i$ \item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial states \item $\mathcal{G}$: guard conditions that define when discrete state transitions may occur \item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$: the discrete state transition function \item $\mathcal{R}$: reset maps that define any instantaneous changes to continuous state upon discrete transitions \item $Inv$: safety invariants on the continuous dynamics \end{itemize} Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior. \textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty. First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation. \textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle. \begin{figure} \centering \begin{tikzpicture}[ state/.style={ circle, draw=black, thick, minimum size=2.2cm, fill=blue!10, align=center, font=\small }, trans/.style={ ->, thick, >=stealth }, guard/.style={ font=\scriptsize, align=center, fill=white, inner sep=2pt }, dynamics/.style={ font=\scriptsize\itshape, text=blue!70!black } ] % States \node[state] (q0) at (0,0) {$q_0$\\Cold\\Shutdown}; \node[state] (q1) at (5,0) {$q_1$\\Heatup}; \node[state] (q2) at (10,0) {$q_2$\\Power\\Operation}; \node[state, fill=red!15] (q3) at (5,-3.5) {$q_3$\\SCRAM}; % Normal transitions \draw[trans] (q0) -- node[guard, above] {$T_{avg} > T_{min}$} (q1); \draw[trans] (q1) -- node[guard, above] {$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2); % Fault transitions \draw[trans, red!70!black] (q1) -- node[guard, left, text=red!70!black] {$\neg Inv_1$} (q3); \draw[trans, red!70!black] (q2) to[bend left=20] node[guard, right, text=red!70!black] {$\neg Inv_2$} (q3); % Recovery transition \draw[trans, dashed] (q3) to[bend left=30] node[guard, below] {Manual reset} (q0); % Self-loops indicating staying in mode \draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$} (q2); % Dynamics labels below states \node[dynamics] at (0,-1.4) {$\dot{x} = f_0(x)$}; \node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x,u)$}; \node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x,u)$}; \node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$}; \end{tikzpicture} \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 continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.} \label{fig:hybrid_automaton} \end{figure} %%% NOTES (Section 1): % - May want to clarify the "no external input" claim with a footnote about % strategic inputs (e.g., remote start/stop commands) % - The reset map R is often identity for physical systems; clarify if needed % ---------------------------------------------------------------------------- % 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS % ---------------------------------------------------------------------------- \subsection{System Requirements, Specifications, and Discrete Controllers} The eight-tuple hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, 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 long, often spanning months or years. The lowest level is the tactical level: the individual control of pumps, turbines, and chemistry. Nuclear power plants today have already automated tactical control somewhat, generally considered ``automatic control'' when autonomous. These controls are almost always continuous systems with a direct impact on the physical state of the plant. Tactical control objectives include maintaining pressurizer level, maintaining core temperature, or adjusting reactivity with a chemical shim. The operational control scope links these two extremes and represents the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant toward strategic goals, bridging high-level and low-level goals. Consider an example: a strategic 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 objective. This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous evolution of the plant according to the control input and control law, while the operational level represents discrete state evolution that determines which tactical control law to apply. We target this operational level for autonomous control. \begin{figure} \centering \begin{tikzpicture}[scale=0.8] % Pyramid layers \fill[blue!30!white] (0,4) -- (2,4) -- (1,5.) -- cycle; \fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4) -- cycle; \fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5) -- cycle; % Labels inside pyramid \node[font=\small\bfseries] at (1,4.5) {Strategic}; \node[font=\small\bfseries] at (1,3.1) {Operational}; \node[font=\small\bfseries] at (1,1.6) {Tactical}; % Descriptions to the right \node[anchor=west, font=\small, text width=8cm] at (5.5,4.6) {\textit{Long-term planning:} maintenance scheduling, capacity planning, economic dispatch}; \node[anchor=west, font=\small, text width=8cm] at (5.5,3.1) {\textit{Discrete decisions:} startup/shutdown sequences, power level changes, mode transitions}; \node[anchor=west, font=\small, text width=8cm] at (5.5,1.6) {\textit{Continuous control:} temperature regulation, pressure control, load following}; % Bracket showing HAHACS scope (simple line with text) \draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) -- cycle; \node[font=\small, align=center, rotate=90] at (-4.2,2.5) {HAHACS scope}; \end{tikzpicture} \caption{Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.} \label{fig:strat_op_tact} \end{figure} This operational control level is the main reason human operators are required in nuclear control today. The hybrid nature of this control system makes it difficult to prove a controller will perform according to strategic requirements; unified infrastructure for building and verifying hybrid systems does not currently exist. Humans fill this layer because their general intelligence provides a safe way to manage the hybrid nature of the system. These operators use prescriptive operating manuals to perform their control with strict procedures on what control to implement at a given time. These procedures are the key to the operational control scope. Constructing a HAHACS leverages two key observations about current practice. First, operational scope control is effectively discrete control. Second, operating procedures describe the rules for implementing this control before implementation. We must completely describe a HAHACS's intended behavior before constructing it. The behavior of any control system originates in requirements: statements about what the system must do, must not do, and under what conditions. For nuclear systems, these requirements derive from multiple 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. Temporal logic provides powerful semantics for building systems with complex but deterministic behavior. It extends classical propositional logic with operators that express properties over time. Using temporal logic, we can relate discrete control modes to one another and define all the requirements of a HAHACS. The guard conditions $\mathcal{G}$ are defined by determining boundary conditions between discrete states and specifying their behavior. Continuous mode invariants can also be expressed as temporal logic statements. These specifications form the basis of any proofs about a HAHACS and constitute the fundamental truth statements about what the behavior of the system is designed to be. Discrete mode transitions include predicates—Boolean functions over the continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true}, \text{false}\}$. These predicates formalize conditions like ``coolant temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.'' We do not impose this discrete abstraction artificially. Operating procedures for nuclear systems already define go/no-go conditions as discrete predicates. Design basis safety analysis determined these thresholds; decades of operational experience have validated them. Our methodology assumes this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations of nuclear engineers have already done the hard work of defining safe operating boundaries. Linear temporal logic (LTL) is particularly well-suited for specifying reactive systems. LTL formulas are built from atomic propositions (our discrete predicates) using Boolean connectives and temporal operators. The key temporal operators are: \begin{itemize} \item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state \item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states \item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state \item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes true \end{itemize} These operators allow us to express safety properties (``the reactor never 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''). We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current workforce. A key feature of FRET is the ability to start with logically imprecise statements and consecutively refine them into well-posed specifications. We can use this to our advantage by directly importing operating procedures and design requirements into FRET in natural language, then iteratively refining them into specifications for a HAHACS. This has two distinct benefits. 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. (Some examples of where FRET has been used and why it will be successful here) %%% NOTES (Section 2): % - Add concrete FRET example showing requirement → FRETish → LTL % - Discuss hysteresis and how to prevent mode chattering near boundaries % - Address sensor noise and measurement uncertainty in threshold definitions % - Consider numerical precision issues when creating discrete automata % ---------------------------------------------------------------------------- % 3. DISCRETE CONTROLLER SYNTHESIS % ---------------------------------------------------------------------------- \subsection{Discrete Controller Synthesis} With system requirements defined as temporal logic specifications, we now build the discrete control system through reactive synthesis. Reactive synthesis automates the creation of reactive programs from temporal logic specifications. A reactive program takes an input for a given state and produces an output. Our systems fit this model: the current discrete state and status of guard conditions form the input; the next discrete state forms the output. Reactive synthesis solves a fundamental problem: given an LTL formula $\varphi$ that specifies desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is called \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller can exist. This realizability check provides immediate value: an unrealizable specification indicates conflicting or impossible requirements in the original procedures, catching errors before implementation. Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. This shift has two critical implications. First, it provides complete traceability. The reasons the controller changes between modes trace back through specifications to requirements, establishing clear liability and justification for system behavior. Second, it replaces probabilistic human judgment with deterministic guarantees. Human operators cannot eliminate error from discrete control decisions; humans are intrinsically fallible. By defining system behavior using temporal logics and synthesizing the controller using deterministic algorithms, strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors. (Talk about how one would go from a discrete automaton to actual code) (Examples of reactive synthesis in the wild) %%% NOTES (Section 3): % - Mention computational complexity of synthesis (doubly exponential worst case) % - Discuss how specification structure affects synthesis tractability % - Reference GR(1) fragment as a tractable subset commonly used in practice % - May want to include an example automaton figure % ---------------------------------------------------------------------------- % 4. CONTINUOUS CONTROLLERS % ---------------------------------------------------------------------------- \subsection{Continuous Control Modes} Reactive synthesis produces a provably correct discrete controller from operating procedures. This discrete controller determines when to switch between modes—but hybrid control requires more. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly. This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification approaches matched to their control objectives. This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers can design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. The operational control scope defines go/no-go decisions that determine what kind of continuous control to implement. The entry or exit conditions of a discrete state are the guard conditions $\mathcal{G}$ that define the boundaries for each continuous controller's allowed state-space region. These continuous controllers all share a common state space, but each individual continuous control mode operates within its own partition—defined by the discrete state $q_i$ and the associated guards. This partitioning of the continuous state space among several discrete vector fields has traditionally posed a difficult problem for validation and verification. The discontinuity of the vector fields at discrete state interfaces makes reachability analysis computationally expensive, and analytic solutions often become intractable \cite{MANYUS THESIS}. We circumvent these issues by designing our hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}. Each discrete mode $q_i$ provides three key pieces of information for continuous controller design: \begin{enumerate} \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, the set of possible initial states when entering this mode \item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$, the target states that trigger transition to the next mode, or is the region in the state space a stabilizing mode remains within. \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$, the envelope of safe states during operation in this mode. These are derived from invariants \(Inv\). \end{enumerate} These sets come directly from the discrete controller synthesis and define 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}$. We classify continuous controllers into three types based on their objectives: transitory, stabilizing, and expulsory. Each type has distinct verification requirements that determine which formal methods tools are appropriate. The following subsections detail each mode type and its verification approach. %%% NOTES (Section 4): % - Add figure showing the relationship between entry/exit/safety sets % - Discuss how standard control techniques (LQR, MPC, PID) fit into this framework % - Mention assume-guarantee reasoning for compositional verification % ---------------------------------------------------------------------------- % 4.1 TRANSITORY MODES % ---------------------------------------------------------------------------- \subsubsection{Transitory Modes} Transitory modes move the plant from one discrete operating condition to another. Their purpose is to execute transitions: start from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers. The control objective for a transitory mode can be stated formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy: \[ \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe} \] That is, from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region. Reachability analysis provides the natural verification tool for transitory modes. Reachability analysis computes the set of all states reachable from a given initial set under the system dynamics. For a transitory mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions: \begin{enumerate} \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the mode achieves its objective) \item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is maintained throughout the transition) \end{enumerate} Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states reachable within time horizon $T$: \[ \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe} \land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset \] The discrete controller defines clear boundaries in continuous state space, making the verification problem for each transitory mode well-posed. The possible initial conditions, target conditions, and safety envelope are all known. The verification task then confirms that the candidate continuous controller achieves the objective from all possible starting points. Several tools exist for computing reachable sets of hybrid systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool depends on the structure of the continuous dynamics. Linear systems admit efficient 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. %%% NOTES (Section 4.1): % - Add timing constraints discussion: what if the transition takes too long? % - Consider timed reachability for systems with deadline requirements % - Mention that the Mealy machine perspective unifies this: continuous system % IS the transition, entry/exit conditions are the discrete states % ---------------------------------------------------------------------------- % 4.2 STABILIZING MODES % ---------------------------------------------------------------------------- \subsubsection{Stabilizing Modes} Transitory modes drive the system toward exit conditions. Stabilizing modes, in contrast, maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. The different control objective requires a different verification approach: reachability analysis answers "can the system reach a target?" while stabilizing modes must prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool. Barrier certificates analyze the dynamics of the system to determine whether flux across a given boundary exists. They evaluate whether any trajectory leaves a given boundary. This definition exactly matches what defines the validity of a stabilizing continuous control mode. Formally, a barrier certificate (or control barrier function) is a scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe set. The idea parallels 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 barrier certificate condition requires: \[ \forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \geq 0 \] This condition states that on the boundary of the safe set (where $B(x) = 0$), the time derivative of $B$ is non-negative. Geometrically, this means the vector field points inward or tangent to the boundary, never outward. If this condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave. Because the design of the discrete controller defines careful boundaries in continuous state space, the barrier is known prior to designing the continuous controller. This eliminates the search for an appropriate barrier and minimizes complication in validating stabilizing continuous control modes. The discrete specifications tell us what region must be invariant; the barrier certificate confirms that the candidate controller achieves this invariance. Finding barrier certificates can be formulated as a sum-of-squares (SOS) optimization problem for polynomial systems, or solved using satisfiability modulo theories (SMT) solvers for broader classes of dynamics. The key advantage is that the verification is independent of how the controller was designed. Standard control techniques can be used to build continuous controllers, and barrier certificates provide a separate check that the 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. %%% NOTES (Section 4.2): % - Clarify relationship between barrier certificates and Lyapunov stability % - Discuss what happens at mode boundaries: barrier for this mode vs guard % for transition % - Mention tools: SOSTOOLS, dReal, barrier function synthesis methods % ---------------------------------------------------------------------------- % 4.3 EXPULSORY MODES % ---------------------------------------------------------------------------- \subsubsection{Expulsory Modes} Transitory and stabilizing modes handle nominal operations; expulsory modes handle off-nominal conditions. When the plant deviates from expected behavior, expulsory modes take over to ensure safety. These continuous controllers prioritize robustness over 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 controlled depressurization procedures. Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions. The mathematical formulation for expulsory mode verification differs from transitory modes in two key ways. First, the entry conditions may be the entire state space (or a large, conservatively bounded region) rather than a well-defined entry set. The failure may occur at any point during operation. Second, the dynamics include parametric uncertainty representing failure modes: \[ \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure} \] where $\Theta_{failure}$ captures the range of possible degraded plant behaviors identified through failure mode and effects analysis (FMEA) or traditional safety analysis. We verify expulsory modes using reachability analysis with parametric uncertainty. The verification condition requires that for all parameter values within the uncertainty set, trajectories from the expanded entry region reach the safe shutdown state: \[ \forall \theta \in \Theta_{failure}: \text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq \mathcal{X}_{shutdown} \] This is more conservative than nominal reachability, accounting for the fact that we cannot know exactly which failure mode is active. Traditional safety analysis techniques inform the construction of $\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis 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. %%% NOTES (Section 4.3): % - Discuss sensor failures vs actual plant failures % - Address unmodeled disturbances that aren't failures % - How much parametric uncertainty is enough? Need methodology for bounds % - Mention graceful degradation: graded responses vs immediate SCRAM % ---------------------------------------------------------------------------- % 5. INDUSTRIAL IMPLEMENTATION % ---------------------------------------------------------------------------- \subsection{Industrial Implementation} The complete methodology—procedure formalization, discrete synthesis, and continuous verification across three mode types—must now be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility and advance from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5). This research will leverage the University of Pittsburgh Cyber Energy Center's partnership with Emerson to implement and test the HAHACS methodology on production control equipment. Emerson's Ovation distributed control system is widely deployed in power generation facilities, including nuclear plants. The Ovation platform provides a realistic target for demonstrating that formally synthesized controllers can execute on industrial hardware meeting timing and reliability requirements. The discrete automaton produced by reactive 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. 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 communication between the Emerson Ovation hardware and the reactor simulation, enabling hardware-in-the-loop testing of the complete hybrid controller. Working with Emerson on such an implementation is an incredible advantage for the success and impact of this work. We will directly address the gap of verification and validation methods for these systems and industry adoption by forming a two-way exchange of knowledge between the laboratory and commercial environments. This work stands to be successful with Emerson implementation because we will have access to system experts at Emerson to help with the fine details of using the Ovation system. At the same time, we will have the benefit of transferring technology directly to industry with a direct collaboration in this research, while getting an excellent perspective of how our research outcomes can align best with customer needs. This section answered two Heilmeier questions: \textbf{What is new?} We integrate reactive synthesis, reachability analysis, and barrier certificates into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis. \textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation. Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—Section 4 addresses the next Heilmeier question: how do we measure success? Not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability. %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration % - Mention what startup sequence will be demonstrated (cold shutdown → % criticality → low power?) % - Discuss how off-nominal scenarios will be tested (sensor failures, % simulated component degradation) % - Reference Westinghouse relationship if relevant