Dane Sabo
a9632a264e
A Writing/ERLM/GOv1.pdf A Writing/ERLM/goals-and-outcomes/v1.tex A Writing/ERLM/goals-and-outcomes/v2.tex M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf
76 lines
4.2 KiB
TeX
76 lines
4.2 KiB
TeX
\section{Goals and Outcomes}
|
|
|
|
The goal of this research is to use formal methods to create high-assurance
|
|
hybrid control systems. Hybrid control systems have great potential for
|
|
implementation in autonomous control as they are able to change control laws
|
|
based on discrete triggers in the operating range of the controller. This allows
|
|
the autonomous controller to use several easily tractable control laws for different
|
|
regions in the state space, instead of using one controller over the entire
|
|
systems operating range. But, the discrete jumps between control laws in a
|
|
hybrid controller present challenges in proving stability and liveness
|
|
properties of the whole system. While tools from control theory can prove
|
|
properties for each individual control mode, they do not generalize when
|
|
switching between control laws is introduced.
|
|
|
|
This research will take a different approach to hybrid controller synthesis and
|
|
verification. Using tools from the formal methods community, we will create
|
|
controllers that are correct-by-construction and allow guarantees to be made
|
|
about the whole system's behavior. To demonstrate this, an autonomous controller
|
|
for a nuclear power plant start-up procedure will be created. Nuclear power is
|
|
an excellent test case for this work as the continuous piece of reactor dynamics
|
|
is well studied, while the discrete component of mode switching is explicitly
|
|
stated in regulatory requirements and operating procedures. Nuclear reactor
|
|
control today \textit{is} a hybrid control system--many functions in the control
|
|
room use automated controllers for basic tasks, but the engagement and selection
|
|
of these controllers is done by human operators referencing procedures to make
|
|
decisions.
|
|
|
|
The capability to create high-assurance hybrid control systems has the potential
|
|
to reduce the labor required to operate critical systems by removing the human
|
|
operator from the loop. Nuclear power stands to greatly benefit from greater
|
|
controller autonomy as the largest expense for reactors today is operations and
|
|
maintenance. Technologies such as microreactors and modular reactors will
|
|
improve the maintenance costs required through the use of factory-made
|
|
replacement components, but will suffer increased operating costs per megawatt
|
|
produced if they are required to staff the same way reactors today are staffed.
|
|
But, if increased autonomy can be introduced, these costs will be ameliorated.
|
|
|
|
If this research is successful, we will be able to do the following:
|
|
|
|
\begin{enumerate}
|
|
|
|
\item
|
|
\textbf{Formalize mode switching requirements as logical specifications that
|
|
can be translated into discrete controller implementations.} The discrete
|
|
transitions between continuous controller modes is often explicitly defined
|
|
for critical systems in operating procedures and regulatory requirements.
|
|
These statements will be translated into a temporal logic, which will then
|
|
be synthesized into a discrete controller implementation for continuous
|
|
controller mode switching.
|
|
|
|
\item
|
|
\textbf{Categorize different continuous controller modes by their strategic
|
|
relavance.} Different control modes serve one of two purposes: they may be
|
|
transitory or stabilizing. Knowing when to switch from one control mode to
|
|
another is handled by the discrete component of the hybrid system, but this
|
|
outcome will identify the properties the continuous components must satisfy
|
|
for each controller mode.
|
|
|
|
\item
|
|
\textbf{Verify that continuous controller modes satisfy dynamic
|
|
requirements.} For the discrete transitions between control modes to be
|
|
useful, we must ensure that the continuous control modes will actually move
|
|
the system to the transition, or if stabilizing, keep the system from
|
|
leaving the control mode.
|
|
|
|
\item
|
|
\textbf{Prove that a hybrid system implementation achieve strategic goals
|
|
across the entire controller operating range.} By creating discrete
|
|
controller transitions from logical specifications that are
|
|
correct-by-construction and validating that continuous components perform
|
|
appropriately between discrete transitions, we can be confident that the
|
|
hybrid system is free from defect and can be utilized as a critical
|
|
autonomous controller.
|
|
|
|
\end{enumerate}
|