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

% GOAL PARAGRAPH
This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.

% INTRODUCTORY PARAGRAPH Hook
Nuclear reactors require extensively trained operators who follow detailed written procedures. Operators switch between control objectives based on plant conditions.
% Gap
Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. To remain competitive, these reactors need autonomous control systems that manage complex operational sequences safely without constant supervision while providing assurance equal to or exceeding that of human-operated systems.

% APPROACH PARAGRAPH Solution
Formal methods from computer science combine with control theory to
build hybrid control systems correct by construction. 
% Rationale
Hybrid systems mirror operator decision-making: discrete
logic switches between continuous control modes. Existing formal methods
generate provably correct switching logic but fail during transitions with continuous dynamics. Control theory verifies continuous behavior but
fails to prove discrete switching correctness. 
% Hypothesis and Technical Approach
Three stages bridge this gap. First, written
operating procedures translate 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 identifies conflicts and ambiguities before implementation.
Second, reactive synthesis generates deterministic automata—provably
correct by construction.
Third, standard control theory designs continuous controllers for each discrete mode; reachability analysis verifies them. Continuous modes classify by their transition objectives. Assume-guarantee contracts and barrier certificates prove safe mode transitions. Local verification of continuous modes
becomes possible without global trajectory analysis across the entire hybrid system. An
Emerson Ovation control system demonstrates this methodology. 
% Pay-off
This autonomous control approach can then manage complex nuclear
power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.

% 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 develop a methodology for converting written operating procedures
    into formal specifications. Reactive synthesis tools then generate
    discrete control logic from these specifications.
    % Outcome
    Control engineers can generate mode-switching controllers from regulatory
    procedures with minimal formal methods expertise, reducing barriers to
    high-assurance control systems.

    % OUTCOME 2 Title
  \item \textit{Verify continuous control behavior across mode transitions.}
    % Strategy
    Reachability analysis verifies that continuous control modes satisfy discrete
    transition requirements. 
    % Outcome
    Engineers design continuous controllers using standard practices while
    maintaining formal correctness guarantees. Mode transitions 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
    implements this methodology.
    % Outcome
    Control engineers implement high-assurance autonomous controls on
    industrial platforms they already use, enabling autonomy without retraining
    costs or new equipment development.

\end{enumerate}