Dane Sabo
8184e48dd3
M .task/backlog.data M .task/completed.data M .task/pending.data M .task/undo.data M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log
86 lines
4.2 KiB
TeX
86 lines
4.2 KiB
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 set of discrete
|
|
states \(q\).
|