Split
4a1cc9a549
Three-level editorial review per Gopen's Sense of Structure and Heilmeier alignment: TACTICAL (sentence-level): - Broke up overly long sentences for clarity - Positioned known information before new (topic-stress) - Converted passive constructions to active where appropriate - Clarified logical relationships with shorter, crisper sentences - Improved verb choice and sentence flow OPERATIONAL (paragraph-level): - Added bridging sentences to improve flow between ideas - Strengthened transitions between subsections - Improved coherence within sections - Clarified argument structure in key passages STRATEGIC (document-level): - Verified Heilmeier question alignment in each section - Improved section summaries to reinforce answers - Strengthened linkages between sections - Ensured consistent narrative thread throughout Focus: Changes that genuinely improve clarity and impact, not nitpicky edits.
54 lines
4.0 KiB
TeX
54 lines
4.0 KiB
TeX
% GOAL PARAGRAPH
|
|
This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
|
|
|
|
% INTRODUCTORY PARAGRAPH Hook
|
|
Today's nuclear reactors operate under the control of extensively trained human operators. These operators follow detailed written procedures and switch between control objectives based on plant conditions.
|
|
% Gap
|
|
Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems offer a solution by managing complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding human-operated systems.
|
|
|
|
% APPROACH PARAGRAPH Solution
|
|
This research combines formal methods from computer science with control theory to produce hybrid control systems that are correct by construction.
|
|
% Rationale
|
|
This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together.
|
|
% 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 by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode, with reachability analysis verifying each controller.
|
|
|
|
Continuous modes classify by transition objective. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system.
|
|
% Pay-off
|
|
This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability.
|
|
|
|
% OUTCOMES PARAGRAPHS
|
|
This research, if successful, produces three concrete outcomes:
|
|
\begin{enumerate}
|
|
% OUTCOME 1 Title
|
|
\item \textit{Synthesize written procedures into verified control logic.}
|
|
% Strategy
|
|
A methodology converts written operating procedures into formal specifications.
|
|
Reactive synthesis tools then generate discrete control logic from these specifications.
|
|
% Outcome
|
|
Control engineers generate mode-switching controllers directly from regulatory
|
|
procedures. Minimal formal methods expertise required. This reduces 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 occur safely and at
|
|
the correct times—provably.
|
|
|
|
% OUTCOME 3 Title
|
|
\item \textit{Demonstrate autonomous reactor startup control with safety
|
|
guarantees.}
|
|
% Strategy
|
|
This methodology demonstrates on a small modular reactor simulation using industry-standard control hardware.
|
|
% 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}
|