91 lines
4.6 KiB
TeX
91 lines
4.6 KiB
TeX
\dasnote{Research statement is very similar to GO because that's what I had
|
|
when I prepared it. If it's going to be an executive summary, it should talk
|
|
more about the other sections rather than just being a slightly different GO
|
|
section.}
|
|
% GOAL PARAGRAPH
|
|
The goal of this research is to develop a methodology for creating autonomous
|
|
hybrid control systems with mathematical guarantees of safe and correct
|
|
behavior.
|
|
|
|
% INTRODUCTORY PARAGRAPH Hook
|
|
Nuclear power relies on extensively trained operators who follow detailed
|
|
written procedures to manage reactor control. Based on these procedures and
|
|
their interpretation of plant conditions, they make critical decisions about
|
|
when to switch between control objectives.
|
|
% Gap
|
|
This reliance on human operators has created an economic challenge for
|
|
next-generation nuclear power plants. Small modular reactors face significantly
|
|
higher per-megawatt staffing costs than conventional plants. Autonomous control
|
|
systems are needed that can safely manage complex operational sequences with the
|
|
same assurance as human-operated systems, but without constant supervision.
|
|
|
|
% APPROACH PARAGRAPH Solution
|
|
To address this need, we will combine formal methods from computer science
|
|
with control theory to build hybrid control systems that are correct by
|
|
construction, leveraging the extensive domain knowledge already embedded in
|
|
existing operating procedures and safety analyses.
|
|
% Rationale
|
|
Hybrid systems use discrete logic to switch between continuous control modes,
|
|
similar to how operators change control strategies. Existing formal methods
|
|
generate provably correct switching logic but cannot handle continuous
|
|
dynamics during transitions, while traditional control theory verifies
|
|
continuous behavior but lacks tools for proving discrete switching
|
|
correctness.
|
|
|
|
% Hypothesis and Technical Approach
|
|
We will bridge this gap through a three-stage methodology. First, we will
|
|
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. This approach
|
|
enables realizability checking that identifies conflicts and ambiguities in
|
|
procedures before implementation. Second, we will synthesize discrete mode
|
|
switching logic using reactive synthesis to produce deterministic automata that
|
|
are correct by construction. Third, we will develop continuous controllers for
|
|
each discrete mode using standard control theory and reachability analysis. We
|
|
will classify continuous modes based on their transition objectives and verify
|
|
safe mode transitions using barrier certificates and reachability analysis.
|
|
This compositional approach enables local verification of continuous modes
|
|
without requiring global trajectory analysis across the entire hybrid system.
|
|
We will validate this methodology through hardware-in-the-loop testing
|
|
on an Emerson Ovation distributed control system, made possible through the
|
|
University of Pittsburgh Cyber Energy Center's industry partnership.
|
|
% Pay-off
|
|
This approach enables autonomous management of 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. These specifications will be synthesized into
|
|
discrete control logic using reactive synthesis tools.
|
|
% Outcome
|
|
Control engineers will be able to generate mode-switching
|
|
controllers from regulatory procedures, reducing barriers to high-assurance control systems.
|
|
|
|
% OUTCOME 2 Title
|
|
\item \textit{Verify continuous control behavior across mode transitions.}
|
|
% Strategy
|
|
We will develop methods using reachability analysis to ensure continuous
|
|
control modes satisfy discrete transition requirements.
|
|
% Outcome
|
|
Engineers will be able to design continuous controllers using standard
|
|
practices while ensuring system correctness and proving mode transitions
|
|
occur safely at the right times.
|
|
|
|
% OUTCOME 3 Title
|
|
\item \textit{Demonstrate autonomous reactor startup control with safety
|
|
guarantees.}
|
|
% Strategy
|
|
We will implement this methodology on a small modular reactor simulation
|
|
using industry-standard control hardware.
|
|
% Outcome
|
|
Without retraining costs or new equipment, control engineers
|
|
will be able to implement high-assurance autonomous controls on industrial
|
|
hardware they already use.
|
|
|
|
\end{enumerate}
|