Obsidian/Writing/ERLM/goals-and-outcomes/v5.tex

\section{Goals and Outcomes}

The goal of this research is to create a methodology for building high assurance
hybrid autonomous control systems. 

%FIRST PARAGRAPH - INTRO HOOK
Commercial control systems for nuclear power have been stuck in the past, far
behind the state of the art of controls.
% 3-5 SENTENCES KNOWN INFO
Nuclear power control systems are extremely high assurance system, where
failures are intolerable. A control failure in nuclear power has a broader
impact than financial losses. Instead, a failure can create extensive economic
losses for the power utility, interruptions for local customers, or in the worst
case, radiological release in the local environment. Because of this, control of
nuclear power is performed by operators who are extensively trained, use
detailed operating procedures, and follow strict requirements.
% GAP
This method of control has been reliable, but is woefully behind the
capabilities of modern less critical control systems, and by relying on human
operators, prevents the introduction of autonomy.
% CRITICAL NEED
To bring nuclear power control into the 21st century, we need a way to develop
autonomous control systems that have strict guarantees and assurance of their
correct behavior across their operating range.

% SECOND PARAGRAPH -  APPROACH SOLUTION
To do this, we will blend tools from computer science and formal methods with
those from engineering and control theory to build high assurance hybrid systems
to perform autonomous control.
% RATIONALE
Hybrids systems have switching behavior, where discrete transitions between
continuous dynamics occur. Verification of these systems is difficult because of
these transitions. We will address this difficulty by building autonomous hybrid
control systems that are correct by construction. We will synthesize the
discrete mode switching behavior from written operating procedures, while
utilizing reachability analysis and assume-guarantee contracts to prove that
continuous modes behave correctly.
% HYPOTHESIS PAY-OFF/IMPACT 
If we are successful in creating a hybrid control system that is correct by
construction, we can implement autonomous control systems in nuclear power with
a great assurance of their safety and performance. Autonomous control is a
technology that is desperately needed for the future of nuclear power. Nuclear
plant designs such as small modular reactors or microcreactors have been
suggested as a way to reduce the enormous capital costs of nuclear power
construction, but are limited in their feasibility by the increased cost of
operator staffing per megawatt generated. If we can reduce the quantity of
operaters needed in these reactors, we can reduce the cost of generating clean
nuclear power and address increasing energy demands.
% QUALIFICATIONS
This work is also situated in the University of Pittsburgh Cyber Energy Center.
This research is colocated with collaboration across the energy industry and
benefits from having access to industry-ready control hardware from Emerson.
The accessibility to industry this research has will ensure that solutions and
capabilities generated are aligned with industry needs.

If this research is successful, we will be able to do the following:
\begin{enumerate}
  % OUTCOME PARAGRAPH 1 TITLE
  \item \textbf{ Synthesize written operating procedures into discrete automata.
    } 
    % STRATEGY
    Discrete automata are the backbone of a continuous hybrid system. These
    automata control the swtiching behavior between continuous modes, and are
    directly analogous to operators changing between control laws. The automated
    creation of these automata is a mature field called reactive synthesis.
    Reactive synthesis is enabled by specifying logical requriements of a
    discrete system. These requirements will be created from current written
    operating procedures directly, through an intermediate tool called FRET,
    which uses a natural-language-like format called FRETish to embed
    requirements.
    % OUTCOME
    By using written operating procedures to create the discrete automata, we
    will provide a means for control systems engineers to create discrete
    switching behavior without having to become logical experts. This reduces
    the barrier to entry for using formal methods tools, making high assurance
    switching mechanisms easier to attain.

% OUTCOME PARAGRAPH 2
% TITLE
  \item \textbf{
      Build hybrid systems using correct by construction principles.
    }
% STRATEGY
    In addition to the discrete system, hybrid systems use continuous modes
    between discrete transitions. These continuous modes will be constructed
    using standard control theory practices, but will use formal methods to
    ensure their correctness. Because the discrete modes and their transitions
    will already be specified from operating requirements, the continuous modes
    will be examined to ensure that only allowable state transitions can be
    reached.
% OUTCOME
    This way, controls engineers can build continuous modes exactly as they
    would before, but iterate on their designs to ensure broader system
    correctness.

% OUTCOME PARAGRAPH 3 TITLE 
  \item \textbf{ Create autonomous control systems with strict safety
    guarantees. }
    % STRATEGY
    By combining the discrete and continuous components while building proof of
    their correctness along the way, we can translate these capabilities into
    realizable autonomous systems for nuclear power. We will use the methodology
    presented in this proposal to build a candidate control system using a
    simulation of a small modular reactor in combination with an Emerson Ovation
    control system.
    % OUTCOME
    By realizing an autonomous hybrid control system using this methodology, we
    will generate evidence that autonomous hybrid control can be realized in the
    nuclear industry with current controls equipment.


\end{enumerate}

% THIRD PARAGRAPH - IMPACT
% INNOVATION
The innovation in this work is the implementation of different formal methods
technologies for the purpose of building hybrid control systems. These
technologies will allow us to build hybrid systems with behavior we can ensure.
% OUTCOME IMPACT
The way that these technologies will be implemented is also designed to incur
the smallest amount of cost possible for possible recreation in industry.
Controls engineers should be able to find this work approachable, and
implementable in new nuclear technology control systems.
% GENERAL IMPACT
New control systems, especially autonomous control, are critical to advancing
the prevalence of nuclear power. Small modular reactors stand to answer the next
energy generation challenge in the United States, but must address the
significant operating cost required by current staffing limits. This work will
allow new reactors to reduce the amount of operators required and improve the
economic feasibility of new reactor designs.