diff --git a/Writing/ERLM/Sabo_Whitepaper.pdf b/Writing/ERLM/Sabo_Whitepaper.pdf new file mode 100644 index 000000000..ea07cd9b9 Binary files /dev/null and b/Writing/ERLM/Sabo_Whitepaper.pdf differ diff --git a/Writing/ERLM/dane_proposal_format.cls b/Writing/ERLM/dane_proposal_format.cls index 0c3fdb02d..4e4fd543f 100644 --- a/Writing/ERLM/dane_proposal_format.cls +++ b/Writing/ERLM/dane_proposal_format.cls @@ -103,6 +103,8 @@ \\ Advisor: Dr. Daniel G. Cole\\ dgcole@pitt.edu\\ +\\ + Track: PhD Mechanical Engineering } \date{\today} diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index 2f7efb537..7dfb5c426 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -2,21 +2,17 @@ \bibstyle{unsrt} \providecommand \oddpage@label [2]{} \@writefile{toc}{\contentsline {section}{\numberline {1}Objectives}{2}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2}Objectives}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {3}Limits of Current Practice}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4}Research Approach}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5}Metrics of Success}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{10}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics of Success}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Broader Impacts}{6}{}\protected@file@percent } \bibcite{10CFR55}{1} -\bibcite{princeton}{2} -\bibcite{Kemeny1979}{3} -\bibcite{NUREG-0899}{4} -\bibcite{DOE-HDBK-1028-2009}{5} -\bibcite{WNA2020}{6} -\bibcite{IAEA-severe-accidents}{7} -\bibcite{Wang2025}{8} -\bibcite{Kiniry2022}{9} -\bibcite{eia_lcoe_2022}{10} -\bibcite{eesi_datacenter_2024}{11} -\@writefile{toc}{\contentsline {section}{References}{12}{}\protected@file@percent } -\gdef \@abspage@last{13} +\bibcite{Kemeny1979}{2} +\bibcite{NUREG-0899}{3} +\bibcite{DOE-HDBK-1028-2009}{4} +\bibcite{WNA2020}{5} +\bibcite{Kiniry2022}{6} +\bibcite{eia_lcoe_2022}{7} +\bibcite{eesi_datacenter_2024}{8} +\@writefile{toc}{\contentsline {section}{References}{7}{}\protected@file@percent } +\gdef \@abspage@last{8} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index efbf987f4..6c3e30cb3 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,9 +1,8 @@ # Fdb version 4 -["pdflatex"] 1760990396.64627 "main.tex" "main.pdf" "main" 1760990397.59592 0 +["pdflatex"] 1760994767.73072 "main.tex" "main.pdf" "main" 1760994768.58948 0 "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 "" "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" - "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c "" @@ -19,14 +18,7 @@ "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a "" - "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 "" - "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" - "/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 "" - "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d "" - "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" - "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" - "/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 "" @@ -35,8 +27,6 @@ "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 "" - "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac "" - "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf" 1136768653 964 5673178ff30617b900214de28ab32b38 "" "/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b "" "/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty" 1644112042 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a "" "/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb "" @@ -221,10 +211,10 @@ "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e "" "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 "" - "dane_proposal_format.cls" 1760370937.93092 2555 2a01bb8bad8f4ed4e921f0e44566678c "" - "main.aux" 1760990397.47327 1085 9e68fae35f59a6899f3340eaf1c73ae0 "pdflatex" - "main.tex" 1760990396.41916 316 db7ca25ef1aea8ffbcbf35ffc893f193 "" - "whitepaper/v1.tex" 1760990371.68075 59622 b94eab76770c3fd9ee71c7178c32dfef "" + "dane_proposal_format.cls" 1760994752.93894 2596 f4b1a6fb5a74347c13e92ea1ba135818 "" + "main.aux" 1760994768.47467 923 a0e5e8073ff8be27724bce962cac74dd "pdflatex" + "main.tex" 1760990942.42923 316 db7ca25ef1aea8ffbcbf35ffc893f193 "" + "whitepaper/v1.tex" 1760994601.26193 23492 0df1332b575872555e2b920878fd817b "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index 48ef389d1..2fe40e449 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -413,10 +413,9 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm @@ -433,34 +432,21 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf INPUT main.aux -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index ba3882fc1..803d81be8 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 20 OCT 2025 15:59 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 20 OCT 2025 17:12 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -876,46 +876,36 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available (Font) Font shape `OT1/ptm/b/n' tried instead on input line 5. [1 -{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./whitepaper/v1.tex [1] [2] [3] [4] +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./whitepaper/v1.tex [1] [2] [3] LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212. LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212. LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214. - [5] [6] -Overfull \hbox (79.94554pt too wide) in paragraph at lines 372--378 -\OT1/ptm/m/n/12 ment trans-lates into tem-po-ral logic as: $\OML/ztmcm/m/it/12 G\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 HighTemp \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 X\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 RodsInserted \OMS/ztmcm/m/n/12 ^ \OT1/ztmcm/m/n/12 (\OMS/ztmcm/m/n/12 :\OML/ztmcm/m/it/12 RodsWithdrawn U OperatorReset\OT1/ztmcm/m/n/12 )))$\OT1/ptm/m/n/12 . - [] - -[7] -Overfull \hbox (19.73378pt too wide) in paragraph at lines 412--423 -\OT1/ptm/m/n/12 op-er-at-ing pro-ce-dures, we can prove that the automaton---and there-fore our hy-brid switch-ing behavior--- - [] - -[8] [9] -LaTeX Font Info: Trying to load font information for TS1+ptm on input line 535. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212. + [4] [5] +LaTeX Font Info: Trying to load font information for TS1+ptm on input line 344. (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. -) [10] [11]) [12] (./main.aux) +) [6]) [7] (./main.aux) *********** LaTeX2e <2023-11-01> patch level 1 L3 programming layer <2024-01-22> *********** ) Here is how much of TeX's memory you used: - 25373 strings out of 476182 - 526915 string characters out of 5795595 + 25363 strings out of 476182 + 526810 string characters out of 5795595 1934975 words of memory out of 5000000 - 46831 multiletter control sequences out of 15000+600000 - 590992 words of font info for 106 fonts, out of 8000000 for 9000 + 46826 multiletter control sequences out of 15000+600000 + 587807 words of font info for 99 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on main.pdf (13 pages, 109205 bytes). + +Output written on main.pdf (8 pages, 68969 bytes). PDF statistics: - 110 PDF objects out of 1000 (max. 8388607) - 64 compressed objects within 1 object stream + 74 PDF objects out of 1000 (max. 8388607) + 41 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 109 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index bc9969ced..27f05025e 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index 11fea118e..f776d5727 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/whitepaper/v1.tex b/Writing/ERLM/whitepaper/v1.tex index 3ff544203..5861f5a1f 100644 --- a/Writing/ERLM/whitepaper/v1.tex +++ b/Writing/ERLM/whitepaper/v1.tex @@ -1,4 +1,3 @@ -\newpage % PROJECT SUMMARY \section*{Project Summary} @@ -99,546 +98,7 @@ correct by construction. Third, we will develop and verify continuous controllers for each discrete mode using standard control theory and reachability analysis. We will classify continuous modes based on their transition objectives, and then employ assume-guarantee contracts and barrier -certificates to prove that mod\documentclass[11pt]{article} - -% Page setup -\usepackage[margin=1in]{geometry} -\usepackage{setspace} -\setstretch{1.0} - -% Packages -\usepackage{amsmath} -\usepackage{cite} - -% Document begins -\begin{document} - -% COVER SHEET -\begin{center} -{\Large \textbf{From Cold Start to Critical: Formal Synthesis of Hybrid \\ -Controllers for Nuclear Reactor Startup}} - -\vspace{0.5in} - -\textbf{White Paper} - -\vspace{0.25in} - -\textbf{NSF Program:} Cyber-Physical Systems (CPS) - -\vspace{0.25in} - -\textbf{Principal Investigator:} Dane A. Sabo\\ -Email: dane.sabo@pitt.edu - -\vspace{0.25in} - -\textbf{Faculty Advisor:} Dr. Daniel G. Cole\\ -Email: dgcole@pitt.edu - -\vspace{0.25in} - -University of Pittsburgh\\ -Department of Mechanical Engineering and Materials Science\\ -Swanson School of Engineering - -\end{center} - -\newpage - -% PROJECT SUMMARY -\section*{Project Summary} - -\subsection*{Overview} - -This research will develop a methodology for creating autonomous hybrid -control systems with mathematical guarantees of safe and correct behavior. -Nuclear power plants require the highest levels of control system reliability, -where failures can result in significant economic losses or radiological -release. Currently, nuclear operations rely on extensively trained human -operators who follow detailed written procedures to manage reactor control. -However, reliance on human operators prevents introduction of autonomous -control capabilities and creates fundamental economic challenges for -next-generation reactor designs. Emerging technologies like small modular -reactors face significantly higher per-megawatt staffing costs than -conventional plants, threatening their economic viability. - -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. Hybrid systems use discrete logic to switch between continuous -control modes, similar to how operators change control strategies. Existing -formal methods can generate provably correct switching logic from written -requirements, but they cannot handle the continuous dynamics that occur during -transitions between modes. Meanwhile, traditional control theory can verify -continuous behavior but lacks tools for proving correctness of discrete -switching decisions. By synthesizing discrete mode transitions directly from -written operating procedures and verifying continuous behavior between -transitions, we can create hybrid control systems with end-to-end correctness -guarantees. - -\subsection*{Intellectual Merit} - -The intellectual merit lies in unifying discrete synthesis and continuous -verification to enable end-to-end correctness guarantees for hybrid systems. -This research will advance knowledge by developing a systematic, -tool-supported methodology for translating written procedures into temporal -logic, synthesizing provably correct discrete switching logic, and developing -verified continuous controllers. The approach addresses a fundamental gap in -hybrid system design by bridging formal methods from computer science and -control theory. - -\subsection*{Broader Impacts} - -This research directly addresses the multi-billion dollar operations and -maintenance cost challenge facing nuclear power deployment. By synthesizing -provably correct hybrid controllers, we can automate routine operational -sequences that currently require constant human oversight, enabling a shift -from direct operator control to supervisory monitoring. Beyond nuclear -applications, this research will establish a generalizable framework for -autonomous control of safety-critical systems including chemical process -control, aerospace systems, and autonomous transportation. - -\newpage - -% RESEARCH DESCRIPTION -\section*{Research Description} - -\section{Objectives} - -The goal of this research is to develop a methodology for creating autonomous -hybrid control systems with mathematical guarantees of safe and correct -behavior for nuclear reactor operations. Nuclear reactors are quintessential -hybrid cyber-physical systems where continuous neutron kinetics and -thermal-hydraulics interact with discrete control mode decisions and trip -logic. Hybrid systems combine continuous dynamics with discrete mode -transitions, formally expressed as $\dot{x}(t) = f(x(t),q(t),u(t))$ for -continuous states and $q(k+1) = \nu(x(k),q(k),u(k))$ for discrete -transitions. - -If this research is successful, we will be able to do the following: - -\begin{enumerate} - \item \textit{Synthesize written procedures into verified control logic.} - 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. This process uses - structured intermediate representations to bridge natural language and - mathematical logic. Control engineers will be able to generate - mode-switching controllers from regulatory procedures with little formal - methods expertise, reducing barriers to high-assurance control systems. - - \item \textit{Verify continuous control behavior across mode transitions.} - We will develop methods using reachability analysis to ensure continuous - control modes satisfy discrete transition requirements. 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. - - \item \textit{Demonstrate autonomous reactor startup control with safety - guarantees.} We will implement this methodology on a small modular - reactor simulation using industry-standard control hardware. This trial - will include multiple coordinated control modes from cold shutdown through - criticality to power operation on a SmAHTR reactor simulation in a - hardware-in-the-loop experiment. Control engineers will be able to - implement high-assurance autonomous controls on industrial platforms they - already use, enabling users to achieve autonomy without retraining costs - or developing new equipment. -\end{enumerate} - -\section{Limits of Current Practice} - -Nuclear reactor control reveals fundamental verification gaps that motivate -formal hybrid control synthesis. These gaps span current operational -practices, human reliability, and even the most advanced formal methods -attempts to date. - -Current generation nuclear power plants employ over 3,600 active NRC-licensed -reactor operators who hold legal authority to make critical decisions -including departing from regulations during emergencies. This authority is -both necessary and problematic. The Three Mile Island accident demonstrated -how personnel error led to partial meltdown when operators misread confusing -readings and shut off emergency systems. The President's Commission identified -a fundamental ambiguity: operators hold full responsibility without formal -verification they can fulfill this under all conditions. - -Nuclear plant procedures exist in a hierarchy from normal operating procedures -through Emergency Operating Procedures to Severe Accident Management -Guidelines. Despite rigorous development processes including technical -evaluation and simulator validation testing, these procedures fundamentally -lack formal verification. No mathematical proof exists that procedures cover -all possible plant states or that required actions can be completed within -available timeframes. This gap between procedural rigor and mathematical -certainty creates the first major limitation of current practice. - -The division between automated and human-controlled functions reveals the -fundamental hybrid control challenge. Highly automated systems handle reactor -protection and emergency core cooling, while human operators retain strategic -decision-making. Current practice treats continuous plant dynamics and -discrete control logic as separate concerns without formal integration. No -application of hybrid control theory exists that could provide mathematical -guarantees across mode transitions. - -Human factors compound these verification gaps. Multiple independent analyses -show that 70--80\% of all nuclear power plant events are attributed to human -error rather than equipment failures. More significantly, the IAEA concluded -that human error was the root cause of all severe accidents at nuclear power -plants. The persistence of this ratio despite four decades of improvements -suggests fundamental cognitive limitations rather than remediable -deficiencies. - -The Three Mile Island accident provides the definitive case study. When a -pressure-operated relief valve stuck open, instrumentation showed only -commanded position, not actual position. This information gap proved decisive. -When Emergency Core Cooling pumps automatically activated, operators shut them -down based on incorrect assessment. Operators faced over 100 simultaneous -alarms, overwhelming their cognitive capacity. The core suffered 44\% fuel -meltdown before stabilization. - -Human Reliability Analysis methods quantify these limitations. Nominal Human -Error Probabilities stand at 0.01 (1\%) for diagnosis tasks under optimal -conditions. These rates degrade dramatically under accident conditions: -inadequate time increases error probability 10-fold, extreme stress by 5-fold, -high complexity by 5-fold. Under combined adverse conditions, human error -probabilities approach 0.1 to 1.0---essentially guaranteed failure. - -The underlying causes are fundamental and cannot be overcome through training -alone. Response time limitations constrain effectiveness. Visual perception -requires 100-200 milliseconds, decisions 200-400 milliseconds. Reactor -transients evolve in seconds. Protection systems must respond in milliseconds, -100-1000 times faster than humans. Working memory capacity is limited to -7$\pm$2 chunks, explaining why TMI's 100+ alarms exceeded operators' -processing capacity. These are not training failures---they are fundamental -properties of human cognition. - -Recent efforts to apply formal methods to nuclear control show both promise -and remaining gaps. The High Assurance Rigorous Digital Engineering for -Nuclear Safety (HARDENS) project represents the most advanced application to -date. Completed in nine months at a fraction of typical costs, HARDENS -produced a complete Reactor Trip System with full traceability from NRC -requirements through formal specifications to verified binaries. - -The project employed impressive formal methods. FRET handled requirements -elicitation. Cryptol provided executable specifications. SAW performed -verification. Automatic code synthesis generated formally verifiable -implementations. This comprehensive approach demonstrated that formal methods -are technically feasible and economically viable for nuclear protection -systems. - -Despite these accomplishments, HARDENS has a fundamental limitation directly -relevant to our work. The project addressed only discrete digital control -logic without modeling or verifying continuous reactor dynamics. Real reactor -safety depends on interaction between continuous processes---temperature, -pressure, neutron flux---and discrete control decisions. HARDENS verified the -discrete controller in isolation but not the closed-loop hybrid system -behavior. - -Experimental validation presents the second major limitation. HARDENS produced -a demonstrator at Technology Readiness Level 3--4 rather than a -deployment-ready system. The gap between formal verification and actual -deployment involves integration with legacy systems, long-term reliability -under harsh environments, and regulatory acceptance of formal methods as -primary assurance evidence. - -These three converging lines reveal the research imperative. Current practice -lacks formal verification of procedures and mode transitions. Human operators -contribute to 70--80\% of incidents despite continuous improvements, -suggesting fundamental rather than remediable limitations. HARDENS -demonstrated feasibility of formal methods but addressed only discrete logic, -leaving hybrid dynamics unverified. The continuous dynamics of reactor physics -combined with discrete control logic demand hybrid automata or differential -dynamic logic that can verify properties spanning both domains. This gap -defines the research opportunity. - -\section{Research Approach} - -This research will overcome the identified limitations by combining formal -methods from computer science with control theory to build hybrid control -systems that are correct by construction. We accomplish this through three -main thrusts that progress from written procedures to verified implementations. - -Commercial nuclear power operations remain manually controlled despite -significant advances in control systems. The key insight is that procedures -performed by human operators are highly prescriptive and well-documented. -Written procedures in nuclear power are sufficiently detailed that we may -translate them into logical formulae with minimal effort. This translation -forms the foundation of our approach. - -To formalize these procedures, we will use temporal logic, which captures -system behaviors through temporal relations. Linear Temporal Logic provides -four fundamental operators: next ($X$), eventually ($F$), globally ($G$), and -until ($U$). These operators enable precise specification of time-dependent -requirements. - -Consider a nuclear reactor SCRAM requirement: ``If a high temperature alarm -triggers, control rods must immediately insert and remain inserted until -operator reset.'' This natural language statement translates into temporal -logic as: $G(HighTemp \rightarrow X(RodsInserted \wedge (\neg RodsWithdrawn\ -U\ OperatorReset)))$. The specification precisely captures the temporal -relationship between alarm, response, and persistence requirement. - -The most efficient path to accomplish this translation is through NASA's -Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a -specialized requirements language that restricts requirements to easily -understood components while eliminating ambiguity. FRET enforces structure by -requiring all requirements to contain six components: Scope, Condition, -Component, Shall, Timing, and Response. - -FRET provides functionality to check realizability of a system. Realizability -analysis determines whether written requirements are complete by examining the -six structural components. Complete requirements neither conflict with one -another nor leave any behavior undefined. Systems that are not realizable -contain behavioral inconsistencies that represent the physical equivalent of -software bugs. Using FRET during autonomous controller development allows us -to identify and resolve these errors systematically. FRET exports requirements -in temporal logic format compatible with reactive synthesis tools, enabling -the second thrust of our approach. - -Reactive synthesis is an active research field focused on generating discrete -controllers from temporal logic specifications. The term reactive indicates -that the system responds to environmental inputs to produce control outputs. -These synthesized systems are finite in size, where each node represents a -unique discrete state. The connections between nodes, called state -transitions, specify the conditions under which the discrete controller moves -from state to state. This complete mapping constitutes a discrete automaton. - -We will employ state-of-the-art reactive synthesis tools, particularly Strix, -which has demonstrated superior performance in the Reactive Synthesis -Competition through efficient parity game solving algorithms. Strix translates -linear temporal logic specifications into deterministic automata automatically -while maximizing generated automata quality. Once constructed, the automaton -can be straightforwardly implemented using standard programming control flow -constructs. - -The discrete automata representation yields an important theoretical -guarantee. Because the discrete automaton is synthesized entirely through -automated tools from design requirements and operating procedures, we can -prove that the automaton---and therefore our hybrid switching behavior---is -correct by construction. This correctness guarantee is paramount. Mode -switching represents the primary responsibility of human operators in control -rooms today. Human operators possess the advantage of real-time -judgment---when mistakes occur, they can correct them dynamically. Autonomous -control lacks this adaptive advantage. By synthesizing controllers from -logical specifications with guaranteed correctness, we eliminate the -possibility of switching errors. - -While discrete system components will be synthesized with correctness -guarantees, they represent only half of the complete system. The continuous -modes will be developed after discrete automaton construction, leveraging the -automaton structure and transitions to design multiple smaller, specialized -continuous controllers. This progression from discrete to continuous design -addresses a key challenge in hybrid system verification. - -The discrete automaton transitions mark decision points for switching between -continuous control modes and define their strategic objectives. We will -classify three types of high-level continuous controller objectives: -Stabilizing modes maintain the hybrid system within its current discrete mode, -corresponding to steady-state normal operating modes like full-power -load-following control. Transitory modes have the primary goal of -transitioning the hybrid system from one discrete state to another, such as -controlled warm-up procedures. Expulsory modes are specialized transitory -modes with additional safety constraints that ensure the system is directed to -a safe stabilizing mode during failure conditions, such as reactor SCRAM. - -Building continuous modes after constructing discrete automata enables local -controller design focused on satisfying discrete transitions. The primary -challenge in hybrid system verification is ensuring global stability across -transitions. Current techniques struggle with this problem because dynamic -discontinuities complicate verification. This work alleviates these problems -by designing continuous controllers specifically with transitions in mind. By -decomposing continuous modes according to their required behavior at -transition points, we avoid solving trajectories through the entire hybrid -system. - -To ensure continuous modes satisfy their requirements, we will employ three -complementary techniques. Reachability analysis computes the reachable set of -states for a given input set. We will use reachability to define continuous -state ranges at discrete transition boundaries and verify that requirements -are satisfied within continuous modes. Assume-guarantee contracts will be -employed when continuous state boundaries are not explicitly defined. For any -given mode, the input range for reachability analysis is defined by the output -ranges of discrete modes that transition to it. This compositional approach -ensures each continuous controller is prepared for its possible input range. -Barrier certificates will prove that mode transitions are satisfied. Control -barrier functions provide a method to certify safety by establishing -differential inequality conditions that guarantee forward invariance of safe -sets. - -Combining these three techniques will enable us to prove that continuous -components satisfy discrete requirements and thus complete system behavior. To -demonstrate this methodology, we will develop an autonomous startup controller -for a Small Modular Advanced High Temperature Reactor (SmAHTR). SmAHTR -represents an ideal test case with well-documented startup procedures that -must transition through multiple distinct operational modes: initial cold -conditions, controlled heating to operating temperature, approach to -criticality, low-power physics testing, and power ascension to full operating -capacity. - -We have already developed a high-fidelity SmAHTR model in Simulink that -captures the thermal-hydraulic and neutron kinetics behavior. The synthesized -hybrid controller will be implemented on an Emerson Ovation control system -platform, which is representative of industry-standard control hardware. The -Advanced Reactor Cyber Analysis and Development Environment (ARCADE) suite -will serve as the integration layer, managing real-time communication between -the Simulink simulation and the Ovation controller. This hardware-in-the-loop -configuration enables validation of the controller implementation on actual -industrial control equipment. - -\section{Metrics of Success} - -This research will be measured by advancement through Technology Readiness -Levels, progressing from fundamental concepts to validated prototype -demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where -system components operate successfully in a relevant laboratory environment. - -TRLs provide the ideal success metric because they explicitly measure the gap -between academic proof-of-concept and practical deployment. This gap is -precisely what our work aims to bridge. TRLs capture both theoretical rigor -and practical feasibility simultaneously. The nuclear industry already uses -TRLs for technology assessment, making this metric directly relevant to -potential adopters. - -Moving from current state (TRL 2--3) to target (TRL 5) requires achieving -three intermediate levels. TRL 3 demonstrates that each component works in -isolation. Startup procedures must be translated into temporal logic -specifications that pass realizability analysis. A discrete automaton must be -synthesized with interpretable structure. At least one continuous controller -must be designed with verified transition requirements. This level proves the -fundamental approach on simplified sequences. - -TRL 4 demonstrates a complete integrated hybrid controller in simulation. All -startup procedures must be formalized with continuous controllers existing for -all discrete modes. Verification must be complete for all mode transitions. -The integrated controller must execute complete startup sequences with zero -safety violations. This level proves that formal correctness guarantees can be -maintained throughout system integration. - -TRL 5 demonstrates the verified controller on industrial control hardware -through hardware-in-the-loop testing. The discrete automaton must be -implemented on Emerson Ovation hardware and verified to match synthesized -specifications exactly. The ARCADE interface must establish stable real-time -communication between Ovation hardware and SmAHTR simulation. Complete -autonomous startup sequences must execute across the full operational -envelope. This level proves that the methodology produces verified controllers -implementable with current technology. - -This research succeeds if it achieves TRL 5, establishing both theoretical -validity and practical feasibility. Success provides a clear pathway for -nuclear industry adoption and broader application to safety-critical -autonomous systems. - -\section{Broader Impacts} - -Nuclear power presents both a compelling application domain and an urgent -economic challenge. Recent interest in powering artificial intelligence -infrastructure has renewed focus on small modular reactors for hyperscale -datacenters. According to the U.S. Energy Information Administration, advanced -nuclear power entering service in 2027 is projected to cost \$88.24 per -megawatt-hour. With datacenter electricity demand projected to reach 1,050 -terawatt-hours annually by 2030, operations and maintenance costs represent -approximately 23--30\% of total levelized cost, translating to \$21--28 -billion annually for projected datacenter demand. - -This research directly addresses the multi-billion dollar O\&M cost challenge. -Current nuclear operations require full control room staffing for each -reactor. These staffing requirements drive high O\&M costs, particularly for -smaller reactor designs where the same overhead must be spread across lower -power output. The economic burden threatens the viability of next-generation -nuclear technologies. - -By synthesizing provably correct hybrid controllers, we can automate routine -operational sequences that currently require constant human oversight. This -enables a fundamental shift from direct operator control to supervisory -monitoring where operators oversee multiple autonomous reactors rather than -manually controlling individual units. The transition fundamentally changes -the economics of nuclear operations. - -The correct-by-construction methodology is critical for this transition. -Traditional automation approaches cannot provide sufficient safety guarantees -for nuclear applications where regulatory requirements and public safety -concerns demand the highest levels of assurance. By formally verifying both -discrete mode-switching logic and continuous control behavior, this research -will produce controllers with mathematical proofs of correctness. These -guarantees enable automation to safely handle routine operations that -currently require human operators to follow written procedures. - -Small modular reactors represent an ideal deployment target. Nuclear -Regulatory Commission certification requires extensive documentation of -control procedures, operational requirements, and safety analyses written in -structured natural language. These regulatory documents can be translated into -temporal logic specifications using FRET, synthesized into discrete switching -logic using reactive synthesis tools, and verified using reachability analysis -and barrier certificates. The infrastructure of requirements is already -complete as part of licensing. This creates a direct pathway from existing -regulatory documentation to formally verified autonomous controllers. - -Beyond nuclear applications, this research will establish a generalizable -framework for autonomous control of safety-critical systems. The methodology -of translating operational procedures into formal specifications, synthesizing -discrete switching logic, and verifying continuous mode behavior applies to -any hybrid system with documented operational requirements. Potential -applications include chemical process control, aerospace systems, and -autonomous transportation. These domains share similar economic and safety -considerations that favor increased autonomy with provable correctness -guarantees. By demonstrating this approach in nuclear power---one of the most -regulated and safety-critical domains---this research will establish both -technical feasibility and regulatory pathways for broader adoption across -critical infrastructure. - -\newpage - -% REFERENCES CITED -\section*{References Cited} - -\begin{thebibliography}{99} - -\bibitem{10CFR55} -U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.'' -\textit{Code of Federal Regulations}, 2024. - -\bibitem{princeton} -Princeton University. ``Nuclear Reactor Operator Training.'' -\textit{Princeton Plasma Physics Laboratory}, 2023. - -\bibitem{Kemeny1979} -J. G. Kemeny et al. ``Report of the President's Commission on the Accident -at Three Mile Island.'' U.S. Government Printing Office, October 1979. - -\bibitem{NUREG-0899} -U.S. Nuclear Regulatory Commission. ``Guidelines for the Preparation of -Emergency Operating Procedures.'' NUREG-0899, August 1982. - -\bibitem{DOE-HDBK-1028-2009} -U.S. Department of Energy. ``Human Performance Improvement Handbook.'' -DOE-HDBK-1028-2009, June 2009. - -\bibitem{WNA2020} -World Nuclear Association. ``Safety of Nuclear Power Reactors.'' -\textit{World Nuclear Association Information Library}, 2020. - -\bibitem{IAEA-severe-accidents} -International Atomic Energy Agency. ``Lessons Learned from Severe Nuclear -Accidents.'' IAEA Technical Report, 2016. - -\bibitem{Wang2025} -Y. Wang et al. ``Human Error Analysis of 190 Events at Chinese Nuclear -Power Plants from 2007-2020.'' \textit{Nuclear Engineering and Design}, -vol. 395, 2025. - -\bibitem{Kiniry2022} -J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear -Safety (HARDENS).'' NRC Final Technical Report ML22326A307, September 2022. - -\bibitem{eia_lcoe_2022} -U.S. Energy Information Administration. ``Levelized Costs of New Generation -Resources in the Annual Energy Outlook 2022.'' Report, March 2022. - -\bibitem{eesi_datacenter_2024} -Environmental and Energy Study Institute. ``Data Center Energy Needs are -Upending Power Grids and Threatening the Climate.'' Web article, 2024. - -\end{thebibliography} - -\end{document}e transitions occur safely and as defined by the +certificates to prove that mode transitions occur safely and as defined by the deterministic automata. This compositional approach enables local verification of continuous modes without requiring global trajectory analysis across the entire hybrid system. We will demonstrate this methodology by developing an @@ -692,142 +152,71 @@ If this research is successful, we will be able to do the following: achieve autonomy without retraining costs or developing new equipment. \end{enumerate} -% -% % IMPACT PARAGRAPH Innovation -% The innovation is unifying discrete synthesis and continuous verification to -% enable end-to-end correctness guarantees for hybrid systems. -% % Outcome Impact -% If successful, control engineers will be able to create autonomous controllers from existing -% procedures with mathematical proof of correct behavior, making high-assurance -% autonomous control practical for safety-critical applications. -% % Impact/Pay-off -% This capability is essential for economic viability of next-generation nuclear -% power. Small modular reactors represent a promising solution to growing energy -% demands, but success depends on reducing per-megawatt operating costs through -% increased autonomy. This research will provide the tools to achieve that autonomy -% while maintaining the exceptional safety record required by the nuclear industry. +\section{State of the Art and Limits of Current Practice} -\section{Limits of Current Practice} -Current generation nuclear power plants employ over 3,600 active NRC-licensed -reactor operators who hold legal authority to make critical decisions -including departing from regulations during emergencies. This authority is -both necessary and problematic, and has caused major nuclear accidents such as -the Three Mile Island Accident. The Three Mile Island accident demonstrated -how personnel error led to partial meltdown when operators misread confusing -readings and shut off emergency systems. The President's Commission identified -a fundamental ambiguity: operators hold full responsibility without formal -verification they can fulfill this under all conditions. +Automation of some nuclear power operations is already performed today. Highly +automated systems handle reactor protection and emergency core cooling, while +human operators retain strategic decision-making. Autonomous systems are trusted +to handle emergency situations that are considered terminal operations, but +otherwise introduce too much risk to reactor operations. Contrary to this notion +is the fact that 70--80\% of all nuclear power plant events are attributed to +human error rather than equipment failures. The persistence of this ratio despite +four decades of improvements to procedures and control rooms suggests +fundamental cognitive limitations rather than remediable deficiencies. -Nuclear plant procedures exist in a hierarchy from normal operating procedures -through Emergency Operating Procedures to Severe Accident Management -Guidelines. Despite rigorous development processes including technical -evaluation and simulator validation testing, these procedures fundamentally -lack formal verification. No mathematical proof exists that procedures cover -all possible plant states or that required actions can be completed within -available timeframes. +The Nuclear Regulatory Commission has recognized that introducing automation +into the control room is the only way forward. Recent efforts to apply formal +methods to nuclear control have shown both promise and remaining gaps. The High +Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project +represents the most advanced application to date. HARDENS produced a complete +Reactor Trip System with full traceability from NRC requirements through formal +specifications to verified binaries of a controller implementation. The project +employed formal methods along the control design stack. This comprehensive +approach demonstrated that formal methods may be technically feasible and +economically viable for nuclear protection systems. -% The division between automated and human-controlled functions reveals the -% fundamental hybrid control challenge. Highly automated systems handle reactor -% protection and emergency core cooling, while human operators retain strategic -% decision-making. Current practice treats continuous plant dynamics and -% discrete control logic as separate concerns without formal integration. No -% application of hybrid control theory exists that could provide mathematical -% guarantees across mode transitions. -% -Human factors compound these verification gaps. 70--80\% of all nuclear power -plant events are attributed to human error rather than equipment failures. More -significantly, the IAEA concluded that human error was the root cause of all -severe accidents at nuclear power plants. The persistence of this ratio despite -four decades of improvements suggests fundamental cognitive limitations rather -than remediable deficiencies. - -The Three Mile Island accident provides the definitive case study. When a -pressure-operated relief valve stuck open, instrumentation showed only -commanded position, not actual position. This information gap proved decisive. -When Emergency Core Cooling pumps automatically activated, operators shut them -down based on incorrect assessment. Operators faced over 100 simultaneous -alarms, overwhelming their cognitive capacity. The core suffered 44\% fuel -meltdown before stabilization. - -Human Reliability Analysis methods quantify these limitations. Nominal Human -Error Probabilities stand at 0.01 (1\%) for diagnosis tasks under optimal -conditions. These rates degrade dramatically under accident conditions: -inadequate time increases error probability 10-fold, extreme stress by 5-fold, -high complexity by 5-fold. Under combined adverse conditions, human error -probabilities approach 0.1 to 1.0---essentially guaranteed failure. - -The underlying causes are fundamental and cannot be overcome through training -alone. Response time limitations constrain effectiveness. Visual perception -requires 100-200 milliseconds, decisions 200-400 milliseconds. Reactor -transients evolve in seconds. Protection systems must respond in milliseconds, -100-1000 times faster than humans. Working memory capacity is limited to -7$\pm$2 chunks, explaining why TMI's 100+ alarms exceeded operators' -processing capacity. These are not training failures---they are fundamental -properties of human cognition. - -Recent efforts to apply formal methods to nuclear control show both promise -and remaining gaps. The High Assurance Rigorous Digital Engineering for -Nuclear Safety (HARDENS) project represents the most advanced application to -date. Completed in nine months at a fraction of typical costs, HARDENS -produced a complete Reactor Trip System with full traceability from NRC -requirements through formal specifications to verified binaries. - -The project employed impressive formal methods. FRET handled requirements -elicitation. Cryptol provided executable specifications. SAW performed -verification. Automatic code synthesis generated formally verifiable -implementations. This comprehensive approach demonstrated that formal methods -are technically feasible and economically viable for nuclear protection -systems. - -Despite these accomplishments, HARDENS has a fundamental limitation directly -relevant to our work. The project addressed only discrete digital control -logic without modeling or verifying continuous reactor dynamics. Real reactor -safety depends on interaction between continuous processes---temperature, -pressure, neutron flux---and discrete control decisions. HARDENS verified the -discrete controller in isolation but not the closed-loop hybrid system -behavior. - -Experimental validation presents the second major limitation. HARDENS produced -a demonstrator at Technology Readiness Level 3--4 rather than a -deployment-ready system. The gap between formal verification and actual -deployment involves integration with legacy systems, long-term reliability -under harsh environments, and regulatory acceptance of formal methods as -primary assurance evidence. - -These three converging lines reveal the research imperative. Current practice -lacks formal verification of procedures and mode transitions. Human operators -contribute to 70--80\% of incidents despite continuous improvements, -suggesting fundamental rather than remediable limitations. HARDENS -demonstrated feasibility of formal methods but addressed only discrete logic, -leaving hybrid dynamics unverified. The continuous dynamics of reactor physics -combined with discrete control logic demand hybrid automata or differential -dynamic logic that can verify properties spanning both domains. This gap -defines the research opportunity. +But despite these accomplishments, HARDENS has a fundamental limitation directly +relevant to our work. The project addressed only discrete digital control logic +without modeling or verifying continuous reactor dynamics. Real reactor safety +depends on interaction between continuous processes and discrete control +decisions. HARDENS verified the discrete controller in isolation but not the +closed-loop hybrid system behavior. \section{Research Approach} This research will overcome the identified limitations by combining formal methods from computer science with control theory to build hybrid control systems that are correct by construction. We accomplish this through three -main thrusts that progress from written procedures to verified implementations. +main thrusts: + +\begin{enumerate} + + \item We will translate natural language procedures and + requirements into temporal logic specifications using the Formal Requirements + Elicitation Tool (FRET). + + \item We will synthesize these temporal logic + specifications into the discrete component of the hybrid controller using + reactive synthesis. + + \item We will build continuous control modes that satisfy discrete controller + transition requirements. + +\end{enumerate} Commercial nuclear power operations remain manually controlled despite significant advances in control systems. The key insight is that procedures -performed by human operators are highly prescriptive and well-documented. -Written procedures in nuclear power are sufficiently detailed that we may -translate them into logical formulae with minimal effort. This To formalize -these procedures, we will use temporal logic, which captures system behaviors -through temporal relations. Linear Temporal Logic provides four fundamental -operators: next ($X$), eventually ($F$), globally ($G$), and until ($U$). These -operators enable precise specification of time-dependent requirements. - -These specifications precisely define behavior in a way that natural language is -not able to reproduce. The most efficient path to accomplish this translation is -through NASA's Formal Requirements Elicitation Tool (FRET). FRET employs -FRETish, a specialized requirements language that restricts requirements to -easily understood components while eliminating ambiguity. FRET enforces -structure by requiring all requirements to contain six components: Scope, -Condition, Component, Shall, Timing, and Response. +performed by human operators are highly prescriptive and well-documented. To +formalize these procedures, we will use temporal logic, which captures system +behaviors through temporal relations. Linear Temporal Logic provides four +fundamental operators: next ($X$), eventually ($F$), globally ($G$), and until +($U$). These operators enable precise specification of time-dependent +requirements. The most efficient path to accomplish this translation is through +NASA's Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a +specialized requirements language that restricts requirements to easily +understood components while eliminating ambiguity. FRET enforces structure by +requiring all requirements to contain six components: Scope, Condition, +Component, Shall, Timing, and Response. FRET provides functionality to check realizability of a system. Realizability analysis determines whether written requirements are complete by examining the @@ -847,32 +236,28 @@ unique discrete state. The connections between nodes, called state transitions, specify the conditions under which the discrete controller moves from state to state. This complete mapping constitutes a discrete automaton. -We will employ state-of-the-art reactive synthesis tools, particularly Strix, -which has demonstrated superior performance in the Reactive Synthesis -Competition through efficient parity game solving algorithms. Strix translates -linear temporal logic specifications into deterministic automata automatically -while maximizing generated automata quality. Once constructed, the automaton -can be straightforwardly implemented using standard programming control flow -constructs. - -The discrete automata representation yields an important theoretical +We will employ reactive synthesis tools which translate linear temporal logic +specifications into deterministic automata automatically while maximizing +generated automata quality. Once constructed, the automaton can be +straightforwardly implemented using standard programming control flow +constructs. The discrete automata representation yields an important theoretical guarantee. Because the discrete automaton is synthesized entirely through automated tools from design requirements and operating procedures, we can prove that the automaton---and therefore our hybrid switching behavior---is -correct by construction. This correctness guarantee is paramount. Mode -switching represents the primary responsibility of human operators in control -rooms today. Human operators possess the advantage of real-time -judgment---when mistakes occur, they can correct them dynamically. Autonomous -control lacks this adaptive advantage. By synthesizing controllers from -logical specifications with guaranteed correctness, we eliminate the -possibility of switching errors. +correct by construction. + +This correctness guarantee is paramount. Mode switching represents the primary +responsibility of human operators in control rooms today. Human operators +possess the advantage of real-time judgment. When mistakes occur, they can +correct them dynamically. Autonomous control lacks this adaptive advantage. By +synthesizing controllers from logical specifications with guaranteed +correctness, we eliminate the possibility of switching errors. While discrete system components will be synthesized with correctness guarantees, they represent only half of the complete system. The continuous modes will be developed after discrete automaton construction, leveraging the automaton structure and transitions to design multiple smaller, specialized -continuous controllers. This progression from discrete to continuous design -addresses a key challenge in hybrid system verification. +continuous controllers. The discrete automaton transitions mark decision points for switching between continuous control modes and define their strategic objectives. We will @@ -897,14 +282,14 @@ system. To ensure continuous modes satisfy their requirements, we will employ three complementary techniques. Reachability analysis computes the reachable set of -states for a given input set. We will use reachability to define continuous -state ranges at discrete transition boundaries and verify that requirements -are satisfied within continuous modes. Assume-guarantee contracts will be +states for a given input set. We will use reachability when continuous +state ranges at discrete transition boundaries are defined and verify that +continuous modes only can reach such defined ranges. Otherwise, assume-guarantee contracts will be employed when continuous state boundaries are not explicitly defined. For any given mode, the input range for reachability analysis is defined by the output ranges of discrete modes that transition to it. This compositional approach ensures each continuous controller is prepared for its possible input range. -Barrier certificates will prove that mode transitions are satisfied. Control +Finally, barrier certificates will prove that mode transitions are satisfied. Control barrier functions provide a method to certify safety by establishing differential inequality conditions that guarantee forward invariance of safe sets. @@ -917,60 +302,38 @@ represents an ideal test case with well-documented startup procedures that must transition through multiple distinct operational modes: initial cold conditions, controlled heating to operating temperature, approach to criticality, low-power physics testing, and power ascension to full operating -capacity. +capacity. We have access to an already developed high-fidelity SmAHTR model in Simulink that +captures the thermal-hydraulic and neutron kinetics behavior. -We have already developed a high-fidelity SmAHTR model in Simulink that -captures the thermal-hydraulic and neutron kinetics behavior. The synthesized -hybrid controller will be implemented on an Emerson Ovation control system -platform, which is representative of industry-standard control hardware. The -Advanced Reactor Cyber Analysis and Development Environment (ARCADE) suite -will serve as the integration layer, managing real-time communication between -the Simulink simulation and the Ovation controller. This hardware-in-the-loop -configuration enables validation of the controller implementation on actual -industrial control equipment. +The synthesized hybrid controller will be implemented on an Emerson Ovation +control system platform, which is representative of industry-standard control +hardware. This control system will be used in a hardware-in-the-loop simulation, +where the Advanced Reactor Cyber Analysis and Development Environment +(ARCADE) suite will serve as the integration layer. This +hardware-in-the-loop configuration enables validation of the controller +implementation on actual industrial control equipment. \section{Metrics of Success} -This research will be measured by advancement through Technology Readiness -Levels, progressing from fundamental concepts to validated prototype -demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where -system components operate successfully in a relevant laboratory environment. +This research will be measured by advancement through Technology Readiness +Levels, progressing from fundamental concepts to validated prototype +demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where system +components operate successfully in a relevant laboratory environment. TRLs +provide the ideal success metric because they explicitly measure the gap between +academic proof-of-concept and practical deployment. This gap is precisely what +our work aims to bridge. TRLs capture both theoretical rigor and practical +feasibility simultaneously. The nuclear industry already uses TRLs for +technology assessment, making this metric directly relevant to potential +adopters. -TRLs provide the ideal success metric because they explicitly measure the gap -between academic proof-of-concept and practical deployment. This gap is -precisely what our work aims to bridge. TRLs capture both theoretical rigor -and practical feasibility simultaneously. The nuclear industry already uses -TRLs for technology assessment, making this metric directly relevant to -potential adopters. - -Moving from current state (TRL 2--3) to target (TRL 5) requires achieving -three intermediate levels. TRL 3 demonstrates that each component works in -isolation. Startup procedures must be translated into temporal logic -specifications that pass realizability analysis. A discrete automaton must be -synthesized with interpretable structure. At least one continuous controller -must be designed with verified transition requirements. This level proves the -fundamental approach on simplified sequences. - -TRL 4 demonstrates a complete integrated hybrid controller in simulation. All -startup procedures must be formalized with continuous controllers existing for -all discrete modes. Verification must be complete for all mode transitions. -The integrated controller must execute complete startup sequences with zero -safety violations. This level proves that formal correctness guarantees can be -maintained throughout system integration. - -TRL 5 demonstrates the verified controller on industrial control hardware -through hardware-in-the-loop testing. The discrete automaton must be -implemented on Emerson Ovation hardware and verified to match synthesized -specifications exactly. The ARCADE interface must establish stable real-time -communication between Ovation hardware and SmAHTR simulation. Complete -autonomous startup sequences must execute across the full operational -envelope. This level proves that the methodology produces verified controllers -implementable with current technology. - -This research succeeds if it achieves TRL 5, establishing both theoretical -validity and practical feasibility. Success provides a clear pathway for -nuclear industry adoption and broader application to safety-critical -autonomous systems. +Moving from current state (TRL 2--3) to target (TRL 5) requires progressing +through component isolation, system integration, and hardware validation. By +reaching TRL 5, we will have demonstrated a complete autonomous hybrid +controller operating on industrial control hardware through hardware-in-the-loop +testing. Achieving TRL 5 establishes both theoretical validity and practical +feasibility, proving that the methodology produces verified controllers +implementable with current technology and providing a clear pathway for nuclear +industry adoption and broader application to safety-critical autonomous systems. \section{Broader Impacts} @@ -984,19 +347,17 @@ terawatt-hours annually by 2030, operations and maintenance costs represent approximately 23--30\% of total levelized cost, translating to \$21--28 billion annually for projected datacenter demand. -This research directly addresses the multi-billion dollar O\&M cost challenge. -Current nuclear operations require full control room staffing for each -reactor. These staffing requirements drive high O\&M costs, particularly for -smaller reactor designs where the same overhead must be spread across lower -power output. The economic burden threatens the viability of next-generation -nuclear technologies. - -By synthesizing provably correct hybrid controllers, we can automate routine -operational sequences that currently require constant human oversight. This -enables a fundamental shift from direct operator control to supervisory -monitoring where operators oversee multiple autonomous reactors rather than -manually controlling individual units. The transition fundamentally changes -the economics of nuclear operations. +This research directly addresses the multi-billion dollar O\&M cost challenge. +Current nuclear operations require full control room staffing for each reactor. +These staffing requirements drive high O\&M costs, particularly for smaller +reactor designs where the same overhead must be spread across lower power +output. The economic burden threatens the viability of next-generation nuclear +technologies. But, by synthesizing provably correct hybrid controllers, we can +automate routine operational sequences that currently require constant human +oversight. This enables a change from direct operator control to +supervisory monitoring where operators oversee multiple autonomous reactors +rather than manually controlling individual units. The transition fundamentally +changes the economics of nuclear operations. The correct-by-construction methodology is critical for this transition. Traditional automation approaches cannot provide sufficient safety guarantees @@ -1007,27 +368,16 @@ will produce controllers with mathematical proofs of correctness. These guarantees enable automation to safely handle routine operations that currently require human operators to follow written procedures. -Small modular reactors represent an ideal deployment target. Nuclear -Regulatory Commission certification requires extensive documentation of -control procedures, operational requirements, and safety analyses written in -structured natural language. These regulatory documents can be translated into -temporal logic specifications using FRET, synthesized into discrete switching -logic using reactive synthesis tools, and verified using reachability analysis -and barrier certificates. The infrastructure of requirements is already -complete as part of licensing. This creates a direct pathway from existing -regulatory documentation to formally verified autonomous controllers. - -Beyond nuclear applications, this research will establish a generalizable -framework for autonomous control of safety-critical systems. The methodology -of translating operational procedures into formal specifications, synthesizing -discrete switching logic, and verifying continuous mode behavior applies to -any hybrid system with documented operational requirements. Potential -applications include chemical process control, aerospace systems, and -autonomous transportation. These domains share similar economic and safety -considerations that favor increased autonomy with provable correctness -guarantees. By demonstrating this approach in nuclear power---one of the most -regulated and safety-critical domains---this research will establish both -technical feasibility and regulatory pathways for broader adoption across +Beyond nuclear applications, this research will establish a generalizable +framework for autonomous control of safety-critical systems. The methodology of +translating operational procedures into formal specifications, synthesizing +discrete switching logic, and verifying continuous mode behavior applies to any +hybrid system with documented operational requirements. Potential applications +include chemical process control, aerospace systems, and autonomous +transportation. These domains share similar economic and safety considerations +that favor increased autonomy with provable correctness guarantees. By +demonstrating this approach in nuclear power this research will establish both +technical feasibility and regulatory pathways for broader adoption across critical infrastructure. \newpage @@ -1040,10 +390,6 @@ critical infrastructure. U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.'' \textit{Code of Federal Regulations}, 2024. -\bibitem{princeton} -Princeton University. ``Nuclear Reactor Operator Training.'' -\textit{Princeton Plasma Physics Laboratory}, 2023. - \bibitem{Kemeny1979} J. G. Kemeny et al. ``Report of the President's Commission on the Accident at Three Mile Island.'' U.S. Government Printing Office, October 1979. @@ -1060,18 +406,9 @@ DOE-HDBK-1028-2009, June 2009. World Nuclear Association. ``Safety of Nuclear Power Reactors.'' \textit{World Nuclear Association Information Library}, 2020. -\bibitem{IAEA-severe-accidents} -International Atomic Energy Agency. ``Lessons Learned from Severe Nuclear -Accidents.'' IAEA Technical Report, 2016. - -\bibitem{Wang2025} -Y. Wang et al. ``Human Error Analysis of 190 Events at Chinese Nuclear -Power Plants from 2007-2020.'' \textit{Nuclear Engineering and Design}, -vol. 395, 2025. - \bibitem{Kiniry2022} J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear -Safety (HARDENS).'' NRC Final Technical Report ML22326A307, September 2022. +Safety (HARDENS).'' NRC Final Technical Report ML22326A307, October 2022. \bibitem{eia_lcoe_2022} U.S. Energy Information Administration. ``Levelized Costs of New Generation @@ -1083,4 +420,3 @@ Upending Power Grids and Threatening the Climate.'' Web article, 2024. \end{thebibliography} -\end{document}