Thesis/1-goals-and-outcomes/research_statement_v1.tex

% GOAL PARAGRAPH
This research develops a methodology that creates autonomous control systems
with guaranteed safe and correct behavior.

% INTRODUCTORY PARAGRAPH Hook
Extensively trained operators manage nuclear reactor control by following detailed written procedures. These operators interpret plant conditions and decide when to switch between control objectives.
% Gap
Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt staffing costs that significantly exceed those of conventional plants. This economic constraint threatens their viability without autonomous control. Autonomous control systems must therefore manage complex operational sequences safely, without constant supervision, while maintaining the same assurance—or better—than human-operated systems.

% APPROACH PARAGRAPH Solution
We combine formal methods from computer science with control theory to
build hybrid control systems that are correct by construction. 
% Rationale
Hybrid systems mirror operator behavior: discrete
logic switches between continuous control modes. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics
during transitions. Control theory verifies continuous behavior but
cannot prove discrete switching correctness. 
% Hypothesis and Technical Approach
A three-stage methodology bridges this gap. First, we translate written
operating procedures into temporal logic specifications using NASA's Formal
Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
condition, component, timing, and response elements. Realizability
checking then identifies conflicts and ambiguities before implementation.
Second, reactive synthesis generates deterministic automata that are provably
correct by construction.
Third, we design continuous controllers for each discrete mode using standard
control theory and verify them using reachability analysis. We classify continuous modes based on
their transition objectives, then employ assume-guarantee contracts and barrier
certificates to prove mode transitions occur safely. This approach enables local verification of continuous modes
without global trajectory analysis across the entire hybrid system. An
Emerson Ovation control system will demonstrate this methodology. 
% Pay-off
This approach demonstrates that autonomous control can manage complex nuclear
power operations while maintaining safety guarantees.

% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
  % OUTCOME 1 Title
  \item \textit{Synthesize written procedures into verified control logic.} 
    % Strategy
    We will develop a methodology for converting written operating procedures
    into formal specifications. Reactive synthesis tools will then generate
    discrete control logic from these specifications.
    % Outcome
    Control engineers will generate mode-switching controllers from regulatory
    procedures with minimal formal methods expertise. This reduces barriers to
    high-assurance control systems.

    % OUTCOME 2 Title
  \item \textit{Verify continuous control behavior across mode transitions.}
    % Strategy
    Reachability analysis will verify that continuous control modes satisfy discrete
    transition requirements. 
    % Outcome
    Engineers will design continuous controllers using standard practices while
    maintaining formal correctness guarantees. Mode transitions will provably occur safely and at
    the correct times.

    % OUTCOME 3  Title
  \item \textit{Demonstrate autonomous reactor startup control with safety
    guarantees.}
    % Strategy
    A small modular reactor simulation using industry-standard control hardware
    will implement this methodology.
    % Outcome
    Control engineers will implement high-assurance autonomous controls on
    industrial platforms they already use. This enables autonomy without retraining
    costs or new equipment development.

\end{enumerate}