\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 set of discrete
states \(q\). 

% what does it mean to be a single discrete state
% what do the transitions mean
% How're we going to use reactive synthesis to do this for us
% what are some state of the art tools to use
% What's the output
% Explain how the transitions are the edges in the state space, and we're
% basically creating hybrid automata without actually specifying the dynamics
% underneath
% we're going to figure out the continuous dynamics in the next section. Then,
% for the continuous section, basically talk about how now that we have the
% discrete modes, we just need to build controllers that satisfy all the
% transitions and operational goals for each mode. We've broken up the control
% system into several smaller pieces that are more manageable. Include how
% reachability becomes a part of that. What does it mean to have input and
% output guarantees based on the allowable transitions?

%write tasks in here maybe. Or the main thrusts.