Obsidian/Writing/ERLM/research-approach/v1.tex

\section{Research Approach}

This research will overcome the limits of current practice to build high
assurance hybrid control systems for critical infrastructure. To do this, 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

\end{enumerate}

In the following sections I will discuss how these thrusts will be accomplished.

\subsection{\((Procedures \wedge FRET) \rightarrow Temporal Specifications\)}

The motivating factor behind this work is the fact that commercial nuclear power
operations have remained manually controlled by human operators, despite
advances in control systems sophistication. The frustrating part of this is that
the procedures performed by human operators are highly prescriptive. Human
operators in nuclear power plants may not be entirely necessary with the
technology we have today.

Written procedures and requirements in nuclear power are descriptive enough we
may be able to translate them into logical formulae with little effort. If we
can accomplish this, we can automate existing procedures without inducing
reengineering. The easiest way to accomplish this task will be through the use
of automated translational tools. Tools like FRET can help accomplish this task.

FRET uses a specialized requriements languaged called FRETish to restrict
requirements to be written in easy to understand components, but without leaving
room for ambiguity. FRET does this by forcing requirements to contain six
possible parts: %CITE FRET MANUAL

\begin{enumerate}
  \item Scope: \textit{What modes does this requirement hold?}
  \item Condition: \textit{Scope + more specificity}
  \item Component: \textit{What does this requirment affect?}
  \item Shall
  \item Timing: \textit{When does the response happen?}
  \item Response: \textit{What should happen?}
\end{enumerate}

FRET provides functionality to check the \textit{realizability} of a system.
Realizability checks whether or not the written requirements are complete by
examining the six components that make up requirements.
Complete requirements are those that do not conflict with one another, and do
not leave any behavior as undefined. Systems that are not realizable from the
procedure definitions and design requirements are problematic beyond realizing
autonomy. These systems have behavior in their systems that is a physical
equivalent of a software bug. With FRET, we can catch these errors while
building an autonomous controller. The second type of error including undefined
behaviors are those that may be left up to human judgement during control. This
is not desirable for high assurance systems, as however trained humans can be,
are still prone to errors. Addressing these vulnerabilities in FRET while
building an autonomous controller will deliver a controller free of these
vulnerabilities.

%The above stuff about realizability should be checked out.

FRET also provides the capability to export the requirements created in a
temporal logic format. This capability allows us to leave FRET and move onto the
next step of our approach, where we will synthesize the discrete mode switching
behavior.

\subsection{\((TemporalLogic \wedge ReactiveSynthesis) \rightarrow
DiscreteAutomata\) }
In this section of our approach we describe how the discrete component of the
hybrid system will be created. The formal specifications created in FRET will be
used with reactive synthesis tools to generate the mode switching components.
These components effectively make up the human component of reactor operation by
automating the decision points typically specified in written procedures. By
removing the human component, we eliminate the possibility of human error and
advance hybrid system autonomy.

Reactive synthesis is an active field in computer science that focuses on the
synthesis of discrete controllers created from temporal logic specifications.
Reactive defines that the system responds to inputs to create outputs. These
systems are finite in size, where each node represents a unique discrete state.
The connections between nodes are called \textit{state transitions}, and
describe under what conditions the discrete controller moves from state to
state. This mapping of all the possible states and transitions for the discrete
controller is known as a discrete automata. From a graph of the automata, it
is possible to completely describe the dynamics of a finite discrete system and
develop an intuitive understanding of how the system will behave. Once the
automata is constructed, it is straight forward to implement in a text-based
programming language using basic control flow tools.

We will use discrete automata to represent the switching behavior of our hybrid
system. From this automata we can extract an important proof. Because this
discrete automata has been synthesized entirely through automated tools from
design requirements and operating procedures, we can prove that the discrete
automata, and therein our hybrid switching behavior, is correct by construction.
Correctness of the switching controller is paramount to this work. The switching
between continuous modes is the primary responsibility of human operators in
control rooms today. Human operators have the benefit of judgement--if a human
operator makes a mistake, they are able to correct for it in real time with
fidelity beyond operating procedures. Autonomous control will not have this
advantage. Instead, we must ensure that an autonomous controller replacing a
human operator will not make mistakes when switching between continuous modes.
By synthesizing these controllers from logical specifications with assurance of
their correctness, we guarantee they will not err.

