danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Edit Goals: fix topic position, integrate qualifications, trim redundancy

Browse Source
This commit is contained in:
Split 2026-03-16 13:53:52 -04:00
parent 54f0f2f1e5
commit c011631557
1 changed files with 78 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

155
1-goals-and-outcomes/goals.tex
View File

@ -12,69 +12,65 @@ behavior.\splitnote{Clear thesis statement. Gets right to it.}
% INTRODUCTORY PARAGRAPH Hook % INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability, Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service interruptions, where failures can result in significant economic losses, service
or radiological release.\splitnote{Stakes established immediately — good hook.} interruptions, or radiological
release.\splitnote{Stakes established immediately — good hook.}
% Known information % Known information
Currently, nuclear plant operations rely on extensively trained human operators Currently, nuclear plant operations rely on extensively trained human
who follow detailed written procedures and strict regulatory requirements to operators who follow detailed written procedures and strict regulatory
manage reactor control. These operators make critical decisions about when to requirements to manage reactor control. These operators make critical
switch between different control modes based on their interpretation of plant decisions about when to switch between different control modes based on their
conditions and procedural guidance. interpretation of plant conditions and procedural guidance.
% Gap % Gap
This reliance on human operators prevents autonomous control capabilities and \oldt{This reliance on human operators prevents autonomous control
creates a fundamental economic challenge for next-generation reactor capabilities and creates a fundamental economic challenge for next-generation
designs. reactor designs.} \newt{This reliance on human operators prevents autonomous
\splitinline{The ``and'' here joins two distinct issues (autonomy barrier + control and creates a fundamental economic barrier for next-generation
economics). Consider making the causal link explicit: ``This reliance on human reactor designs.} Small modular reactors face per-megawatt staffing costs
operators not only prevents autonomous control capabilities but also far exceeding those of conventional plants, threatening their economic
creates...'' or split into two sentences.} viability.
Small modular reactors, in particular, face per-megawatt staffing costs far
exceeding those of conventional plants and threaten their economic viability.
% Critical Need % Critical Need
What is needed is a method to create autonomous control systems that safely \oldt{What is needed is a method to create autonomous control systems that
manage complex operational sequences with the same assurance as human-operated safely manage complex operational sequences with the same assurance as
systems, but without constant human supervision. human-operated systems, but without constant human supervision.}
\splitinline{``What is needed is'' — Gopen would call this a weak topic \newt{Autonomous control systems must safely manage complex operational
position. The sentence buries the subject. Try: ``Autonomous control systems sequences with the same assurance as human-operated systems, but without
must safely manage complex operational sequences...'' Puts the actor in the constant human supervision.}
topic position.}
% APPROACH PARAGRAPH Solution % APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction. build hybrid control systems that are correct by construction.
% Rationale % Rationale
Hybrid systems use discrete logic to switch between continuous control modes, Hybrid systems use discrete logic to switch between continuous control modes,
mirroring how operators change control strategies. Existing formal methods can mirroring how operators change control strategies. Existing formal methods
generate provably correct switching logic from written requirements, but they can generate provably correct switching logic from written requirements, but
cannot handle the continuous dynamics that occur during transitions between they cannot handle the continuous dynamics that occur during transitions
modes. Meanwhile, traditional control theory can verify continuous behavior but between modes. Meanwhile, traditional control theory can verify continuous
lacks tools for proving correctness of discrete switching behavior but lacks tools for proving correctness of discrete switching
decisions.\splitnote{Excellent setup of the gap — shows why neither approach decisions.\splitnote{Excellent setup of the gap — shows why neither approach
alone is sufficient.} alone is sufficient.}
% Hypothesis % Hypothesis
By synthesizing discrete mode transitions directly from written operating By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can create procedures and verifying continuous behavior between transitions, we can
hybrid control systems with end-to-end correctness guarantees. If existing create hybrid control systems with end-to-end correctness guarantees. If
procedures can be formalized into logical specifications and continuous dynamics existing procedures can be formalized into logical specifications and
verified against transition requirements, then autonomous controllers can be continuous dynamics verified against transition requirements, then autonomous
built that are provably free from design controllers can be built that are provably free from design
defects.\splitnote{Hypothesis is clear and testable.} defects.\splitnote{Hypothesis is clear and testable.}
% Pay-off % Pay-off
This approach will enable autonomous control in nuclear power plants while \oldt{This approach will enable autonomous control in nuclear power plants
maintaining the high safety standards required by the industry. while maintaining the high safety standards required by the industry.
% Qualifications % Qualifications
This work is conducted within the University of Pittsburgh Cyber Energy Center, This work is conducted within the University of Pittsburgh Cyber Energy
which provides access to industry collaboration and Emerson control hardware, Center, which provides access to industry collaboration and Emerson control
ensuring that developed solutions align with practical implementation hardware, ensuring that developed solutions align with practical
requirements. implementation requirements.} \newt{This approach will enable autonomous
\splitinline{This qualifications paragraph feels orphaned here. It's important control in nuclear power plants while maintaining the high safety standards
context but reads as an afterthought. Consider integrating it into the required by the industry. The University of Pittsburgh Cyber Energy Center's
approach paragraph (``...demonstrated on Emerson hardware through our partnership with Emerson provides access to industry-standard control
partnership with the Cyber Energy Center'') or moving to a ``Why This Will hardware, ensuring that developed solutions align with practical
Succeed'' framing later.} implementation requirements from the outset.}
% OUTCOMES PARAGRAPHS % OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following: If this research is successful, we will be able to do the following:
@ -85,27 +81,30 @@ If this research is successful, we will be able to do the following:
\item \textbf{Translate written procedures into verified control logic.} \item \textbf{Translate written procedures into verified control logic.}
% Strategy % Strategy
We will develop a methodology for converting existing written operating We will develop a methodology for converting existing written operating
procedures into formal specifications that can be automatically synthesized procedures into formal specifications that can be automatically
into discrete control logic. This process will use structured intermediate synthesized into discrete control logic. This process will use structured
representations to bridge natural language procedures and mathematical intermediate representations to bridge natural language procedures and
logic. mathematical logic.
% Outcome % Outcome
Control system engineers will generate verified mode-switching controllers \oldt{Control system engineers will generate verified mode-switching
directly from regulatory procedures without formal methods controllers directly from regulatory procedures without formal methods
expertise,\dasinline{Same comment as in executive expertise, lowering the barrier to high-assurance control systems.}
summary. Might not be true and is not the point.} \newt{This will lower the barrier to high-assurance control systems by
lowering the barrier to high-assurance control systems. generating verified mode-switching controllers directly from regulatory
procedures.}\dasinline{Same comment as in executive summary. Might not be
true and is not the point.}
% OUTCOME 2 Title % OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.} \item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy % Strategy
We will establish methods for analyzing continuous control modes to ensure We will establish methods for analyzing continuous control modes to ensure
they satisfy discrete transition requirements. Using classical control they satisfy discrete transition requirements. Using classical control
theory for linear systems and reachability analysis for nonlinear dynamics, theory for linear systems and reachability analysis for nonlinear
we will verify that each continuous mode safely reaches its intended dynamics, we will verify that each continuous mode safely reaches its
transitions. intended transitions.
Engineers will design continuous controllers using standard practices while % Outcome
iterating to ensure broader system correctness, proving that mode Engineers will design continuous controllers using standard practices
while iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times. transitions occur safely and at the correct times.
% OUTCOME 3 Title % OUTCOME 3 Title
@ -116,31 +115,33 @@ If this research is successful, we will be able to do the following:
nuclear reactor startup procedures, implementing it on a small modular nuclear reactor startup procedures, implementing it on a small modular
reactor simulation using industry-standard control hardware. This reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power modes from cold shutdown through criticality to power
operation.\splitnote{``cold shutdown through criticality to power operation.\splitnote{``cold shutdown through criticality to power
operation'' — concrete and impressive scope.} operation'' — concrete and impressive scope.}
% Outcome % Outcome
We will demonstrate that autonomous hybrid control can be realized in the We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward reduced nuclear industry with current equipment, establishing a path toward
operator staffing while maintaining safety. reduced operator staffing while maintaining safety.
\end{enumerate} \end{enumerate}
% IMPACT PARAGRAPH Innovation % IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid verification to enable end-to-end correctness guarantees for hybrid
systems.\splitnote{Clear ``what's new'' statement.} systems.\splitnote{Clear ``what's new'' statement.}
% Outcome Impact % Outcome Impact
If successful, control engineers will create autonomous controllers from If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance existing procedures with mathematical proof of correct behavior.
autonomous control will become practical for safety-critical applications. High-assurance autonomous control will become practical for safety-critical
applications.
% Impact/Pay-off % Impact/Pay-off
This capability is essential for the economic viability of next-generation \oldt{This capability is essential for the economic viability of
nuclear power. Small modular reactors offer a promising solution to growing next-generation nuclear power. Small modular reactors offer a promising
energy demands, but their success depends on reducing per-megawatt operating solution to growing energy demands, but their success depends on reducing
costs through increased autonomy.\dasinline{This paragraph is literally per-megawatt operating costs through increased autonomy. This research will
the same as the rest of the GO. Does not belong here provide the tools to achieve that autonomy while maintaining the exceptional
and feels very redundant.} This research will provide the tools to safety record the nuclear industry requires.} \newt{This research will
achieve that autonomy while maintaining the exceptional safety record the provide the tools to achieve that autonomy while maintaining the exceptional
nuclear industry requires.\splitnote{Strong closing --- ties technical work to safety record the nuclear industry
real-world impact and economic necessity.} requires.}\dasinline{This paragraph is literally the same as the rest of the
GO. Does not belong here and feels very redundant.}