diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 06c3185..38c2f4e 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -15,7 +15,7 @@ Emergency Operating Procedures (EOPs) for design-basis accidents, Severe Accident Management Guidelines (SAMGs) for beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are -developed using guidance from NUREG-0900~\cite{NUREG-0899, 10CFR50.34}, but their +developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies fundamentally on expert judgment and simulator validation rather than formal verification. Procedures undergo technical evaluation, simulator validation testing, and biennial review as part of operator diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index b98954f..4b5199a 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -452,11 +452,11 @@ reachable within time horizon $T$: \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset \] -Because the discrete controller defines clear boundaries in continuous state +\textcolor{blue}{Because the discrete controller defines clear boundaries in continuous state space, the verification problem for each transitory mode is well-posed. We know the possible initial conditions, we know the target conditions, and we know the safety envelope. The verification task is to confirm that the candidate -continuous controller achieves the objective from all possible starting points. +continuous controller achieves the objective from all possible starting points.} Several tools exist for computing reachable sets of hybrid systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool @@ -478,20 +478,18 @@ appropriate to the fidelity of the reactor models available. \subsubsection{Stabilizing Modes} -\textcolor{blue}{Stabilizing modes are continuous controllers with an objective -of maintaining a particular discrete state indefinitely. Rather than driving -the system toward an exit condition, they keep the system within a safe -operating region. Examples include steady-state power operation, hot standby, -and load-following at constant power level.} +Stabilizing modes are continuous controllers with an objective of maintaining a +particular discrete state indefinitely. Rather than driving the system toward an +exit condition, they keep the system within a safe operating region. Examples +include steady-state power operation, hot standby, and load-following at +constant power level. Reachability analysis for stabilizing modes may not be a +suitable approach to validation. Instead, we plan to use barrier certificates. +Barrier certificates analyze the dynamics of the system to determine whether +flux across a given boundary exists. They evaluate whether any trajectory leaves +a given boundary. This definition is exactly what defines the validity of a +stabilizing continuous control mode. -Reachability analysis for stabilizing modes may not be the most prudent approach -to validation. Instead, barrier certificates must be used. Barrier certificates -analyze the dynamics of the system to determine whether flux across a given -boundary exists. They evaluate whether any trajectory leaves a given boundary. -This definition is exactly what defines the validity of a stabilizing continuous -control mode. - -\textcolor{blue}{A barrier certificate (or control barrier function) is a +A barrier certificate (or control barrier function) is a scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe set. The idea is analogous to Lyapunov functions for stability: rather than computing trajectories explicitly, we find a certificate @@ -504,7 +502,7 @@ barrier certificate condition requires: This condition states that on the boundary of the safe set (where $B(x) = 0$), the time derivative of $B$ is non-negative. Geometrically, this means the vector field points inward or tangent to the boundary, never outward. If this -condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave.} +condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave. Because the design of the discrete controller defines careful boundaries in continuous state space, the barrier is known prior to designing the continuous @@ -513,13 +511,17 @@ complication in validating stabilizing continuous control modes. The discrete specifications tell us what region must be invariant; the barrier certificate confirms that the candidate controller achieves this invariance. -\textcolor{blue}{Finding barrier certificates can be formulated as a +Finding barrier certificates can be formulated as a sum-of-squares (SOS) optimization problem for polynomial systems, or solved using satisfiability modulo theories (SMT) solvers for broader classes of dynamics. The key advantage is that the verification is independent of how the controller was designed. Standard control techniques can be used to build continuous controllers, and barrier certificates provide a separate -check that the result satisfies the required invariants.} +check that the result satisfies the required invariants. This also allows for +the checking of control modes with different models than they are designed for. +For example, a lower fidelity model can be used for controller design, but a +higher fidelity model can be used for the actual validation of that stabilizing +controller. %%% NOTES (Section 4.2): % - Clarify relationship between barrier certificates and Lyapunov stability @@ -533,17 +535,12 @@ check that the result satisfies the required invariants.} \subsubsection{Expulsory Modes} -The validation of transitory and stabilizing modes hinges on an assumption of -correct plant models. In the case of a mechanical failure, the model will almost -certainly be invalidated. For this reason, we must also build safe shutdown -modes, since a human will not be in the loop to handle failures. - -\textcolor{blue}{Expulsory modes are continuous controllers responsible for +Expulsory modes are continuous controllers responsible for ensuring safety when failures occur. They are designed for robustness rather than optimality. The control objective is to drive the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and -controlled depressurization procedures.} +controlled depressurization procedures. We can detect that physical failures exist because our physical controllers have been previously proven correct by reachability and barrier certificates. We know @@ -554,7 +551,7 @@ violated by the continuous physical controller. This is a direct consequence of having verified the nominal continuous control modes: unexpected behavior implies off-nominal conditions. -\textcolor{blue}{The mathematical formulation for expulsory mode verification +The mathematical formulation for expulsory mode verification differs from transitory modes in two key ways. First, the entry conditions may be the entire state space (or a large, conservatively bounded region) rather than a well-defined entry set. The failure may occur at any point during @@ -565,7 +562,7 @@ failure modes: \] where $\Theta_{failure}$ captures the range of possible degraded plant behaviors identified through failure mode and effects analysis (FMEA) or -traditional safety analysis.} +traditional safety analysis. We verify expulsory modes using reachability analysis with parametric uncertainty. The verification condition requires that for all parameter values @@ -578,12 +575,12 @@ the safe shutdown state: This is more conservative than nominal reachability, accounting for the fact that we cannot know exactly which failure mode is active. -\textcolor{blue}{Traditional safety analysis techniques inform the construction +Traditional safety analysis techniques inform the construction of $\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis accident analysis identify credible failure scenarios and their effects on plant dynamics. The expulsory mode must handle the worst-case dynamics within -this envelope. This is where conservative controller design is appropriate: -safety margins matter more than performance during emergency shutdown.} +this envelope. This is where conservative controller design is appropriate as +safety margins will matter more than performance during emergency shutdown. %%% NOTES (Section 4.3): % - Discuss sensor failures vs actual plant failures @@ -597,40 +594,25 @@ safety margins matter more than performance during emergency shutdown.} \subsection{Industrial Implementation} -\textcolor{blue}{The methodology described above must be validated on realistic +The methodology described above must be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility. This research will leverage the University of Pittsburgh Cyber Energy Center's partnership with Emerson to implement and test the HAHACS methodology on -production control equipment.} - -\textcolor{blue}{Emerson's Ovation distributed control system is widely deployed +production control equipment. Emerson's Ovation distributed control system is widely deployed in power generation facilities, including nuclear plants. The Ovation platform provides a realistic target for demonstrating that formally synthesized controllers can execute on industrial hardware meeting timing and reliability requirements. The discrete automaton produced by reactive synthesis will be compiled to run on Ovation controllers, with verification that the implemented -behavior matches the synthesized specification exactly.} +behavior matches the synthesized specification exactly. -\textcolor{blue}{For the continuous dynamics, we will use a small modular +For the continuous dynamics, we will use a small modular reactor simulation. The SmAHTR (Small modular Advanced High Temperature Reactor) model provides a relevant testbed for startup and shutdown procedures. The ARCADE (Advanced Reactor Control Architecture Development Environment) interface will establish communication between the Emerson Ovation hardware and the reactor simulation, enabling hardware-in-the-loop testing of the complete -hybrid controller.} - -\textcolor{blue}{The demonstration will proceed through stages aligned with -Technology Readiness Levels: -\begin{enumerate} - \item \textbf{TRL 3:} Individual components validated in isolation (synthesized - automaton, verified continuous modes) - \item \textbf{TRL 4:} Integrated hybrid controller executing complete sequences - in pure simulation - \item \textbf{TRL 5:} Hardware-in-the-loop testing with Ovation executing the - discrete controller and simulation providing plant response -\end{enumerate} -Success at TRL 5 demonstrates that the methodology produces deployable -controllers, not merely theoretical constructs.} +hybrid controller. Working with Emerson on such an implementation is an incredible advantage for the success and impact of this work. We will directly address the gap of diff --git a/main.aux b/main.aux index 971193e..d4e6641 100644 --- a/main.aux +++ b/main.aux @@ -33,25 +33,25 @@ \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{18}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{18}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{18}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{19}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent } \citation{eia_lcoe_2022} \citation{eesi_datacenter_2024} \citation{eia_lcoe_2022} -\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{21}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent } \bibstyle{ieeetr} \bibdata{references} -\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{23}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent } \gtt@chartextrasize{0}{164.1287pt} -\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{23}{}\protected@file@percent } -\newlabel{fig:gantt}{{3}{23}{Schedule, Milestones, and Deliverables}{figure.3}{}} -\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{23}{}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent } +\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent } \bibcite{NUREG-0899}{1} \bibcite{10CFR50.34}{2} \bibcite{10CFR55.59}{3} @@ -67,5 +67,5 @@ \bibcite{Kiniry2024}{13} \bibcite{eia_lcoe_2022}{14} \bibcite{eesi_datacenter_2024}{15} -\@writefile{toc}{\contentsline {section}{References}{24}{}\protected@file@percent } -\gdef \@abspage@last{28} +\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent } +\gdef \@abspage@last{27} diff --git a/main.fdb_latexmk b/main.fdb_latexmk index 01a63e5..c8ebbb4 100644 --- a/main.fdb_latexmk +++ b/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 1772647153.79833 "main.aux" "main.bbl" "main" 1772647228.17025 2 +["bibtex main"] 1772657516.80216 "main.aux" "main.bbl" "main" 1772909692.49481 2 "./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe "" "/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" - "main.aux" 1772647227.95816 5748 e33be58dd60b44046113ddb8b0d9bf30 "pdflatex" + "main.aux" 1772909692.27813 5748 38dc212531f318e67f49d597c2908f59 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1772647226.2456 "main.tex" "main.pdf" "main" 1772647228.17034 0 +["pdflatex"] 1772909690.76715 "main.tex" "main.pdf" "main" 1772909692.4949 0 "/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" @@ -245,17 +245,17 @@ "/usr/local/texlive/2025/texmf.cnf" 1741450484 577 418a7058ec8e006d8704f60ecd22c938 "" "1-goals-and-outcomes/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 "" "1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f "" - "2-state-of-the-art/v2.tex" 1772219521.82345 12622 8fd5435154f6a45bb3e558ffebacbf58 "" - "3-research-approach/v3.tex" 1772647226.05037 36560 f9231e331bb93290a2a1d788c915c945 "" + "2-state-of-the-art/v2.tex" 1772909690.23793 12622 1460f7a4c2b48a1a772d8a0f5db216af "" + "3-research-approach/v3.tex" 1772743152.76875 35753 93d4c7b608feeba783c33affa59dd220 "" "4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc "" "5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 "" "6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c "" "8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 "" "dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 "" - "main.aux" 1772647227.95816 5748 e33be58dd60b44046113ddb8b0d9bf30 "pdflatex" - "main.bbl" 1772647153.8597 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" + "main.aux" 1772909692.27813 5748 38dc212531f318e67f49d597c2908f59 "pdflatex" + "main.bbl" 1772657516.86263 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" "main.tex" 1772218582.98667 954 b43a8fa32e5ebbd5cc6319a366737c39 "" - "main.toc" 1772647227.96211 2129 5b96f286c13251cf15256102f6fd6b8f "pdflatex" + "main.toc" 1772909692.28232 2129 eb658283ff0c872296846602d3e9dde6 "pdflatex" (generated) "main.aux" "main.log" diff --git a/main.log b/main.log index 5c8dfc8..d25f137 100644 --- a/main.log +++ b/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 4 MAR 2026 13:00 +This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 7 MAR 2026 13:54 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -948,38 +948,36 @@ LaTeX Warning: Citation `MANYUS THESIS' on page 11 undefined on input line 383. [12] -[13] +[13]) -[14]) +[14] (./4-metrics-of-success/v1.tex -[15] (./4-metrics-of-success/v1.tex +[15]) -[16]) +[16] (./5-risks-and-contingencies/v1.tex -[17] (./5-risks-and-contingencies/v1.tex +[17] -[18] +[18]) -[19]) +[19] (./6-broader-impacts/v1.tex) -[20] (./6-broader-impacts/v1.tex) +[20] -[21] - -[22] (./8-schedule/v1.tex +[21] (./8-schedule/v1.tex Missing character: There is no , in font nullfont! ) (./main.bbl -[23] +[22] Underfull \hbox (badness 10000) in paragraph at lines 32--33 \OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[] [] -[24]) +[23]) -[25] (./main.aux) +[24] (./main.aux) *********** LaTeX2e <2024-11-01> patch level 2 L3 programming layer <2025-01-18> @@ -998,10 +996,10 @@ Here is how much of TeX's memory you used: 1141 hyphenation exceptions out of 8191 110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on main.pdf (28 pages, 189916 bytes). +Output written on main.pdf (27 pages, 188983 bytes). PDF statistics: - 183 PDF objects out of 1000 (max. 8388607) - 111 compressed objects within 2 object streams + 180 PDF objects out of 1000 (max. 8388607) + 109 compressed objects within 2 object streams 0 named destinations out of 1000 (max. 500000) 109 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/main.pdf b/main.pdf index 88cad6d..f36c443 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.synctex.gz b/main.synctex.gz index 4c72008..97829ee 100644 Binary files a/main.synctex.gz and b/main.synctex.gz differ diff --git a/main.toc b/main.toc index 6817872..a85d0b9 100644 --- a/main.toc +++ b/main.toc @@ -13,15 +13,15 @@ \contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}% \contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}% \contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}% -\contentsline {section}{\numberline {4}Metrics for Success}{16}{}% -\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}% -\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}% -\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{16}{}% -\contentsline {section}{\numberline {5}Risks and Contingencies}{18}{}% -\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{18}{}% -\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{18}{}% -\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{19}{}% -\contentsline {section}{\numberline {6}Broader Impacts}{21}{}% -\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{23}{}% -\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{23}{}% -\contentsline {section}{References}{24}{}% +\contentsline {section}{\numberline {4}Metrics for Success}{15}{}% +\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}% +\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}% +\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}% +\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}% +\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}% +\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}% +\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}% +\contentsline {section}{\numberline {6}Broader Impacts}{20}{}% +\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}% +\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}% +\contentsline {section}{References}{23}{}%