diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 58acee016..1c5fe408b 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 1764974760.71217 "main.aux" "main.bbl" "main" 1764974761.6655 0 +["bibtex main"] 1764974760.71217 "main.aux" "main.bbl" "main" 1764975051.10496 0 "./references.bib" 1764974759.12837 5129 de2dc116e7908a86456f09f33e7d7ac7 "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" - "main.aux" 1764974761.51097 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" + "main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1764974760.76605 "main.tex" "main.pdf" "main" 1764974761.66567 0 +["pdflatex"] 1764975050.20677 "main.tex" "main.pdf" "main" 1764975051.10514 0 "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 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 "" @@ -245,14 +245,14 @@ "budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 "" "dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c "" "goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 "" - "main.aux" 1764974761.51097 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" + "main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" "main.bbl" 1764974760.75697 2467 75ddd8bc744ac1d7c685bc124699a008 "bibtex main" "main.tex" 1764974466.74023 804 d25a45e5732ab0e63adac220a8893f96 "" "metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 "" "research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f "" "risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 "" "schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d "" - "state-of-the-art/v6.tex" 1764972984.45499 13382 928592dcd1dd1113207582a3c5467b68 "" + "state-of-the-art/v6.tex" 1764975048.60283 13382 c10ff226a1b21f79fbc41b5ad41d2e48 "" "supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 "" "supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 "" "supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 "" diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index ad30cac47..f58c369ec 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) 5 DEC 2025 17:46 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 5 DEC 2025 17:50 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index 30ddee1cd..0a1affeb4 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 a981ed7da..3033ea37f 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/state-of-the-art/v6.tex b/Writing/ERLM/state-of-the-art/v6.tex index 8cbc6e550..91f3af893 100644 --- a/Writing/ERLM/state-of-the-art/v6.tex +++ b/Writing/ERLM/state-of-the-art/v6.tex @@ -138,16 +138,16 @@ limitations are fundamental rather than remediable part of human-driven control. The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project represents the most advanced application of formal methods to nuclear -reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address the nuclear industry's -fundamental dilemma: existing U.S. nuclear control rooms rely on analog -technologies from the 1950s--60s. This technology is woefully out of date -compared to modern control technologies, and incurs significant risk and cost to -plant operation. The NRC contracted Galois, a company of formal methods experts, -to demonstrate that Model-Based Systems Engineering and formal methods could -design, verify, and implement a complex protection system meeting regulatory -criteria at a fraction of typical cost. The project delivered a Reactor Trip -System (RTS) implementation with full traceability from NRC Request for -Proposals and IEEE standards through formal architecture specifications to +reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address the +nuclear industry's fundamental dilemma: existing U.S. nuclear control rooms rely +on analog technologies from the 1950s--60s. This technology is woefully out of +date compared to modern control technologies, and incurs significant risk and +cost to plant operation. The NRC contracted Galois, a company of formal methods +experts, to demonstrate that Model-Based Systems Engineering and formal methods +could design, verify, and implement a complex protection system meeting +regulatory criteria at a fraction of typical cost. The project delivered a +Reactor Trip System (RTS) implementation with full traceability from NRC Request +for Proposals and IEEE standards through formal architecture specifications to formally verified software. %%% did it actually do an FPGA demonstration? Dubious.