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

Editorial pass 2: Clarity and sentence structure improvements

Browse Source 
- Broke up complex sentences for better clarity
- Replaced first-person pronouns with more formal constructions
- Improved parallel structure in lists
- Enhanced readability in technical sections
- Maintained precision while improving accessibility
This commit is contained in:
Split 2026-03-09 17:54:08 -04:00
parent d365f6927a
commit c0c67f52f3
2 changed files with 27 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
3-research-approach/v3.tex
View File

@ -236,7 +236,7 @@ eventually reaches operating temperature''), and response properties (``if
coolant pressure drops, the system initiates shutdown within bounded time''). coolant pressure drops, the system initiates shutdown within bounded time'').
I use FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training. This methodology uses FRET (Formal Requirements Elicitation Tool)—developed by NASA for high-assurance timed systems—to build these temporal logic statements. FRET provides an intermediate language between temporal logic and natural language. It enables rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility proves crucial for industrial feasibility: the current nuclear workforce can adopt these tools without extensive formal methods training.
FRET's key feature is its ability to start with logically imprecise FRET's key feature is its ability to start with logically imprecise
statements and refine them consecutively into well-posed specifications. We statements and refine them consecutively into well-posed specifications. We
@ -293,7 +293,7 @@ Reactive synthesis produces a provably correct discrete controller that determin
Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method.
This methodology's scope requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification, which confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques—this work assumes that capability exists. The contribution lies in the verification framework confirming that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. This methodology's scope requires clarification. This work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques. This work assumes that capability exists. The contribution lies in the verification framework. It confirms that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
The operational control scope defines go/no-go decisions that determine what The operational control scope defines go/no-go decisions that determine what
kind of continuous control to implement. The entry or exit conditions of a kind of continuous control to implement. The entry or exit conditions of a
@ -310,7 +310,7 @@ the vector fields at discrete state interfaces makes reachability analysis
computationally expensive, and analytic solutions often become intractable computationally expensive, and analytic solutions often become intractable
\cite{MANYUS THESIS}. \cite{MANYUS THESIS}.
I circumvent these issues by designing the hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}. This methodology circumvents these issues by designing the hybrid system from the bottom up with verification in mind. The discrete transitions define each continuous control mode's input and output sets clearly \textit{a priori}.
Each discrete mode $q_i$ provides Each discrete mode $q_i$ provides
three key pieces of information for continuous controller design: three key pieces of information for continuous controller design:
@ -377,7 +377,7 @@ systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool
depends on the structure of the continuous dynamics. Linear systems admit depends on the structure of the continuous dynamics. Linear systems admit
efficient polyhedral or ellipsoidal reachability computations. Nonlinear efficient polyhedral or ellipsoidal reachability computations. Nonlinear
systems require more conservative over-approximations using techniques such as systems require more conservative over-approximations using techniques such as
Taylor models or polynomial zonotopes. For this work, we will select tools Taylor models or polynomial zonotopes. This work will select tools
appropriate to the fidelity of the reactor models available. appropriate to the fidelity of the reactor models available.
%%% NOTES (Section 4.1): %%% NOTES (Section 4.1):
@ -505,7 +505,7 @@ requirements. The discrete automaton produced by reactive synthesis will be
compiled to run on Ovation controllers, with verification that the implemented compiled to run on Ovation controllers, with verification that the implemented
behavior matches the synthesized specification exactly. behavior matches the synthesized specification exactly.
For the continuous dynamics, we will use a small modular For the continuous dynamics, this work will use a small modular
reactor simulation. The SmAHTR (Small modular Advanced High Temperature reactor simulation. The SmAHTR (Small modular Advanced High Temperature
Reactor) model provides a relevant testbed for startup and shutdown procedures. Reactor) model provides a relevant testbed for startup and shutdown procedures.
The ARCADE (Advanced Reactor Control Architecture Development Environment) The ARCADE (Advanced Reactor Control Architecture Development Environment)
@ -513,16 +513,15 @@ interface will establish communication between the Emerson Ovation hardware and
the reactor simulation, enabling hardware-in-the-loop testing of the complete the reactor simulation, enabling hardware-in-the-loop testing of the complete
hybrid controller. hybrid controller.
Working with Emerson on such an implementation is an incredible advantage for Working with Emerson on such an implementation provides an incredible advantage for
the success and impact of this work. We will directly address the gap of the success and impact of this work. The collaboration directly addresses the gap in
verification and validation methods for these systems and industry adoption by verification and validation methods for these systems and industry adoption. It
forming a two-way exchange of knowledge between the laboratory and commercial forms a two-way exchange of knowledge between the laboratory and commercial
environments. This work stands to be successful with Emerson implementation environments. This work stands to succeed with Emerson implementation
because we will have access to system experts at Emerson to help with the fine because it will have access to system experts at Emerson. These experts can help with the fine
details of using the Ovation system. At the same time, we will have the benefit details of using the Ovation system. At the same time, the collaboration will
of transferring technology directly to industry with a direct collaboration in transfer technology directly to industry through direct research participation. This provides an excellent perspective on how research
this research, while getting an excellent perspective of how our research outcomes can best align with customer needs.
outcomes can align best with customer needs.
This section addressed two critical Heilmeier questions: What is new? Why will it succeed? This section addressed two critical Heilmeier questions: What is new? Why will it succeed?

