Auto sync: 2025-10-27 12:34:41 (15 files changed)
M .task/backlog.data M .task/pending.data M .task/undo.data A Writing/ERLM/SaboRisksAndContingencies.pdf M Writing/ERLM/broader-impacts/v1.tex M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls
This commit is contained in:
parent
2b8232a17f
commit
59e3923cd2
@ -205,3 +205,4 @@
|
||||
{"description":"Make one-slide about Ovation Research connection for Emerson CEO visit","due":"20251024T040000Z","entry":"20251024T151943Z","modified":"20251024T151954Z","priority":"H","start":"20251024T151954Z","status":"pending","uuid":"882115bd-e94a-4a5d-a22f-5b142a87d77e"}
|
||||
{"description":"Check When2Meet and schedule meeting","due":"20251024T040000Z","end":"20251024T210105Z","entry":"20251023T161642Z","modified":"20251024T210105Z","project":"Internship","status":"completed","uuid":"bac970fa-0e14-4f40-93d0-287859e8ab0b"}
|
||||
{"description":"Make one-slide about Ovation Research connection for Emerson CEO visit","due":"20251024T040000Z","end":"20251024T210105Z","entry":"20251024T151943Z","modified":"20251024T210105Z","priority":"H","status":"completed","uuid":"882115bd-e94a-4a5d-a22f-5b142a87d77e"}
|
||||
{"description":"RnC Assumptions Excercise","entry":"20251021T200919Z","modified":"20251027T144045Z","project":"ERLM","start":"20251027T144045Z","status":"pending","uuid":"c010f099-d235-4243-974b-ccbcba4e75ba","tags":["writing"]}
|
||||
|
||||
@ -40,7 +40,7 @@
|
||||
[description:"RA What is reachability, barrier certs" entry:"1761077262" modified:"1761079200" project:"Thesis" status:"pending" tags:"whiteboard,writing" tags_whiteboard:"x" tags_writing:"x" uuid:"95a11f85-7606-4cc1-9efa-4a7ef19c9f36"]
|
||||
[description:"RA Emerson Ovation Subsection" entry:"1761077284" modified:"1761079200" project:"Thesis" status:"pending" tags:"whiteboard,writing" tags_whiteboard:"x" tags_writing:"x" uuid:"5d4627a4-cfb6-4e0e-95ef-d9f557d1a717"]
|
||||
[description:"BI Reactor operator shortage, human factors limits" entry:"1761077306" modified:"1761079200" project:"Thesis" status:"pending" tags:"whiteboard,writing" tags_whiteboard:"x" tags_writing:"x" uuid:"7f7fbf5c-1ae8-4abc-9488-fa66e7b3f958"]
|
||||
[description:"RnC Assumptions Excercise" entry:"1761077359" modified:"1761077359" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"c010f099-d235-4243-974b-ccbcba4e75ba"]
|
||||
[description:"RnC Assumptions Excercise" entry:"1761077359" modified:"1761576045" project:"ERLM" start:"1761576045" status:"pending" tags:"writing" tags_writing:"x" uuid:"c010f099-d235-4243-974b-ccbcba4e75ba"]
|
||||
[description:"Come up with a toy problem for Research Approach" entry:"1761077394" modified:"1761079200" project:"Thesis" status:"pending" tags:"brainstorming" tags_brainstorming:"x" uuid:"2c537727-f404-44d3-9442-7113eb9f2362"]
|
||||
[description:"Triage Lees comments on research approach" entry:"1761078828" modified:"1761079200" project:"Thesis" status:"pending" uuid:"d334e98d-df5c-48ba-9c5c-b8a2da9fbd26"]
|
||||
[description:"Find Oklo recruiter" entry:"1761078940" modified:"1761078940" status:"pending" uuid:"25581dec-d1ad-407e-86d0-ec08de7a6e46"]
|
||||
|
||||
@ -727,3 +727,7 @@ time 1761339665
|
||||
old [description:"Make one-slide about Ovation Research connection for Emerson CEO visit" due:"1761278400" entry:"1761319183" modified:"1761319194" priority:"H" start:"1761319194" status:"pending" uuid:"882115bd-e94a-4a5d-a22f-5b142a87d77e"]
|
||||
new [description:"Make one-slide about Ovation Research connection for Emerson CEO visit" due:"1761278400" end:"1761339665" entry:"1761319183" modified:"1761339665" priority:"H" status:"completed" uuid:"882115bd-e94a-4a5d-a22f-5b142a87d77e"]
|
||||
---
|
||||
time 1761576045
|
||||
old [description:"RnC Assumptions Excercise" entry:"1761077359" modified:"1761077359" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"c010f099-d235-4243-974b-ccbcba4e75ba"]
|
||||
new [description:"RnC Assumptions Excercise" entry:"1761077359" modified:"1761576045" project:"ERLM" start:"1761576045" status:"pending" tags:"writing" tags_writing:"x" uuid:"c010f099-d235-4243-974b-ccbcba4e75ba"]
|
||||
---
|
||||
|
||||
BIN
Writing/ERLM/SaboRisksAndContingencies.pdf
Normal file
BIN
Writing/ERLM/SaboRisksAndContingencies.pdf
Normal file
Binary file not shown.
@ -1,4 +1,4 @@
|
||||
\subsection{Broader Impacts}
|
||||
\section{Broader Impacts}
|
||||
|
||||
Nuclear power presents both a compelling application domain and an urgent
|
||||
economic challenge. Recent interest in powering artificial intelligence
|
||||
|
||||
@ -1,18 +1,65 @@
|
||||
\relax
|
||||
\bibstyle{unsrt}
|
||||
\providecommand \oddpage@label [2]{}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Objectives}{2}{}\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 }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
|
||||
\citation{10CFR55}
|
||||
\citation{princeton}
|
||||
\citation{Kemeny1979}
|
||||
\citation{Kemeny1979}
|
||||
\citation{NUREG-0899}
|
||||
\citation{10CFR55}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}\protected@file@percent }
|
||||
\citation{DOE-HDBK-1028-2009,WNA2020}
|
||||
\citation{IAEA-severe-accidents}
|
||||
\citation{Wang2025}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
|
||||
\citation{Kemeny1979}
|
||||
\citation{NUREG-CR-6883}
|
||||
\citation{NUREG-2114}
|
||||
\citation{Rasmussen1983}
|
||||
\citation{Miller1956}
|
||||
\citation{Reason1990}
|
||||
\citation{Kiniry2022}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}Rigorous Digital Engineering Demonstrated Feasibility}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Comprehensive Formal Methods Toolkit Provided Verification}{5}{}\protected@file@percent }
|
||||
\citation{Kiniry2022}
|
||||
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.3}Critical Limitation: Discrete Control Logic Only}{6}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.4}Experimental Validation Gap Limits Technology Readiness}{6}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Research Imperative: Formal Hybrid Control Synthesis}{7}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{8}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{9}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{10}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{12}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{13}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{13}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{13}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{14}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{14}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{15}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{16}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{17}{}\protected@file@percent }
|
||||
\citation{eia_lcoe_2022}
|
||||
\citation{eesi_datacenter_2024}
|
||||
\citation{eia_lcoe_2022}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{18}{}\protected@file@percent }
|
||||
\bibdata{references}
|
||||
\bibcite{10CFR55}{1}
|
||||
\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}
|
||||
\bibcite{IAEA-severe-accidents}{6}
|
||||
\bibcite{Wang2025}{7}
|
||||
\bibcite{NUREG-CR-6883}{8}
|
||||
\bibcite{NUREG-2114}{9}
|
||||
\bibcite{Rasmussen1983}{10}
|
||||
\bibcite{Miller1956}{11}
|
||||
\bibcite{Reason1990}{12}
|
||||
\bibcite{Kiniry2022}{13}
|
||||
\bibcite{eia_lcoe_2022}{14}
|
||||
\bibcite{eesi_datacenter_2024}{15}
|
||||
\@writefile{toc}{\contentsline {section}{References}{20}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{22}
|
||||
|
||||
@ -1,11 +1,22 @@
|
||||
# Fdb version 4
|
||||
["pdflatex"] 1760994767.73072 "main.tex" "main.pdf" "main" 1760994768.58948 0
|
||||
["bibtex main"] 1761582767.74064 "main.aux" "main.bbl" "main" 1761582781.96291 0
|
||||
"./references.bib" 1760562704.16405 17887 8c959c4bb228b5a8c44fd08ed0751b05 ""
|
||||
"/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
|
||||
"main.aux" 1761582781.75348 4309 2fe6e70a469147f9fa7894d181c11730 "pdflatex"
|
||||
(generated)
|
||||
"main.bbl"
|
||||
"main.blg"
|
||||
(rewritten before read)
|
||||
["pdflatex"] 1761582780.88005 "main.tex" "main.pdf" "main" 1761582781.96318 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 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm" 1136768653 2228 e564491c42a4540b5ebb710a75ff306c ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm" 1136768653 4480 10409ed8bab5aea9ec9a78028b763919 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b ""
|
||||
@ -18,15 +29,28 @@
|
||||
"/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/cm/cmtt12.tfm" 1136768653 772 9a936b7f5e2ff0557fce0f62822f0bbf ""
|
||||
"/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/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a ""
|
||||
"/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/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca ""
|
||||
"/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 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf" 1136768653 1384 6ac0f8b839230f5d9389287365b243c0 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 ""
|
||||
"/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 ""
|
||||
@ -211,10 +235,16 @@
|
||||
"/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 ""
|
||||
"broader-impacts/v1.tex" 1761582743.25611 4913 f040011f0dbfa050cad013bb8737b473 ""
|
||||
"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 ""
|
||||
"goals-and-outcomes/v6.tex" 1759931957.10694 6070 286ca847b1aac31431e0658cd2989ea2 ""
|
||||
"main.aux" 1761582781.75348 4309 2fe6e70a469147f9fa7894d181c11730 "pdflatex"
|
||||
"main.bbl" 1761582767.77825 3342 075c8b964a4c2fd091cb5b3a254f2d36 "bibtex main"
|
||||
"main.tex" 1761582764.60719 338 084198f0761b22477b610a20748757ce ""
|
||||
"metrics-of-success/v1.tex" 1760371276.72563 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
|
||||
"research-approach/v3.tex" 1759939583.16696 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
|
||||
"risks-and-contingencies/v1.tex" 1761582682.04479 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
|
||||
"state-of-the-art/v5.tex" 1760985490.34139 21194 7c0c8b627f15a0d811e7e10493b34cbf ""
|
||||
(generated)
|
||||
"main.aux"
|
||||
"main.log"
|
||||
|
||||
@ -401,18 +401,23 @@ 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/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT ./whitepaper/v1.tex
|
||||
INPUT ./whitepaper/v1.tex
|
||||
INPUT ./whitepaper/v1.tex
|
||||
INPUT ./whitepaper/v1.tex
|
||||
INPUT whitepaper/v1.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT goals-and-outcomes/v6.tex
|
||||
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/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/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT ./state-of-the-art/v5.tex
|
||||
INPUT ./state-of-the-art/v5.tex
|
||||
INPUT ./state-of-the-art/v5.tex
|
||||
INPUT ./state-of-the-art/v5.tex
|
||||
INPUT state-of-the-art/v5.tex
|
||||
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
|
||||
@ -438,15 +443,61 @@ 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/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/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/zptmcm7y.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
|
||||
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 ./research-approach/v3.tex
|
||||
INPUT ./research-approach/v3.tex
|
||||
INPUT ./research-approach/v3.tex
|
||||
INPUT ./research-approach/v3.tex
|
||||
INPUT research-approach/v3.tex
|
||||
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 ./metrics-of-success/v1.tex
|
||||
INPUT ./metrics-of-success/v1.tex
|
||||
INPUT ./metrics-of-success/v1.tex
|
||||
INPUT ./metrics-of-success/v1.tex
|
||||
INPUT metrics-of-success/v1.tex
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm
|
||||
INPUT ./risks-and-contingencies/v1.tex
|
||||
INPUT ./risks-and-contingencies/v1.tex
|
||||
INPUT ./risks-and-contingencies/v1.tex
|
||||
INPUT ./risks-and-contingencies/v1.tex
|
||||
INPUT risks-and-contingencies/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT broader-impacts/v1.tex
|
||||
INPUT ./main.bbl
|
||||
INPUT ./main.bbl
|
||||
INPUT main.bbl
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm
|
||||
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/public/amsfonts/cm/cmtt12.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/utmbi8a.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
|
||||
|
||||
@ -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 17:12
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 27 OCT 2025 12:33
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
file:line:error style messages enabled.
|
||||
@ -876,36 +876,49 @@ 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]
|
||||
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v6.tex [1]) (./state-of-the-art/v5.tex
|
||||
|
||||
LaTeX Warning: Citation `princeton' on page 2 undefined on input line 19.
|
||||
|
||||
[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 212.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 145.
|
||||
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 212.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 145.
|
||||
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 212.
|
||||
[4] [5]
|
||||
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 344.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 145.
|
||||
[4]
|
||||
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 177.
|
||||
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
|
||||
) [6]) [7] (./main.aux)
|
||||
) [5] [6]) (./research-approach/v3.tex [7] [8] [9] [10] [11]) (./metrics-of-success/v1.tex [12] [13]) (./risks-and-contingencies/v1.tex [14] [15] [16]) (./broader-impacts/v1.tex [17] [18]) [19] (./main.bbl
|
||||
Underfull \hbox (badness 10000) in paragraph at lines 25--28
|
||||
\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
|
||||
[]
|
||||
|
||||
[20]) [21] (./main.aux)
|
||||
***********
|
||||
LaTeX2e <2023-11-01> patch level 1
|
||||
L3 programming layer <2024-01-22>
|
||||
***********
|
||||
|
||||
|
||||
LaTeX Warning: There were undefined references.
|
||||
|
||||
)
|
||||
Here is how much of TeX's memory you used:
|
||||
25363 strings out of 476182
|
||||
526810 string characters out of 5795595
|
||||
25445 strings out of 476182
|
||||
528559 string characters out of 5795595
|
||||
1934975 words of memory out of 5000000
|
||||
46826 multiletter control sequences out of 15000+600000
|
||||
587807 words of font info for 99 fonts, out of 8000000 for 9000
|
||||
46875 multiletter control sequences out of 15000+600000
|
||||
592787 words of font info for 111 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
|
||||
</usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
|
||||
Output written on main.pdf (8 pages, 68969 bytes).
|
||||
110i,6n,107p,1008b,333s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
|
||||
Output written on main.pdf (22 pages, 164089 bytes).
|
||||
PDF statistics:
|
||||
74 PDF objects out of 1000 (max. 8388607)
|
||||
41 compressed objects within 1 object stream
|
||||
148 PDF objects out of 1000 (max. 8388607)
|
||||
89 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)
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@ -3,17 +3,18 @@
|
||||
\begin{document}
|
||||
|
||||
\maketitle
|
||||
% \input{goals-and-outcomes/v6}
|
||||
% \input{state-of-the-art/v5}
|
||||
% \input{research-approach/v3}
|
||||
% \input{broader-impacts/v1}
|
||||
% \input{metrics-of-success/v1}
|
||||
%
|
||||
% \newpage
|
||||
% \bibliography{references}
|
||||
\input{goals-and-outcomes/v6}
|
||||
\input{state-of-the-art/v5}
|
||||
\input{research-approach/v3}
|
||||
\input{metrics-of-success/v1}
|
||||
\input{risks-and-contingencies/v1}
|
||||
\input{broader-impacts/v1}
|
||||
|
||||
\newpage
|
||||
\bibliography{references}
|
||||
|
||||
% White Paper
|
||||
|
||||
\input{whitepaper/v1}
|
||||
% \input{whitepaper/v1}
|
||||
|
||||
\end{document}
|
||||
|
||||
67
Writing/ERLM/risks-and-contingencies/assumptions.md
Normal file
67
Writing/ERLM/risks-and-contingencies/assumptions.md
Normal file
@ -0,0 +1,67 @@
|
||||
# Risk and Contingencies Assumptions Exercise
|
||||
|
||||
**The outcome I want to achieve is?**
|
||||
- Turn written reqs into discrete controller
|
||||
- Build continuous modes that ensure hybrid stability
|
||||
- Implement on industrial controller with HIL simulation
|
||||
|
||||
**What can't anyone solve this today?**
|
||||
- Nobody has tried to build system like this with stability
|
||||
in mind from the ground up. NUCE is a specific domain this
|
||||
is useful. Reliance on human operators for safety.
|
||||
|
||||
**The research approach I am using is?**
|
||||
- Formal Methods + Control Theory
|
||||
- FRET - Reachability
|
||||
- Reactive Synthesis
|
||||
|
||||
**This research approach relies on these fundamental
|
||||
principles?**
|
||||
- Temporal logic precision
|
||||
- automata
|
||||
- differential and difference equations
|
||||
- procedure writing
|
||||
|
||||
**The experiment that I will perform is?**
|
||||
- trying to make an autonomous start up procedure for a
|
||||
SmAHTR reactor
|
||||
|
||||
**The equipment I will use is?**
|
||||
1. FRET
|
||||
2. STRIX
|
||||
3. Simulink
|
||||
4. Reachability tools
|
||||
5. Ovation
|
||||
|
||||
**I will analyze the results using?**
|
||||
1. Prose. How hard was this to do, what MacGuyvering needed
|
||||
done? What TRL?
|
||||
|
||||
**The expected outcome of this experiment is?**
|
||||
1. A working autonomous start up controller can take a
|
||||
simulation from cold to critical without needing a human
|
||||
operator to intervene.
|
||||
|
||||
**What happens if this experiment does not work?**
|
||||
1. We'll shift to a smaller, simpler problem where we can
|
||||
overcome the limits.
|
||||
|
||||
**What happens if the hypothesis or prediction is false?**
|
||||
1. We'll show the gap between current procedure writing and
|
||||
where we need to be to actually do synthesis.
|
||||
|
||||
**What assumptions do I have that, if proven wrong, would
|
||||
derail this project?**
|
||||
1. Temporal logic from FRET is easy to synthesize with STRIX
|
||||
2. I'm not going to have state-space explosion happen
|
||||
3. Writing a start-up procedure for SmAHTR isn't that hard
|
||||
4. People give a crap about molten salt reactors
|
||||
5. This whole discrete boundary thing is not going to be
|
||||
really hard to implement. The idea is conditions for the
|
||||
transitions between modes to be boolean variables for
|
||||
the temporal lgoic, but that they correspond to some surface
|
||||
in the continuous state space. How am I going to keep track
|
||||
of that?
|
||||
6. Computational cost. Center for Research Computing is the
|
||||
answer.
|
||||
|
||||
231
Writing/ERLM/risks-and-contingencies/v1.tex
Normal file
231
Writing/ERLM/risks-and-contingencies/v1.tex
Normal file
@ -0,0 +1,231 @@
|
||||
\section{Risks and Contingencies}
|
||||
|
||||
This research relies on several critical assumptions that, if invalidated,
|
||||
would require scope adjustment or methodological revision. The primary risks to
|
||||
successful completion fall into four categories: computational tractability of
|
||||
synthesis and verification, complexity of the discrete-continuous interface,
|
||||
completeness of procedure formalization, and hardware-in-the-loop integration
|
||||
challenges. Each risk has associated indicators for early detection and
|
||||
contingency plans that preserve research value even if core assumptions prove
|
||||
false. The staged project structure ensures that partial success yields
|
||||
publishable results and clear identification of remaining barriers to
|
||||
deployment.
|
||||
|
||||
\subsection{Computational Tractability of Synthesis}
|
||||
|
||||
The first major assumption is that formalized startup procedures will yield
|
||||
automata small enough for efficient synthesis and verification. Reactive
|
||||
synthesis scales exponentially with specification complexity, which creates risk
|
||||
that temporal logic specifications derived from complete startup procedures may
|
||||
produce automata with thousands of states. Such large automata would require
|
||||
synthesis times exceeding days or weeks, preventing demonstration of the
|
||||
complete methodology within project timelines. Reachability analysis for
|
||||
continuous modes with high-dimensional state spaces may similarly prove
|
||||
computationally intractable. Either barrier would constitute a fundamental
|
||||
obstacle to achieving the research objectives.
|
||||
|
||||
Several indicators would provide early warning of computational tractability
|
||||
problems. Synthesis times exceeding 24 hours for simplified procedure subsets
|
||||
would suggest that complete procedures are intractable. Generated automata
|
||||
containing more than 1,000 discrete states would indicate that the discrete
|
||||
state space is too large for efficient verification. Specifications flagged as
|
||||
unrealizable by FRET or STRIX would reveal fundamental conflicts in the
|
||||
formalized procedures. Reachability analysis failing to converge within
|
||||
reasonable time bounds would show that continuous mode verification cannot be
|
||||
completed with available computational resources.
|
||||
|
||||
The contingency plan for computational intractability is to reduce scope to a
|
||||
minimal viable startup sequence. This reduced sequence would cover only cold
|
||||
shutdown to criticality to low power hold, omitting power ascension and other
|
||||
operational phases. The subset would still demonstrate the complete
|
||||
methodology while reducing computational burden. The research contribution
|
||||
would remain valid even with reduced scope, proving that formal hybrid control
|
||||
synthesis is achievable for safety-critical nuclear applications. The limitation
|
||||
to simplified operational sequences would be explicitly documented as a
|
||||
constraint rather than a failure.
|
||||
|
||||
Reachability analysis specifically can exploit time-scale separation inherent in
|
||||
reactor dynamics. Fast thermal transients can be treated quasi-steady relative
|
||||
to slower nuclear kinetics, which enables decomposition into smaller subsystems.
|
||||
Temperature dynamics operate on time scales of seconds to minutes, while neutron
|
||||
kinetics respond in milliseconds to seconds for prompt effects and hours for
|
||||
xenon poisoning. These distinct time scales permit separate analysis with
|
||||
conservative coupling assumptions between subsystems, dramatically reducing the
|
||||
dimensionality of reachability computations.
|
||||
|
||||
Mitigation strategies exist even before contingency plans become necessary.
|
||||
Access to the University of Pittsburgh Center for Research Computing provides
|
||||
high-performance computing resources if single-workstation computation proves
|
||||
insufficient. Parallel synthesis algorithms and distributed reachability
|
||||
analysis can leverage these resources to extend computational feasibility.
|
||||
Compositional verification approaches using assume-guarantee reasoning can
|
||||
decompose monolithic verification problems into tractable subproblems, each of
|
||||
which can be solved independently before composition.
|
||||
|
||||
\subsection{Discrete-Continuous Interface Formalization}
|
||||
|
||||
The second critical assumption concerns the mapping between boolean guard
|
||||
conditions in temporal logic and continuous state boundaries required for mode
|
||||
transitions. This interface represents the fundamental challenge of hybrid
|
||||
systems: relating discrete switching logic to continuous dynamics. Temporal
|
||||
logic operates on boolean predicates, while continuous control requires
|
||||
reasoning about differential equations and reachable sets. Guard conditions that
|
||||
require complex nonlinear predicates may resist boolean abstraction, making
|
||||
synthesis intractable. Continuous safety regions that cannot be expressed as
|
||||
conjunctions of verifiable constraints would similarly create insurmountable
|
||||
verification challenges. The risk extends beyond static interface definition to
|
||||
dynamic behavior across transitions: barrier certificates may fail to exist for
|
||||
proposed transitions, or continuous modes may be unable to guarantee convergence
|
||||
to discrete transition boundaries.
|
||||
|
||||
Early indicators of interface formalization problems would appear during both
|
||||
synthesis and verification phases. Guard conditions requiring complex nonlinear
|
||||
predicates that resist boolean abstraction would suggest fundamental misalignment
|
||||
between discrete specifications and continuous realities. Continuous safety
|
||||
regions that cannot be expressed as conjunctions of half-spaces or polynomial
|
||||
inequalities would indicate that the interface between discrete guards and
|
||||
continuous invariants is too complex. Failure to construct barrier certificates
|
||||
proving safety across mode transitions would reveal that the continuous dynamics
|
||||
cannot be formally related to discrete switching logic. Reachability analysis
|
||||
showing that continuous modes cannot reach intended transition boundaries from
|
||||
all possible initial conditions would demonstrate that the synthesized discrete
|
||||
controller is incompatible with achievable continuous behavior.
|
||||
|
||||
The primary contingency for interface complexity is to restrict continuous modes
|
||||
to operate within polytopic invariants. Polytopes are state regions defined as
|
||||
intersections of linear half-spaces, which map directly to boolean predicates
|
||||
through linear inequality checks. This restriction ensures tractable synthesis
|
||||
while maintaining theoretical rigor, though at the cost of limiting
|
||||
expressiveness compared to arbitrary nonlinear regions. The discrete-continuous
|
||||
interface remains well-defined and verifiable with polytopic restrictions,
|
||||
providing a clear fallback position that preserves the core methodology.
|
||||
Conservative over-approximations offer an alternative approach: a nonlinear safe
|
||||
region can be inner-approximated by a polytope, sacrificing operational
|
||||
flexibility to maintain formal guarantees. The three-mode classification already
|
||||
structures the problem to minimize complex transitions, with critical safety
|
||||
properties concentrated in expulsory modes that can receive additional design
|
||||
attention.
|
||||
|
||||
Mitigation strategies focus on designing continuous controllers with discrete
|
||||
transitions as primary objectives from the outset. Rather than designing
|
||||
continuous control laws independently and verifying transitions post-hoc, the
|
||||
approach uses transition requirements as design constraints. Control barrier
|
||||
functions provide a systematic method to synthesize controllers that guarantee
|
||||
forward invariance of safe sets and convergence to transition boundaries. This
|
||||
design-for-verification approach reduces the likelihood that interface
|
||||
complexity becomes insurmountable. Focusing verification effort on expulsory
|
||||
modes---where safety is most critical---allows more complex analysis to be
|
||||
applied selectively rather than uniformly across all modes, concentrating
|
||||
computational resources where they matter most for safety assurance.
|
||||
|
||||
\subsection{Procedure Formalization Completeness}
|
||||
|
||||
The third assumption is that existing SmAHTR startup procedures contain
|
||||
sufficient detail and clarity for translation into temporal logic specifications.
|
||||
Nuclear operating procedures, while extensively detailed, were written for human
|
||||
operators who bring contextual understanding and adaptive reasoning to their
|
||||
interpretation. Procedures may contain implicit knowledge, ambiguous directives,
|
||||
or references to operator judgment that resist formalization in current
|
||||
specification languages. Underspecified timing constraints, ambiguous condition
|
||||
definitions, or gaps in operational coverage would cause synthesis to fail or
|
||||
produce incorrect automata. The risk is not merely that formalization is
|
||||
difficult, but that current procedures fundamentally lack the precision required
|
||||
for autonomous control, revealing a gap between human-oriented documentation and
|
||||
machine-executable specifications.
|
||||
|
||||
Several indicators would reveal formalization completeness problems early in the
|
||||
project. FRET realizability checks failing due to underspecified behaviors or
|
||||
conflicting requirements would indicate that procedures do not form a complete
|
||||
specification. Multiple valid interpretations of procedural steps with no clear
|
||||
resolution would demonstrate that procedure language is insufficiently precise
|
||||
for automated synthesis. Procedures referencing ``operator judgment,'' ``as
|
||||
appropriate,'' or similar discretionary language for critical decisions would
|
||||
explicitly identify points where human reasoning cannot be directly formalized.
|
||||
Domain experts unable to provide crisp answers to specification questions about
|
||||
edge cases would suggest that the procedures themselves do not fully define
|
||||
system behavior, relying instead on operator training and experience to fill
|
||||
gaps.
|
||||
|
||||
The contingency plan treats inadequate specification as itself a research
|
||||
contribution rather than a project failure. Documenting specific ambiguities
|
||||
encountered would create a taxonomy of formalization barriers: timing
|
||||
underspecification, missing preconditions, discretionary actions, and undefined
|
||||
failure modes. Each category would be analyzed to understand why current
|
||||
procedure-writing practices produce these gaps and what specification languages
|
||||
would need to address them. Proposed extensions to FRETish or similar
|
||||
specification languages would demonstrate how to bridge the gap between current
|
||||
procedures and the precision needed for autonomous control. The research output
|
||||
would shift from ``here is a complete autonomous controller'' to ``here is what
|
||||
formal autonomous control requires that current procedures do not provide, and
|
||||
here are language extensions to bridge that gap.'' This contribution remains
|
||||
valuable to both the nuclear industry and formal methods community, establishing
|
||||
clear requirements for next-generation procedure development and autonomous
|
||||
control specification languages.
|
||||
|
||||
Early-stage procedure analysis with domain experts provides the primary
|
||||
mitigation strategy. Collaboration through the University of Pittsburgh Cyber
|
||||
Energy Center enables identification and resolution of ambiguities before
|
||||
synthesis attempts, rather than discovering them during failed synthesis runs.
|
||||
Iterative refinement with reactor operators and control engineers can clarify
|
||||
procedural intent before formalization begins, reducing the risk of discovering
|
||||
insurmountable specification gaps late in the project. Comparison with
|
||||
procedures from multiple reactor designs---pressurized water reactors, boiling
|
||||
water reactors, and advanced designs---may reveal common patterns and standard
|
||||
ambiguities amenable to systematic resolution. This cross-design analysis would
|
||||
strengthen the generalizability of any proposed specification language
|
||||
extensions, ensuring they address industry-wide practices rather than
|
||||
SmAHTR-specific quirks.
|
||||
|
||||
\subsection{Hardware-in-the-Loop Integration Complexity}
|
||||
|
||||
The fourth assumption is that the ARCADE interface can provide stable real-time
|
||||
communication between Simulink simulation and Ovation control hardware at
|
||||
control rates required for reactor dynamics. Hardware-in-the-loop testing
|
||||
introduces timing constraints, communication latency, and platform compatibility
|
||||
challenges that are absent in pure simulation. Control rates for reactor systems
|
||||
typically range from 10-100 Hz for continuous control to millisecond response
|
||||
times for protection system actions. Control loop jitter, communication
|
||||
dropouts, or computational limitations in the Ovation PLC could prevent
|
||||
successful HIL validation even if the synthesized controller is theoretically
|
||||
correct. Real-time operating system constraints, network latency, and hardware
|
||||
execution speed may prove incompatible with verified timing assumptions embedded
|
||||
in the controller design.
|
||||
|
||||
Early indicators would identify hardware integration problems before they derail
|
||||
the entire validation effort. Communication dropouts or buffer overruns between ARCADE
|
||||
and Ovation would indicate that the interface cannot maintain stable real-time
|
||||
data exchange. The Ovation PLC proving unable to execute the synthesized
|
||||
automaton at required speed would reveal fundamental computational limitations
|
||||
of the target hardware platform. Timing analysis showing that hardware cannot
|
||||
meet real-time deadlines assumed during verification would demonstrate
|
||||
incompatibility between formal guarantees and physical implementation
|
||||
constraints.
|
||||
|
||||
The contingency plan is to demonstrate the controller in software-in-the-loop
|
||||
configuration with detailed timing analysis showing industrial hardware
|
||||
feasibility. Software-in-the-loop testing executes the complete verified
|
||||
controller in a real-time software environment that emulates hardware timing
|
||||
constraints without requiring physical hardware. Combined with worst-case
|
||||
execution time analysis of the synthesized automaton and continuous control
|
||||
algorithms, software-in-the-loop validation can provide strong evidence of
|
||||
implementability even without physical hardware demonstration. This approach
|
||||
maintains TRL 4 rather than TRL 5, but still validates
|
||||
the synthesis methodology and establishes a clear pathway to hardware
|
||||
deployment. The research contribution remains intact: demonstrating that formal
|
||||
hybrid control synthesis produces implementable controllers, with remaining
|
||||
barriers clearly identified as hardware integration challenges rather than
|
||||
fundamental methodological limitations.
|
||||
|
||||
Mitigation strategies leverage existing infrastructure and adopt early testing
|
||||
practices. ARCADE has been successfully used for reactor simulation HIL testing
|
||||
at the University of Pittsburgh, establishing feasibility in principle and
|
||||
providing institutional knowledge about common integration challenges. Conducting
|
||||
early integration testing during the synthesis phase, rather than deferring HIL
|
||||
attempts until late in the project, identifies timing constraints and
|
||||
communication requirements that can inform controller design. Early testing
|
||||
ensures that synthesized controllers are compatible with hardware limitations
|
||||
from the outset, rather than discovering incompatibilities after synthesis is
|
||||
complete. The Ovation platform supports multiple implementation approaches
|
||||
including function blocks, structured text, and ladder logic, which provides
|
||||
flexibility in how synthesized automata are realized and may enable workarounds
|
||||
if one implementation approach proves problematic.
|
||||
@ -1,4 +1,3 @@
|
||||
|
||||
% PROJECT SUMMARY
|
||||
\section*{Project Summary}
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user