296 lines
17 KiB
TeX
296 lines
17 KiB
TeX
\section{Research Approach}
|
|
|
|
This research will overcome the limitations of current practice to build
|
|
high-assurance hybrid control systems for critical infrastructure. Hybrid
|
|
systems combine continuous dynamics (flows) with discrete transitions (jumps),
|
|
which can be formally expressed as:
|
|
|
|
\begin{equation}
|
|
\dot{x}(t) = f(x(t),q(t),u(t))
|
|
\end{equation}
|
|
|
|
\begin{equation}
|
|
q(k+1) = \nu(x(k),q(k),u(k))
|
|
\end{equation}
|
|
|
|
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
|
|
discrete transitions. The continuous states $x$, discrete state $q$, and
|
|
control input $u$ interact to produce hybrid behavior. The discrete state $q$
|
|
defines which continuous dynamics mode is currently active. Our focus centers
|
|
on continuous autonomous hybrid systems, where continuous states remain
|
|
unchanged during jumps—a property naturally exhibited by physical systems. For
|
|
example, a nuclear reactor switching from warm-up to load-following control
|
|
cannot instantaneously change its temperature or control rod position, but can
|
|
instantaneously change control laws.
|
|
|
|
To build these systems with formal correctness guarantees, we must accomplish
|
|
three main thrusts:
|
|
|
|
\begin{enumerate}
|
|
\item Translate operating procedures and requirements into temporal logic
|
|
formulae
|
|
|
|
\item Create the discrete half of a hybrid controller using reactive synthesis
|
|
|
|
\item Develop continuous controllers to operate between modes, and verify
|
|
their correctness using reachability analysis
|
|
|
|
\end{enumerate}
|
|
|
|
The following sections discuss how these thrusts will be accomplished.
|
|
|
|
\subsection{$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}
|
|
|
|
The motivation behind this work stems from the fact that commercial nuclear
|
|
power operations remain manually controlled by human operators, despite
|
|
significant advances in control systems sophistication. The key insight is that
|
|
procedures performed by human operators are highly prescriptive and
|
|
well-documented. This suggests that human operators in nuclear power plants may
|
|
not be entirely necessary given today's available technology.
|
|
|
|
Written procedures and requirements in nuclear power are sufficiently detailed
|
|
that we may be able to translate them into logical formulae with minimal effort.
|
|
If successful, this approach would enable automation of existing procedures
|
|
without requiring system reengineering. To formalize these procedures, we will
|
|
use temporal logic, which captures system behaviors through temporal relations.
|
|
Linear Temporal Logic (LTL) provides four fundamental operators: next ($X$),
|
|
eventually ($F$), globally ($G$), and until ($U$). These operators enable
|
|
precise specification of time-dependent requirements.
|
|
|
|
Consider a nuclear reactor SCRAM requirement expressed in natural language:
|
|
\textit{``If a high temperature alarm triggers, control rods must immediately
|
|
insert and remain inserted until operator reset.''} This plain language
|
|
requirement can be translated into a rigorous logical specification:
|
|
|
|
\begin{equation}
|
|
G(HighTemp \rightarrow X(RodsInserted \wedge (\neg RodsWithdrawn\ U\
|
|
OperatorReset)))
|
|
\end{equation}
|
|
|
|
This specification precisely captures the temporal relationship between the
|
|
alarm condition, the required response, and the persistence requirement. The
|
|
global operator $G$ ensures this property holds throughout system operation,
|
|
while the next operator $X$ enforces immediate response. The until operator
|
|
$U$ maintains the state constraint until the reset condition occurs.
|
|
|
|
The most efficient path to accomplish this translation is through NASA's
|
|
Formal Requirements Elicitation Tool (FRET). FRET employs a specialized
|
|
requirements language called FRETish that restricts requirements to easily
|
|
understood components while eliminating ambiguity. FRETish bridges natural
|
|
language and mathematical specifications through a structured English-like
|
|
syntax that is automatically translatable to temporal logic.
|
|
|
|
FRET enforces this structure by requiring all requirements to contain six
|
|
components: %CITE FRET MANUAL
|
|
|
|
\begin{enumerate}
|
|
\item Scope: \textit{What modes does this requirement apply to?}
|
|
\item Condition: \textit{Scope plus additional specificity}
|
|
\item Component: \textit{What system element does this requirement affect?}
|
|
\item Shall
|
|
\item Timing: \textit{When does the response occur?}
|
|
\item Response: \textit{What action should be taken?}
|
|
\end{enumerate}
|
|
|
|
FRET provides functionality to check the \textit{realizability} of a system.
|
|
Realizability analysis determines whether written requirements are complete by
|
|
examining the six structural components. Complete requirements are those that
|
|
neither conflict with one another nor leave any behavior undefined. Systems
|
|
that are not realizable from their procedure definitions and design
|
|
requirements present problems beyond autonomous control implementation. Such
|
|
systems contain behavioral inconsistencies that represent the physical
|
|
equivalent of software bugs. Using FRET during autonomous controller
|
|
development allows us to identify and resolve these errors systematically.
|
|
|
|
The second category of realizability issues involves undefined behaviors that
|
|
are typically left to human judgment during control operations. This
|
|
ambiguity is undesirable for high-assurance systems, since even well-trained
|
|
humans remain prone to errors. By addressing these specification gaps in FRET
|
|
during autonomous controller development, we can deliver controllers free from
|
|
these vulnerabilities.
|
|
|
|
FRET provides the capability to export requirements in temporal logic format
|
|
compatible with reactive synthesis tools. This export functionality enables
|
|
progression to the next step of our approach: synthesizing discrete mode
|
|
switching behavior from the formalized requirements.
|
|
|
|
\subsection{$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow
|
|
DiscreteAutomata$}
|
|
|
|
Reactive synthesis is an active research field in computer science focused on
|
|
generating discrete controllers from temporal logic specifications. The term
|
|
``reactive'' indicates that the system responds to environmental inputs to
|
|
produce control outputs. These synthesized systems are finite in size, where
|
|
each node represents a unique discrete state. The connections between nodes,
|
|
called \textit{state transitions}, specify the conditions under which the
|
|
discrete controller moves from state to state. This complete mapping of possible
|
|
states and transitions constitutes a \textit{discrete automaton}. Discrete
|
|
automata can be represented graphically as a series of nodes that are discrete
|
|
states, with traces indicating transitions between states. From the automaton
|
|
graph, it becomes possible to fully describe the dynamics of the discrete system
|
|
and develop intuitive understanding of system behavior. Hybrid systems
|
|
naturally exhibit discrete behavior amenable to formal analysis through these
|
|
finite state representations.
|
|
|
|
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
|
|
which has demonstrated superior performance in the Reactive Synthesis
|
|
Competition (SYNTCOMP) through efficient parity game solving algorithms. Strix
|
|
translates linear temporal logic specifications into deterministic automata
|
|
automatically while maximizing generated automata quality. Once constructed, the
|
|
automaton can be straightforwardly implemented using standard programming
|
|
control flow constructs. The graphical representation provided by the automaton
|
|
enables inspection and facilitates communication with controls programmers who
|
|
may not have formal methods expertise.
|
|
|
|
We will use discrete automata to represent the switching behavior of our hybrid
|
|
system. This approach yields an important theoretical guarantee: because the
|
|
discrete automaton is synthesized entirely through automated tools from design
|
|
requirements and operating procedures, we can prove that the automaton—and
|
|
therefore our hybrid switching behavior—is \textit{correct by construction}.
|
|
Correctness of the switching controller is paramount to this work. Mode
|
|
switching represents the primary responsibility of human operators in control
|
|
rooms today. Human operators possess the advantage of real-time judgment—when
|
|
mistakes occur, they can correct them dynamically with capabilities that extend
|
|
beyond written procedures. Autonomous control lacks this adaptive advantage.
|
|
Instead, we must ensure that autonomous controllers replacing human operators
|
|
will not make switching errors between continuous modes. By synthesizing
|
|
controllers from logical specifications with guaranteed correctness, we
|
|
eliminate the possibility of switching errors.
|
|
|
|
\subsection{$(DiscreteAutomata \wedge ControlTheory \wedge Reachability)
|
|
\rightarrow ContinuousModes$}
|
|
|
|
While discrete system components will be synthesized with correctness
|
|
guarantees, they represent only half of the complete system. Autonomous
|
|
controllers like those we are developing exhibit continuous dynamics within
|
|
discrete states, as described by $f(\cdot)$ in Equation 1. This section
|
|
describes how we will develop continuous control modes, verify their
|
|
correctness, and address the unique verification challenges of hybrid systems.
|
|
|
|
The approach described for producing discrete automata yields physics-agnostic
|
|
specifications that represent only half of a complete hybrid autonomous
|
|
controller. These automata alone cannot define the full behavior of the
|
|
control systems we aim to construct. The continuous modes will be developed
|
|
after discrete automaton construction, leveraging the automaton structure and
|
|
transitions to design multiple smaller, specialized continuous controllers.
|
|
|
|
The discrete automaton transitions are key to the supervisory behavior of the
|
|
autonomous controller. These transitions mark decision points for switching
|
|
between continuous control modes and define their strategic objectives. We
|
|
will classify three types of high-level continuous controller objectives based
|
|
on discrete mode transitions:
|
|
|
|
\begin{enumerate}
|
|
\item \textbf{Stabilizing:} A stabilizing control mode has one primary
|
|
objective: maintaining the hybrid system within its current discrete mode.
|
|
This corresponds to steady-state normal operating modes, such as a
|
|
full-power load-following controller in a nuclear power plant. Stabilizing
|
|
modes can be identified from discrete automata as nodes with only incoming
|
|
transitions.
|
|
|
|
\item \textbf{Transitory:} A transitory control mode has the primary goal of
|
|
transitioning the hybrid system from one discrete state to another. In
|
|
nuclear applications, this might represent a controlled warm-up procedure.
|
|
Transitory modes ultimately drive the system toward a stabilizing
|
|
steady-state mode. These modes may have secondary objectives within a
|
|
discrete state, such as maintaining specific temperature ramp rates before
|
|
reaching full-power operation.
|
|
|
|
\item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode
|
|
with additional safety constraints. Expulsory modes ensure the system is
|
|
directed to a safe stabilizing mode during failure conditions. For example,
|
|
if a transitory mode fails to achieve its intended transition, the
|
|
expulsory mode activates to immediately and irreversibly guide the system
|
|
toward a globally safe state. A reactor SCRAM exemplifies an expulsory
|
|
continuous mode: when initiated, it must reliably terminate the nuclear
|
|
reaction and direct the reactor toward stabilizing decay heat removal.
|
|
|
|
\end{enumerate}
|
|
|
|
Building continuous modes after constructing discrete automata enables local
|
|
controller design focused on satisfying discrete transitions. The primary
|
|
challenge in hybrid system verification is ensuring global stability across
|
|
transitions. Current techniques struggle with this problem because dynamic
|
|
discontinuities complicate verification. This work alleviates these problems by
|
|
designing continuous controllers specifically with transitions in mind. By
|
|
decomposing continuous modes according to their required behavior at transition
|
|
points, we avoid solving trajectories through the entire hybrid system. Instead,
|
|
we can use local behavior information at transition boundaries. To ensure
|
|
continuous modes satisfy their requirements, we will employ three main
|
|
techniques: reachability analysis, assume-guarantee contracts, and barrier
|
|
certificates.
|
|
|
|
\textbf{Reachability Analysis:} Reachability analysis computes the reachable set
|
|
of states for a given input set. While trivial for linear continuous systems,
|
|
recent advances have extended reachability to complex nonlinear systems. We will
|
|
use reachability to define continuous state ranges at discrete transition
|
|
boundaries and verify that requirements are satisfied within continuous modes.
|
|
Recent advances using neural network approximations of Hamilton-Jacobi equations
|
|
have demonstrated significant speedups while maintaining safety guarantees for
|
|
high-dimensional systems, expanding the practical applicability of these
|
|
methods.
|
|
|
|
\textbf{Assume-Guarantee Contracts:} Assume-guarantee contracts will be
|
|
employed when continuous state boundaries are not explicitly defined. For any
|
|
given mode, the input range for reachability analysis is defined by the output
|
|
ranges of discrete modes that transition to it. This compositional approach
|
|
ensures each continuous controller is prepared for its possible input range,
|
|
enabling subsequent reachability analysis without requiring global system
|
|
analysis.
|
|
|
|
\textbf{Barrier Certificates:} Finally, we will use barrier certificates to
|
|
prove that mode transitions are satisfied. Barrier certificates ensure that
|
|
continuous modes on either side of a transition behave appropriately. Control
|
|
barrier functions provide a method to certify safety by establishing
|
|
differential inequality conditions that guarantee forward invariance of safe
|
|
sets. For example, a barrier certificate can guarantee that a transitory mode
|
|
transferring control to a stabilizing mode will always move away from the
|
|
transition boundary, rather than destabilizing the target stabilizing mode.
|
|
|
|
Combining these three techniques will enable us to prove that continuous
|
|
components of our hybrid controller satisfy discrete requirements, and thus,
|
|
complete system behavior. To demonstrate this methodology, we will develop an
|
|
autonomous startup controller for a Small Modular Advanced High Temperature
|
|
Reactor (SmAHTR). SmAHTR represents an ideal test case as a liquid-salt cooled
|
|
reactor design with well-documented startup procedures that must transition
|
|
through multiple distinct operational modes: initial cold conditions, controlled
|
|
heating to operating temperature, approach to criticality, low-power physics
|
|
testing, and power ascension to full operating capacity. We have already
|
|
developed a high-fidelity SmAHTR model in Simulink that captures the
|
|
thermal-hydraulic and neutron kinetics behavior essential for verifying
|
|
continuous controller performance under realistic plant dynamics. The
|
|
synthesized hybrid controller will be implemented on an Emerson Ovation control
|
|
system platform, which is representative of industry-standard control hardware
|
|
deployed in modern nuclear facilities. The Advanced Reactor Cyber Analysis and
|
|
Development Environment (ARCADE) suite will serve as the integration layer,
|
|
managing real-time communication between the Simulink simulation and the Ovation
|
|
controller. This hardware-in-the-loop configuration enables validation of the
|
|
controller implementation on actual industrial control equipment interfacing
|
|
with a realistic reactor simulation, providing assessment of computational
|
|
performance, real-time execution constraints, and communication latency effects.
|
|
By demonstrating autonomous startup control on this representative platform, we
|
|
will establish both the theoretical validity and practical feasibility of the
|
|
synthesis methodology for deployment in actual small modular reactor systems.
|
|
|
|
This unified approach addresses a fundamental gap in hybrid system design by
|
|
bridging formal methods and control theory through a systematic, tool-supported
|
|
methodology. By translating existing nuclear procedures into temporal logic,
|
|
synthesizing provably correct discrete switching logic, and developing verified
|
|
continuous controllers, we create a complete framework for autonomous hybrid
|
|
control with mathematical guarantees. The result is an autonomous controller
|
|
that not only replicates human operator decision-making but does so with formal
|
|
assurance that switching logic is correct by construction and continuous
|
|
behavior satisfies safety requirements. This methodology transforms nuclear
|
|
reactor control from a manually intensive operation requiring constant human
|
|
oversight into a fully autonomous system with higher reliability than
|
|
human-operated alternatives. More broadly, this approach establishes a
|
|
replicable framework for developing high-assurance autonomous controllers in any
|
|
domain where operating procedures are well-documented and safety is paramount.
|
|
|
|
% COMMENTS FOR FUTURE REVISION:
|
|
% 1. Add concrete examples throughout (specific nuclear procedures, requirements)
|
|
% 2. Include a figure showing the overall workflow/methodology
|
|
% 3. Consider adding a subsection on validation approach
|
|
% 4. Strengthen the connections between subsections
|
|
% 5. Add discussion of limitations and assumptions
|