27
6-broader-impacts/v1.tex
View File

@ -26,17 +26,16 @@ Synthesizing provably correct hybrid controllers from formal specifications auto
The correct-by-construction methodology proves critical for this transition. The correct-by-construction methodology proves critical for this transition.
Traditional automation approaches cannot provide sufficient safety guarantees Traditional automation approaches cannot provide sufficient safety guarantees
for nuclear applications, where regulatory requirements and public safety for nuclear applications. Regulatory requirements and public safety
concerns demand the highest levels of assurance. By formally verifying both the concerns demand the highest levels of assurance. This research formally verifies both the
discrete mode-switching logic and the continuous control behavior, this research discrete mode-switching logic and the continuous control behavior. It
produces controllers with mathematical proofs of correctness. These produces controllers with mathematical proofs of correctness. These
guarantees enable automation to safely handle routine operations---startup guarantees enable automation to safely handle routine operations: startup
sequences, power level changes, and normal operational transitions---that sequences, power level changes, and normal operational transitions. These operations
currently require human operators to follow written procedures. Operators will currently require human operators to follow written procedures. Operators will
remain in supervisory roles to handle off-normal conditions and provide remain in supervisory roles to handle off-normal conditions and provide
authorization for major operational changes, but the routine cognitive burden of authorization for major operational changes. The routine cognitive burden of
procedure execution shifts to provably correct automated systems that are much procedure execution shifts to provably correct automated systems that cost far less to operate.
cheaper to operate.
SMRs represent an ideal deployment target for this technology. Nuclear SMRs represent an ideal deployment target for this technology. Nuclear
Regulatory Commission certification requires extensive documentation of control Regulatory Commission certification requires extensive documentation of control
@ -49,15 +48,15 @@ continuous control modes. The infrastructure of requirements and specifications
already exists as part of the licensing process, creating a direct pathway from already exists as part of the licensing process, creating a direct pathway from
existing regulatory documentation to formally verified autonomous controllers. existing regulatory documentation to formally verified autonomous controllers.
Beyond reducing operating costs for new reactors, this research will establish a Beyond reducing operating costs for new reactors, this research establishes a
generalizable framework for autonomous control of safety-critical systems. The generalizable framework for autonomous control of safety-critical systems. The
methodology of translating operational procedures into formal specifications, methodology translates operational procedures into formal specifications. It
synthesizing discrete switching logic, and verifying continuous mode behavior synthesizes discrete switching logic. It verifies continuous mode behavior. This methodology
applies to any hybrid system with documented operational requirements. Potential applies to any hybrid system with documented operational requirements. Potential
applications include chemical process control, aerospace systems, and autonomous applications include chemical process control, aerospace systems, and autonomous
transportation, where similar economic and safety considerations favor increased transportation. Similar economic and safety considerations favor increased
autonomy with provable correctness guarantees. Demonstrating this approach in autonomy with provable correctness guarantees in these domains. Demonstrating this approach in
nuclear power---one of the most regulated and safety-critical domains---will nuclear power—one of the most regulated and safety-critical domains—will
establish both the technical feasibility and regulatory pathway for broader establish both the technical feasibility and regulatory pathway for broader
adoption across critical infrastructure. adoption across critical infrastructure.