\subsection{\((DiscreteAutomata \wedge ControlTheory \wedge Reachability)
\rightarrow ContinuousModes\)}

While the discrete components of our system will be synthesized with assurance
of correctness, that is only half of the story. Autonomous controllers like the
ones we are building have continuous dynamics underneath the discrete states. In
this section, we describe how we will build out the continuous control modes,
will verify their correctness, and the unique challenges of hybrid systems that
we will overcome with this work.

First and foremost, lets discuss the glaring problem left unaddressed in the last
section. From the requirements and specifications, we described a way to produce
discrete automata. These automata are physics agnostic, and are only half of
the picture of a hybrid autonomous controller. They alone do not define the
complete behavior of the control systems that we are trying to build. The
continuous modes of the controller will be developed after the discrete automata
is produced, as we are going to lever the structure of the automata and it's
transitions to build out several smaller continuous controllers. 

The transitions of the discrete automata are the key to the supervisory behavior
of the autonomous controller. These transitions mark decision points to switch
between continuous control modes, and their strategic objectives. We will define
three types of high-level continuous controller goals based on the transitions
between discrete modes:

\begin{enumerate}
  \item \textbf{Stabilizing:} A stabilizing control mode in our hybrid system is
    a continuous control mode with one primary objective. It issues continuous
    control inputs keep the hybrid system in the current mode. This is analogous
    to an steady-state normal operating mode, such as full power load following
    conrtoller in a nuclear power plant. Stabilizing modes can be identified
    from discrete automata as nodes that only have transitions pointing towards
    them. 
    
  \item \textbf{Transitory:} A transitory control mode is a continuous mode with
    a primary goal of transitioning the hybrid system from one discrete state to
    another. In a nuclear context, this can represent a continuous mode such as
    a controlled warm-up procedure. The transitory mode ultimately wants to move
    the control system to a stabilizing steady-state mode. Transitory modes may
    have secondary control goals within one discrete state, such as maintaining a
    specific rate of temperature increase before reaching full-power operation. 

  \item \textbf{Expulsory:} An expulsory mode is a type of transitory mode that
    has special restrictions. Expulsory modes are continuous control modes that
    are designed to ensure the system is directed to a safe stabilizing mode in
    case of a failure. For example, if a transitory mode fails to deliver the
    system to the correct next mode, the expulsory mode is designed to be
    activated and immediately and irrevocably steward the system towards a
    globally safe state. A straightforward example of an expulsory continuous
    mode is a reactor SCRAM. At any point that a SCRAM is initiated, it should
    be possible to kill the reaction and direct the reactor towards a
    stabilizing decay heat removal mode.

\end{enumerate}

The benefit of building continuous modes after constructing the discrete
automata is that we can build local controllers to satisfy the discrete
transitions. The most common problems when verifying hybrid systems is the
challenge of assuring global stability conditions over transitions. Current
techniques make this a difficult problem because discontinuities in the dynamics
are not conducive to easy verification. This work helps alieviate these problems
by specifically building continuous controllers with the transitions in mind. By
breaking down continuous modes into their required behavior at the transition
points, we do not need to solve trajectories through the entire hybrid system,
but instead can use information about the local behavior of continuous modes at
the transition barrier. 

To ensure that continuous modes satisfy their requirements, we will use three
main techniques: reachability analysis, assume-guarantee contracts, and barrier
certificates. Reachability analysis is used to obtain the reachable set of
states for a given input set of states for a system. For linear continous
systems, reachability is trivial, but recent advances have expanded reachability
to complex nonlinear systems. We will use reachability to define the continuous
range of states at discrete transition barriers, or when a range of continuous
states is prescribed by a requirement, ensure that the requirement is satisfied
for the continuous mode. We will use assume-guarantee contracts for when
continuous states borders are not defined. Essentially, this means that for a
given mode, the input range to use with reachability is defined by the output
ranges of the discrete modes that transition to it. This ensures that each
continuous controller is prepared for the possible input range it may receive,
and that reachability analysis can then be used. Finally, we will use barrier
certificates to prove that transitions between modes are satisfied. Barrier
certificates ensure that along a transition the continuous modes on either side
do not behave adversely. For example, a barrier certificate can ensure that a
transitory mode handing off to a stabilizing mode will always move away from the
transition border, rather than leave the stabilizing mode. Combining these three
techniques will allow us to prove the continuous components of our hybrid
controller satisfy the discrete requirements.