danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Auto sync: 2025-12-05 17:50:51 (5 files changed)

Browse Source 
M  Writing/ERLM/main.fdb_latexmk

M  Writing/ERLM/main.log

M  Writing/ERLM/main.pdf

M  Writing/ERLM/main.synctex.gz

M  Writing/ERLM/state-of-the-art/v6.tex
This commit is contained in:
Dane Sabo 2025-12-05 17:50:51 -05:00
parent 54cc24e2f9
commit 9e01a8e6a1
5 changed files with 16 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Writing/ERLM/main.fdb_latexmk
View File

@ -1,13 +1,13 @@
# Fdb version 4 # 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 "" "./references.bib" 1764974759.12837 5129 de2dc116e7908a86456f09f33e7d7ac7 ""
"/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" "/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) (generated)
"main.bbl" "main.bbl"
"main.blg" "main.blg"
(rewritten before read) (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 "" "/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/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/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
@ -245,14 +245,14 @@
"budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 "" "budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
"dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c "" "dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c ""
"goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 "" "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.bbl" 1764974760.75697 2467 75ddd8bc744ac1d7c685bc124699a008 "bibtex main"
"main.tex" 1764974466.74023 804 d25a45e5732ab0e63adac220a8893f96 "" "main.tex" 1764974466.74023 804 d25a45e5732ab0e63adac220a8893f96 ""
"metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 "" "metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
"research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f "" "research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
"risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 "" "risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
"schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d "" "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/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
"supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 "" "supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
"supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 "" "supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 ""

2
Writing/ERLM/main.log
View File

@ -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 entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled. file:line:error style messages enabled.

BIN
Writing/ERLM/main.pdf
View File

Binary file not shown.

BIN
Writing/ERLM/main.synctex.gz
View File

Binary file not shown.

20
Writing/ERLM/state-of-the-art/v6.tex
View File

@ -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) The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
project represents the most advanced application of formal methods to nuclear 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 reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address the
fundamental dilemma: existing U.S. nuclear control rooms rely on analog nuclear industry's fundamental dilemma: existing U.S. nuclear control rooms rely
technologies from the 1950s--60s. This technology is woefully out of date on analog technologies from the 1950s--60s. This technology is woefully out of
compared to modern control technologies, and incurs significant risk and cost to date compared to modern control technologies, and incurs significant risk and
plant operation. The NRC contracted Galois, a company of formal methods experts, cost to plant operation. The NRC contracted Galois, a company of formal methods
to demonstrate that Model-Based Systems Engineering and formal methods could experts, to demonstrate that Model-Based Systems Engineering and formal methods
design, verify, and implement a complex protection system meeting regulatory could design, verify, and implement a complex protection system meeting
criteria at a fraction of typical cost. The project delivered a Reactor Trip regulatory criteria at a fraction of typical cost. The project delivered a
System (RTS) implementation with full traceability from NRC Request for Reactor Trip System (RTS) implementation with full traceability from NRC Request
Proposals and IEEE standards through formal architecture specifications to for Proposals and IEEE standards through formal architecture specifications to
formally verified software. formally verified software.
%%% did it actually do an FPGA demonstration? Dubious. %%% did it actually do an FPGA demonstration? Dubious.