diff --git a/Writing/ERLM/GOv1.pdf b/Writing/ERLM/GOv1.pdf new file mode 100644 index 000000000..daa3e3d2a Binary files /dev/null and b/Writing/ERLM/GOv1.pdf differ diff --git a/Writing/ERLM/goals-and-outcomes/v1.tex b/Writing/ERLM/goals-and-outcomes/v1.tex new file mode 100644 index 000000000..fcbd28626 --- /dev/null +++ b/Writing/ERLM/goals-and-outcomes/v1.tex @@ -0,0 +1,66 @@ +\section{Goals and Outcomes} + +The goal of this research is to use formal methods to create control systems +that can switch between operating modes with a high assurance of correct +construction. Modern control systems today often exist as hybrid control +systems. Hybrid systems are those that have both continuous and discrete +dynamics. Because of this, hybrid systems cannot be fully analyzed using only +tools from continuous or discrete methods. Today, hybrid control systems are +unable to be completely verified, that is to say we do not currently have ways +of being building hybrid control systems that we can be certain meet high level +strategic objectives, or who's behavior is totally understood. + +The ambiguity on hybrid system behavior is problematic when one of the most +useful cases of hybrid system control is for improved autonomy of critical +systems. Nuclear power is a salient example. For a nuclear reactor during +start-up, every mode of power from initially cold-start, to controlled core +heating, and eventually full operating power is well understood dynamically. +For each of these modes, significant portions of the control are optimized using +automated controllers for each stage. The problem that remains for human +operators is choosing when to switch from control law to the next, and ensuring +that the proper conditions are met to do so--but these conditions are also +clearly defined in regulation and operating procedures a priori. + +We can use the fact that these transition points are well understood in +combination with formal methods to synthesize the discrete part of a hybrid +system. From that point, we can have a robust chain of proof that our discrete +jumps will happen only at the correct times. Once that is established, we can +use reachability analysis and traditional control theory to ensure that each +operation 'mode' satisfies liveness, stability, or performance requirements. +With the combination of these two methods, we can be sure of correct behavior +switching between modes, and that strategic goals remain met while transitioning +from one mode switch to the next. + +If this research is successful, we will be able to do the following: + +\begin{enumerate} + + \item + \textbf{Formalize} mode switching requirements as logical statements that + can then be translated into a controller implementation. This piece will + address the correct-by-construction generation of the mode switching + controller. + + \item + \textbf{Categorize} different continuous modes by their strategic relevance. + Certain modes exist as control laws from one mode to the next, such as a + controlled heating rate on reactor start-up before reaching operational + conditions. Other modes exist as stable regions, such as full-power + operation. + + \item + \textbf{Verify} continuous modes and accompanying continuous control laws + satisfy strategic requirements. This can be done with reachability analysis, + and ensuring that each mode transition as allowed from the requirements + synthesis squares up against the reachability analysis and the continuous + dynamics. + + \item + \textbf{Prove} that a given hybrid system achieves strategic goals across + hybrid control modes. By seperately formalizing and analyzing continuous + dyanmics and discrete dynamics, we can come back to say the whole hybrid + system has met a strong guarantee of requirement adherence. + +\end{enumerate} + + diff --git a/Writing/ERLM/goals-and-outcomes/v2.tex b/Writing/ERLM/goals-and-outcomes/v2.tex new file mode 100644 index 000000000..3fd52ea6a --- /dev/null +++ b/Writing/ERLM/goals-and-outcomes/v2.tex @@ -0,0 +1,75 @@ +\section{Goals and Outcomes} + +The goal of this research is to use formal methods to create high-assurance +hybrid control systems. Hybrid control systems have great potential for +implementation in autonomous control as they are able to change control laws +based on discrete triggers in the operating range of the controller. This allows +the autonomous controller to use several easily tractable control laws for different +regions in the state space, instead of using one controller over the entire +systems operating range. But, the discrete jumps between control laws in a +hybrid controller present challenges in proving stability and liveness +properties of the whole system. While tools from control theory can prove +properties for each individual control mode, they do not generalize when +switching between control laws is introduced. + +This research will take a different approach to hybrid controller synthesis and +verification. Using tools from the formal methods community, we will create +controllers that are correct-by-construction and allow guarantees to be made +about the whole system's behavior. To demonstrate this, an autonomous controller +for a nuclear power plant start-up procedure will be created. Nuclear power is +an excellent test case for this work as the continuous piece of reactor dynamics +is well studied, while the discrete component of mode switching is explicitly +stated in regulatory requirements and operating procedures. Nuclear reactor +control today \textit{is} a hybrid control system--many functions in the control +room use automated controllers for basic tasks, but the engagement and selection +of these controllers is done by human operators referencing procedures to make +decisions. + +The capability to create high-assurance hybrid control systems has the potential +to reduce the labor required to operate critical systems by removing the human +operator from the loop. Nuclear power stands to greatly benefit from greater +controller autonomy as the largest expense for reactors today is operations and +maintenance. Technologies such as microreactors and modular reactors will +improve the maintenance costs required through the use of factory-made +replacement components, but will suffer increased operating costs per megawatt +produced if they are required to staff the same way reactors today are staffed. +But, if increased autonomy can be introduced, these costs will be ameliorated. + +If this research is successful, we will be able to do the following: + +\begin{enumerate} + + \item + \textbf{Formalize mode switching requirements as logical specifications that + can be translated into discrete controller implementations.} The discrete + transitions between continuous controller modes is often explicitly defined + for critical systems in operating procedures and regulatory requirements. + These statements will be translated into a temporal logic, which will then + be synthesized into a discrete controller implementation for continuous + controller mode switching. + + \item + \textbf{Categorize different continuous controller modes by their strategic + relavance.} Different control modes serve one of two purposes: they may be + transitory or stabilizing. Knowing when to switch from one control mode to + another is handled by the discrete component of the hybrid system, but this + outcome will identify the properties the continuous components must satisfy + for each controller mode. + + \item + \textbf{Verify that continuous controller modes satisfy dynamic + requirements.} For the discrete transitions between control modes to be + useful, we must ensure that the continuous control modes will actually move + the system to the transition, or if stabilizing, keep the system from + leaving the control mode. + + \item + \textbf{Prove that a hybrid system implementation achieve strategic goals + across the entire controller operating range.} By creating discrete + controller transitions from logical specifications that are + correct-by-construction and validating that continuous components perform + appropriately between discrete transitions, we can be confident that the + hybrid system is free from defect and can be utilized as a critical + autonomous controller. + +\end{enumerate} diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index ce199a9d7..2e8c5c74b 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -1,6 +1,6 @@ \relax \bibstyle{unsrt} \providecommand \oddpage@label [2]{} -\bibdata{references} \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } -\gdef \@abspage@last{2} +\bibdata{references} +\gdef \@abspage@last{3} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index dab15963e..c9e6964ee 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,5 +1,5 @@ # Fdb version 4 -["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756866345.56251 0 +["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756913150.42547 0 "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" "main.aux" 0 -1 0 "pdflatex" "references.bib" 0 -1 0 "" @@ -7,14 +7,16 @@ "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1756866345.1432 "main.tex" "main.pdf" "main" 1756866345.56276 0 - "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 "" +["pdflatex"] 1756913149.4861 "main.tex" "main.pdf" "main" 1756913150.42571 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/helvetic/phvb7t.tfm" 1136768653 2240 eb56c13537f4d8a0bd3fafc25572b1bd "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm" 1136768653 4484 b828043cbd581d289d955903c1339981 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr7t.tfm" 1136768653 2520 53e01eef820ca829e42c1333c3fd02b9 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm" 1136768653 4712 9ef4d7d106579d4b136e1529e1a4533c "" + "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro7t.tfm" 1136768653 2772 ab6561c8ff5ee69ff6d5961b9356db5a "" + "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro8r.tfm" 1136768653 4964 f223217e5e1f85fa3742fb0480aba9e8 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df "" "/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/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a "" @@ -26,8 +28,10 @@ "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb" 1136849748 35941 f27169cc74234d5bd5e4cca5abafaabb "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb" 1136849748 44648 23115b2a545ebfe2c526c3ca99db8b95 "" + "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb" 1136849748 48169 b4fd9d908b9ee8c65d4305ad39071c5e "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf" 1136768653 1372 1c26b449eb4a1a0bcf6ac7cfe376d450 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf" 1136768653 1372 dc841a9f00a1a11b1443367ae6c5588e "" + "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvro7t.vf" 1136768653 1372 9948cedecdb0445a3b5cf1b8a8082ab8 "" "/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 "" @@ -207,12 +211,13 @@ "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f "" "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" - "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1726065856.46263 128028 f533b797fba58d231669ea19e894e23e "" - "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae "" - "dane_proposal_format.cls" 1756866343.25274 2551 deee3ebc77bdfb5d08546fb19b3bdd53 "" - "main.aux" 1756866345.49569 213 8bec41973e7f8a0e3c5820f1e8e33fe1 "pdflatex" + "/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" 1756902979.42453 2551 deee3ebc77bdfb5d08546fb19b3bdd53 "" + "goals-and-outcomes/v2.tex" 1756913147.34838 3929 81698d2601ffbfc97dd16c2553a8806b "" + "main.aux" 1756913150.28919 213 c6307743402c02a0530961857d9d1a69 "pdflatex" "main.bbl" 0 -1 0 "bibtex main" - "main.tex" 1756865478.72503 3553 735c6dfea3f38b408b7239e8aa1a4ada "" + "main.tex" 1756910438.79598 141 c588c1bc2f6a6f85c912c3842ff6c482 "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index b8ab0e1b1..0746a54b0 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -382,14 +382,23 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm +INPUT ./goals-and-outcomes/v2.tex +INPUT ./goals-and-outcomes/v2.tex +INPUT ./goals-and-outcomes/v2.tex +INPUT ./goals-and-outcomes/v2.tex +INPUT goals-and-outcomes/v2.tex INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvro7t.vf +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm INPUT main.aux INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb +INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index a0a80c950..23d5e696b 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.11) 2 SEP 2025 22:25 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 3 SEP 2025 11:25 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -829,31 +829,30 @@ LaTeX Font Info: Trying to load font information for U+msb on input line 5. File: umsb.fd 2013/01/14 v3.01 AMS symbols B ) [1 -{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] -Overfull \hbox (0.67523pt too wide) in paragraph at lines 57--62 -\OT1/phv/m/n/12 each mode tran-si-tion as al-lowed from the re-quire-ments syn-the-sis squares up against - [] - +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v2.tex +LaTeX Font Info: Font shape `OT1/phv/m/it' in size <12> not available +(Font) Font shape `OT1/phv/m/sl' tried instead on input line 23. + [1]) No file main.bbl. -[1] (./main.aux) +[2] (./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: - 25245 strings out of 476182 - 524777 string characters out of 5795595 - 1933975 words of memory out of 5000000 - 46726 multiletter control sequences out of 15000+600000 - 571272 words of font info for 60 fonts, out of 8000000 for 9000 + 25258 strings out of 476182 + 525061 string characters out of 5795595 + 1934975 words of memory out of 5000000 + 46733 multiletter control sequences out of 15000+600000 + 573158 words of font info for 62 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 (2 pages, 24992 bytes). + +Output written on main.pdf (3 pages, 30389 bytes). PDF statistics: - 49 PDF objects out of 1000 (max. 8388607) - 24 compressed objects within 1 object stream + 57 PDF objects out of 1000 (max. 8388607) + 29 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 999ad67b6..99477d251 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 c01e72720..a51db1e95 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index 0621f5050..d88fd0a92 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -3,72 +3,9 @@ \begin{document} \maketitle -\section{Goals and Outcomes} -The goal of this research is to use formal methods to create control systems -that can switch between operating modes with a high assurance of correct -construction. Modern control systems today often exist as hybrid control -systems. Hybrid systems are those that have both continuous and discrete -dynamics. Because of this, hybrid systems cannot be fully analyzed using only -tools from continuous or discrete methods. Today, hybrid control systems are -unable to be completely verified, that is to say we do not currently have ways -of being building hybrid control systems that we can be certain meet high level -strategic objectives, or who's behavior is totally understood. - -The ambiguity on hybrid system behavior is problematic when one of the most -useful cases of hybrid system control is for improved autonomy of critical -systems. Nuclear power is a salient example. For a nuclear reactor during -start-up, every mode of power from initially cold-start, to controlled core -heating, and eventually full operating power is well understood dynamically. -For each of these modes, significant portions of the control are optimized using -automated controllers for each stage. The problem that remains for human -operators is choosing when to switch from control law to the next, and ensuring -that the proper conditions are met to do so--but these conditions are also -clearly defined in regulation and operating procedures a priori. - -We can use the fact that these transition points are well understood in -combination with formal methods to synthesize the discrete part of a hybrid -system. From that point, we can have a robust chain of proof that our discrete -jumps will happen only at the correct times. Once that is established, we can -use reachability analysis and traditional control theory to ensure that each -operation 'mode' satisfies liveness, stability, or performance requirements. -With the combination of these two methods, we can be sure of correct behavior -switching between modes, and that strategic goals remain met while transitioning -from one mode switch to the next. - -If this research is successful, we will be able to do the following: - -\begin{enumerate} - - \item - \textbf{Formalize} mode switching requirements as logical statements that - can then be translated into a controller implementation. This piece will - address the correct-by-construction generation of the mode switching - controller. - - \item - \textbf{Categorize} different continuous modes by their strategic relevance. - Certain modes exist as control laws from one mode to the next, such as a - controlled heating rate on reactor start-up before reaching operational - conditions. Other modes exist as stable regions, such as full-power - operation. - - \item - \textbf{Verify} continuous modes and accompanying continuous control laws - satisfy strategic requirements. This can be done with reachability analysis, - and ensuring that each mode transition as allowed from the requirements - synthesis squares up against the reachability analysis and the continuous - dynamics. - - \item - \textbf{Prove} that a given hybrid system achieves strategic goals across - hybrid control modes. By seperately formalizing and analyzing continuous - dyanmics and discrete dynamics, we can come back to say the whole hybrid - system has met a strong guarantee of requirement adherence. - -\end{enumerate} +\input{goals-and-outcomes/v2} \bibliography{references} \end{document} -