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

Auto sync: 2025-12-05 22:19:28 (32 files changed)

Browse Source 
M  .task/backlog.data

M  .task/pending.data

M  .task/undo.data

M  Writing/ERLM/1-goals-and-outcomes/research_statement.tex

A  Writing/ERLM/1-goals-and-outcomes/research_statement_v2.tex

A  Writing/ERLM/1-goals-and-outcomes/v8.tex

A  Writing/ERLM/2-state-of-the-art/v7.tex

M  Writing/ERLM/3-research-approach/v4.tex
This commit is contained in:
Dane Sabo 2025-12-05 22:19:28 -05:00
parent 4980358ea4
commit b6364e6428
32 changed files with 2320 additions and 236 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
.task/backlog.data
View File

@ -362,3 +362,10 @@
{"description":"Review and edit Goals and Outcomes section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"0888fdb8-f5cd-4374-a589-b7b3c1bbd472","tags":["editing"]}
{"description":"Review and edit Research Approach section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"9ce7d23c-0f56-49af-b97d-a684966cfbae","tags":["editing"]}
{"description":"Review and edit Metrics of Success section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251206T004956Z","project":"ERLM","start":"20251206T004956Z","status":"pending","uuid":"29cc8c63-1fb7-4523-9953-603467b929ee","tags":["editing"]}
{"description":"Review and edit Metrics of Success section","due":"20251205T050000Z","end":"20251206T025832Z","entry":"20251202T132235Z","modified":"20251206T025836Z","project":"ERLM","status":"completed","uuid":"29cc8c63-1fb7-4523-9953-603467b929ee","tags":["editing"]}
{"description":"Review and edit Risks and Contingencies section","due":"20251205T050000Z","end":"20251206T025836Z","entry":"20251202T132235Z","modified":"20251206T025837Z","project":"ERLM","status":"completed","uuid":"e354ab0c-cef7-41e2-bfb4-d98886e512b7","tags":["editing"]}
{"description":"Review and edit Broader Impacts section","due":"20251205T050000Z","end":"20251206T025837Z","entry":"20251202T132236Z","modified":"20251206T025839Z","project":"ERLM","status":"completed","uuid":"d1fa2409-2f2f-4855-81be-14ee617df5d2","tags":["editing"]}
{"description":"Review and edit Budget section","due":"20251205T050000Z","end":"20251206T025839Z","entry":"20251202T132236Z","modified":"20251206T025839Z","project":"ERLM","status":"completed","uuid":"689420d6-7191-42b6-b691-94ad39c8e0dd","tags":["editing"]}
{"description":"Review and edit Schedule section","due":"20251205T050000Z","end":"20251206T025839Z","entry":"20251202T132236Z","modified":"20251206T025842Z","project":"ERLM","status":"completed","uuid":"14fee599-fe0f-4773-90fc-c5f78291f425","tags":["editing"]}
{"description":"Verify RFP compliance for all sections","due":"20251205T050000Z","end":"20251206T025842Z","entry":"20251202T132246Z","modified":"20251206T025843Z","project":"ERLM","status":"completed","uuid":"a4c027fa-f50d-4efc-ab61-5b8054810a80","tags":["editing"]}
{"description":"Final proofread and polish entire proposal","due":"20251205T050000Z","end":"20251206T025843Z","entry":"20251202T132246Z","modified":"20251206T025844Z","project":"ERLM","status":"completed","uuid":"5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54","tags":["editing"]}

14
.task/pending.data
View File

@ -67,11 +67,11 @@
[description:"Reach out to SOAR for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"535c2ffc-f233-46f0-ac33-a93cbfd12f81"]
[description:"Reach out to Material Advantage for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"00072514-5622-4a44-9826-49690be83767"]
[description:"Reach out to FSAE for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"ca5f0450-483f-4a93-aba1-d06e71b4df5c"]
[description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
[description:"Review and edit Risks and Contingencies section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"]
[description:"Review and edit Broader Impacts section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"]
[description:"Review and edit Budget section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"]
[description:"Review and edit Schedule section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"14fee599-fe0f-4773-90fc-c5f78291f425"]
[description:"Verify RFP compliance for all sections" due:"1764910800" entry:"1764681766" modified:"1764681766" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"a4c027fa-f50d-4efc-ab61-5b8054810a80"]
[description:"Final proofread and polish entire proposal" due:"1764910800" entry:"1764681766" modified:"1764681766" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54"]
[description:"Review and edit Metrics of Success section" due:"1764910800" end:"1764989912" entry:"1764681755" modified:"1764989916" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
[description:"Review and edit Risks and Contingencies section" due:"1764910800" end:"1764989916" entry:"1764681755" modified:"1764989917" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"]
[description:"Review and edit Broader Impacts section" due:"1764910800" end:"1764989917" entry:"1764681756" modified:"1764989919" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"]
[description:"Review and edit Budget section" due:"1764910800" end:"1764989919" entry:"1764681756" modified:"1764989919" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"]
[description:"Review and edit Schedule section" due:"1764910800" end:"1764989919" entry:"1764681756" modified:"1764989922" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"14fee599-fe0f-4773-90fc-c5f78291f425"]
[description:"Verify RFP compliance for all sections" due:"1764910800" end:"1764989922" entry:"1764681766" modified:"1764989923" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"a4c027fa-f50d-4efc-ab61-5b8054810a80"]
[description:"Final proofread and polish entire proposal" due:"1764910800" end:"1764989923" entry:"1764681766" modified:"1764989924" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54"]
[description:"Compile and generate final PDF" due:"1764910800" entry:"1764681766" modified:"1764681766" project:"ERLM" status:"pending" uuid:"2a8e9294-aecc-434a-b5dd-a468baf8f4a8"]

28
.task/undo.data
View File

@ -1294,3 +1294,31 @@ time 1764982196
old [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
new [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
---
time 1764989916
old [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
new [description:"Review and edit Metrics of Success section" due:"1764910800" end:"1764989912" entry:"1764681755" modified:"1764989916" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
---
time 1764989917
old [description:"Review and edit Risks and Contingencies section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"]
new [description:"Review and edit Risks and Contingencies section" due:"1764910800" end:"1764989916" entry:"1764681755" modified:"1764989917" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"]
---
time 1764989919
old [description:"Review and edit Broader Impacts section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"]
new [description:"Review and edit Broader Impacts section" due:"1764910800" end:"1764989917" entry:"1764681756" modified:"1764989919" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"]
---
time 1764989919
old [description:"Review and edit Budget section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"]
new [description:"Review and edit Budget section" due:"1764910800" end:"1764989919" entry:"1764681756" modified:"1764989919" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"]
---
time 1764989922
old [description:"Review and edit Schedule section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"14fee599-fe0f-4773-90fc-c5f78291f425"]
new [description:"Review and edit Schedule section" due:"1764910800" end:"1764989919" entry:"1764681756" modified:"1764989922" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"14fee599-fe0f-4773-90fc-c5f78291f425"]
---
time 1764989923
old [description:"Verify RFP compliance for all sections" due:"1764910800" entry:"1764681766" modified:"1764681766" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"a4c027fa-f50d-4efc-ab61-5b8054810a80"]
new [description:"Verify RFP compliance for all sections" due:"1764910800" end:"1764989922" entry:"1764681766" modified:"1764989923" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"a4c027fa-f50d-4efc-ab61-5b8054810a80"]
---
time 1764989924
old [description:"Final proofread and polish entire proposal" due:"1764910800" entry:"1764681766" modified:"1764681766" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54"]
new [description:"Final proofread and polish entire proposal" due:"1764910800" end:"1764989923" entry:"1764681766" modified:"1764989924" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54"]
---

29
Writing/ERLM/1-goals-and-outcomes/research_statement.tex
View File

@ -35,9 +35,8 @@ NASA's Formal Requirements Elicitation Tool (FRET), which structures
requirements into scope, condition, component, timing, and response elements.
This structured approach enables realizability checking to identify conflicts
and ambiguities in procedures before implementation. Second, we will synthesize
discrete mode switching logic from these specifications using reactive synthesis
tools such as Strix, which generates deterministic automata that are provably
correct by construction. Third, we will develop and verify continuous
discrete mode switching logic using reactive synthesi which generates provably
correct deterministic automata. Third, we will develop 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
@ -45,9 +44,7 @@ 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
autonomous startup controller for a Small Modular Advanced High Temperature
Reactor (SmAHTR) and implementing it on an Emerson Ovation control system using
the ARCADE hardware-in-the-loop platform.
autonomous startup controller on an Emerson Ovation control system.
% Pay-off
This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety guarantees.
@ -85,27 +82,9 @@ If this research is successful, we will be able to do the following:
guarantees. }
% Strategy
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.
% Outcome
using industry-standard control hardware. % Outcome
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}
%
% % 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.

82
Writing/ERLM/1-goals-and-outcomes/research_statement_v2.tex Normal file
View File

@ -0,0 +1,82 @@
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
control systems with event-driven control laws that have guarantees of safe and
correct behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed
written procedures to manage reactor control. Based on these procedures and
operators' interpretation of plant conditions, operators make critical decisions
about when to switch between control objectives.
% Gap
But, reliance on human operators has created an economic challenge for
next-generation nuclear power plants. Small modular reactors face significantly
higher per-megawatt staffing costs than conventional plants. Autonomous control
systems are needed that can safely manage complex operational sequences with the
same assurance as human-operated systems, but without constant supervision.
% APPROACH PARAGRAPH Solution
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.
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics
during transitions, while traditional control theory verifies continuous
behavior but lacks tools for proving discrete switching correctness.
% Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will
translate written operating procedures into temporal logic specifications using
NASA's Formal Requirements Elicitation Tool (FRET), which structures
requirements into scope, condition, component, timing, and response elements.
This structured approach enables realizability checking to identify conflicts
and ambiguities in procedures before implementation. Second, we will synthesize
discrete mode switching logic using reactive synthesis
to generate deterministic automata that are provably
correct by construction. Third, we will develop 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 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 on an Emerson Ovation control system.
% Pay-off
This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety guarantees.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
% OUTCOME 1 Title
\item \textit{Synthesize written procedures into verified control logic.}
% Strategy
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.
% Outcome
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.
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions. }
% Strategy
We will develop methods using reachability analysis to ensure continuous control modes
satisfy discrete transition requirements.
% Outcome
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.
% OUTCOME 3 Title
\item \textit{Demonstrate autonomous reactor startup control with safety
guarantees. }
% Strategy
We will implement this methodology on a small modular reactor simulation
using industry-standard control hardware. % Outcome
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}

114
Writing/ERLM/1-goals-and-outcomes/v8.tex Normal file
View File

@ -0,0 +1,114 @@
\section{Goals and Outcomes}
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct
behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service interruptions,
or radiological release.
% Known information
Currently, nuclear plant operations rely on extensively trained human operators
who follow detailed written procedures and strict regulatory requirements to
manage reactor control. These operators make critical decisions about when to
switch between different control modes based on their interpretation of plant
conditions and procedural guidance.
% Gap
This reliance on human operators prevents autonomous control capabilities and
creates a fundamental economic challenge for next-generation reactor designs.
Small modular reactors, in particular, face per-megawatt staffing costs far
exceeding those of conventional plants and threaten their economic viability.
% Critical Need
What is needed is a method to create autonomous control systems that safely
manage complex operational sequences with the same assurance as human-operated
systems, but without constant human supervision.
% APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction.
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
mirroring 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.
% Hypothesis
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. If existing
procedures can be formalized into logical specifications and continuous dynamics
verified against transition requirements, then autonomous controllers can be
built that are provably free from design defects.
% Pay-off
This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry.
% Qualifications
This work is conducted within the University of Pittsburgh Cyber Energy Center,
which provides access to industry collaboration and Emerson control hardware,
ensuring that developed solutions align with practical implementation
requirements.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
% OUTCOME 1 Title
\item \textbf{Translate written procedures into verified control logic.}
% Strategy
We will develop a methodology for converting existing written operating
procedures into formal specifications that can be automatically synthesized
into discrete control logic. This process will use structured intermediate
representations to bridge natural language procedures and mathematical
logic.
% Outcome
Control system engineers will generate verified mode-switching controllers
directly from regulatory procedures without formal methods expertise,
lowering the barrier to high-assurance control systems.
% OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy
We will establish methods for analyzing continuous control modes to ensure
they satisfy discrete transition requirements. Using classical control
theory for linear systems and reachability analysis for nonlinear dynamics,
we will verify that each continuous mode safely reaches its intended
transitions.
Engineers will design continuous controllers using standard practices while
iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times.
% OUTCOME 3 Title
\item \textbf{Demonstrate autonomous reactor startup control with safety
guarantees.}
% Strategy
We will apply this methodology to develop an autonomous controller for
nuclear reactor startup procedures, implementing it on a small modular
reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power operation.
% Outcome
We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward reduced
operator staffing while maintaining safety.
\end{enumerate}
% IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance
autonomous control will become practical for safety-critical applications.
% Impact/Pay-off
This capability is essential for the economic viability of next-generation
nuclear power. Small modular reactors offer a promising solution to growing
energy demands, but their 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 the
nuclear industry requires.

165
Writing/ERLM/2-state-of-the-art/v7.tex Normal file
View File

@ -0,0 +1,165 @@
\section{State of the Art and Limits of Current Practice}
The principal aim of this research is to create autonomous reactor control
systems that are tractably safe. To understand what is being automated, we must
first understand how nuclear reactors are operated today. This section examines
reactor operators and the operating procedures we aim to leverage, then
investigates limitations of human-based operation, and concludes with current
formal methods approaches to reactor control systems.
\subsection{Current Reactor Procedures and Operation}
Nuclear plant procedures exist in a hierarchy: normal operating procedures for
routine operations, abnormal operating procedures for off-normal conditions,
Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
developed using guidance from NUREG-0900~\cite{NUREG-0899, 10CFR50.34}, but their
development relies fundamentally on expert judgment and simulator validation
rather than formal verification. Procedures undergo technical evaluation,
simulator validation testing, and biennial review as part of operator
requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
procedures fundamentally lack formal verification of key safety properties. No
mathematical proof exists that procedures cover all possible plant states, that
required actions can be completed within available timeframes, or that
transitions between procedure sets maintain safety invariants.
\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
and completeness.} Current procedure development relies on expert judgment and
simulator validation. No mathematical proof exists that procedures cover all
possible plant states, that required actions can be completed within available
timeframes, or that transitions between procedure sets maintain safety
invariants. Paper-based procedures cannot ensure correct application, and even
computer-based procedure systems lack the formal guarantees that automated
reasoning could provide.
Nuclear plants operate with multiple control modes: automatic control, where the
reactor control system maintains target parameters through continuous reactivity
adjustment; manual control, where operators directly manipulate the reactor; and
various intermediate modes. In typical pressurized water reactor operation, the
reactor control system automatically maintains a floating average temperature
and compensates for power demand changes through reactivity feedback loops
alone. Safety systems, by contrast, operate with implemented automation. Reactor
Protection Systems trip automatically on safety signals with millisecond
response times, and engineered safety features actuate automatically on accident
signals without operator action required.
The division between automated and human-controlled functions reveals the
fundamental challenge of hybrid control. Highly automated systems handle reactor
protection---automatic trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
however, retain control of strategic decision-making: power level changes,
startup/shutdown sequences, mode transitions, and procedure implementation.
\subsection{Human Factors in Nuclear Accidents}
Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United States~\cite{operator_statistics}. These
operators divide into Reactor Operators (ROs), who manipulate reactor controls,
and Senior Reactor Operators (SROs), who direct plant operations and serve as
shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
operator requires several years of training.
The persistent role of human error in nuclear safety incidents---despite decades
of improvements in training and procedures---provides the most compelling
motivation for formal automated control with mathematical safety guarantees.
Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
including departing from normal regulations during emergencies. The Three Mile
Island (TMI) accident demonstrated how a combination of personnel error, design
deficiencies, and component failures led to partial meltdown when operators
misread confusing and contradictory readings and shut off the emergency water
system~\cite{Kemeny1979}. The President's Commission on TMI identified a
fundamental ambiguity: placing responsibility for safe power plant operations on
the licensee without formal verification that operators can fulfill this
responsibility does not guarantee safety. This tension between operational
flexibility and safety assurance remains unresolved: the person responsible for
reactor safety is often the root cause of failures.
Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus approximately
20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
Fukushima Daiichi---has been identified as poor safety management and safety
culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
of 190 events at Chinese nuclear power plants from
2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
errors, while 92\% were associated with latent errors---organizational and
systemic weaknesses that create conditions for failure.
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
that cannot be overcome through training alone.} The persistent human
error contribution despite four decades of improvements demonstrates that these
limitations are fundamental rather than a remediable part of human-driven control.
\subsection{HARDENS and Formal Methods}
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 a fundamental dilemma: existing U.S. nuclear control
rooms rely on analog technologies from the 1950s--60s. This technology is
obsolete compared to modern control systems and incurs significant risk and
cost. The NRC contracted Galois, a formal methods firm, 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 verified software.
HARDENS employed formal methods tools and techniques across the verification
hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
Requirements Elicitation Tool) to capture stakeholder requirements, domain
engineering, certification requirements, and safety requirements. Requirements
were analyzed for consistency, completeness, and realizability using SAT and SMT
solvers. Executable formal models used Cryptol to create a behavioral model of
the entire RTS, including all subsystems, components, and limited digital twin
models of sensors, actuators, and compute infrastructure. Automatic code
synthesis generated verifiable C implementations and SystemVerilog hardware
implementations directly from Cryptol models---eliminating the traditional gap
between specification and implementation where errors commonly arise.
Despite its accomplishments, HARDENS has a fundamental limitation directly
relevant to hybrid control synthesis: the project addressed only discrete
digital control logic without modeling or verifying continuous reactor dynamics.
The Reactor Trip System specification and verification covered discrete state
transitions (trip/no-trip decisions), digital sensor input processing through
discrete logic, and discrete actuation outputs (reactor trip commands). The
project did not address continuous dynamics of nuclear reactor physics. Real
reactor safety depends on the interaction between continuous
processes---temperature, pressure, neutron flux---evolving in response to
discrete control decisions. HARDENS verified the discrete controller in
isolation but not the closed-loop hybrid system behavior.
\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
continuous dynamics or hybrid system verification.} Verifying discrete control
logic alone provides no guarantee that the closed-loop system exhibits desired
continuous behavior such as stability, convergence to setpoints, or maintained
safety margins.
HARDENS produced a demonstrator system at Technology Readiness Level 2--3
(analytical proof of concept with laboratory breadboard validation) rather than
a deployment-ready system validated through extended operational testing. The
NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
considered in development, not a finalized product, and that ``The demonstration
of its technical soundness was to be at a level consistent with satisfaction of
the current regulatory criteria, although with no explicit demonstration of how
regulatory requirements are met.'' The project did not include deployment in
actual nuclear facilities, testing with real reactor systems under operational
conditions, side-by-side validation with operational analog RTS systems,
systematic failure mode testing (radiation effects, electromagnetic
interference, temperature extremes), NRC licensing review, or human factors
validation with licensed operators in realistic control room scenarios.
\textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
validation.} While formal verification provides mathematical correctness
guarantees for the implemented discrete logic, the gap between formal
verification and actual system deployment involves myriad practical
considerations: integration with legacy systems, long-term reliability
under harsh environments, human-system interaction in realistic
operational contexts, and regulatory acceptance of formal methods as
primary assurance evidence.

14
Writing/ERLM/3-research-approach/v4.tex
View File

@ -93,6 +93,8 @@ scenario because all decisions are represented by discrete variables.
Formulating operating rules using this logic enforces a finite and correct way
of operating.
Reactive synthesis is an active research field in computer science focused on
generating discrete controllers from temporal logic specifications. The term
``reactive'' indicates that the system responds to environmental inputs to
@ -166,6 +168,18 @@ control systems we aim to construct. The continuous modes will be developed
after discrete automaton construction, leveraging the automaton structure and
transitions to design multiple smaller, specialized continuous controllers.
Of note is the fact that the translation into this linear temporal logic does
something to create barriers between different control modes. Switching from one
mode to another mode becomes a discrete, boolean variable. \(RodsInserted\) or
\(HighTemp\) in the temporal specifications are booleans, but in the real system
can represent a physical feature in the state space. These features are where
continuous control modes end and begin, and their definition is critical in
defining which control mode is active at any given time. This information of
where in the state space these conditions represent will be preserved from the
original requirements by including them in the development of the continuous
control modes, but will not be considered as numeric values in the synthesis of
the discrete mode switching portion of the autonomous controller.
The discrete automaton transitions are key to the supervisory behavior of the
autonomous controller. These transitions mark decision points for switching
between continuous control modes and define their strategic objectives. We

285
Writing/ERLM/3-research-approach/v5.tex Normal file
View File

@ -0,0 +1,285 @@
\section{Research Approach}
This research will overcome the limitations of current practice to build
high-assurance hybrid control systems for critical infrastructure. Building
these systems with formal correctness guarantees requires three main thrusts:
\begin{enumerate}
\item Translate operating procedures and requirements into temporal logic
formulae
\item Create the discrete half of a hybrid controller using reactive synthesis
\item Develop continuous controllers to operate between modes, and verify
their correctness
\end{enumerate}
Commercial nuclear power operations remain manually controlled by human
operators, yet the procedures they follow are highly prescriptive and
well-documented. This suggests that human operators may not be entirely
necessary given current technology. Written procedures and requirements are
sufficiently detailed that they may be translatable into logical formulae with
minimal effort. If successful, this approach enables automation of existing
procedures without system reengineering. To formalize these procedures, we will
use temporal logic, which captures system behaviors through temporal relations.
The most efficient path for this translation is NASA's Formal Requirements
Elicitation Tool (FRET). FRET employs a specialized requirements language called
FRETish that restricts requirements to easily understood components while
eliminating ambiguity~\cite{katis_capture_2022}. FRETish bridges natural language
and mathematical specifications through a structured English-like syntax
automatically translatable to temporal logic.
FRET enforces this structure by requiring all requirements to contain six
components: %CITE FRET MANUAL
\begin{enumerate}
\item Scope: \textit{What modes does this requirement apply to?}
\item Condition: \textit{Scope plus additional specificity}
\item Component: \textit{What system element does this requirement affect?}
\item Shall
\item Timing: \textit{When does the response occur?}
\item Response: \textit{What action should be taken?}
\end{enumerate}
FRET provides functionality to check system \textit{realizability}. 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 from
their procedure definitions and design requirements present problems beyond
autonomous control implementation. Such systems contain behavioral
inconsistencies---the physical equivalent of software bugs. Using FRET during
autonomous controller development allows systematic identification and
resolution of these errors.
The second category of realizability issues involves undefined behaviors
typically left to human judgment during operations. This ambiguity is
undesirable for high-assurance systems, since even well-trained humans remain
prone to errors. Addressing these specification gaps in FRET during development
yields controllers free from these vulnerabilities.
FRET exports requirements in temporal logic format compatible with reactive
synthesis tools. Linear Temporal Logic (LTL) builds upon modal logic's
foundational operators for necessity ($\Box$, ``box'') and possibility
($\Diamond$, ``diamond''), extending them to reason about temporal
behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a
property holds at all future times (necessarily always), while the diamond
operator $\Diamond$ expresses that a property holds at some future time
(possibly eventually). These are complemented by the next operator ($X$) for the
immediate successor state and the until operator ($U$) for expressing
persistence conditions.
Consider a nuclear reactor SCRAM requirement expressed in natural language:
\textit{``If a high temperature alarm triggers, control rods must immediately
insert and remain inserted until operator reset.''} This plain language
requirement can be translated into a rigorous logical specification:
\begin{equation}
\Box(HighTemp \rightarrow X(RodsInserted \wedge (\neg
RodsWithdrawn\ U\ OperatorReset)))
\end{equation}
This specification precisely captures the temporal relationship between the
alarm condition, the required response, and the persistence requirement. The
necessity operator $\Box$ ensures this safety property holds throughout all
possible future system executions, while the next operator $X$ enforces
immediate response. The until operator $U$ maintains the state constraint until
the reset condition occurs. No ambiguity exists in this scenario because all
decisions are represented by discrete variables. Formulating operating rules in
this logic enforces finite, correct operation.
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, with each node representing a unique
discrete state. The connections between nodes, called \textit{state
transitions}, specify the conditions under which the discrete controller moves
from state to state. This complete mapping of possible states and transitions
constitutes a \textit{discrete automaton}. Discrete automata can be represented
graphically as nodes (discrete states) with edges indicating transitions between
them. From the automaton graph, one can fully describe discrete system dynamics
and develop intuitive understanding of system behavior. Hybrid systems naturally
exhibit discrete behavior amenable to formal analysis through these finite state
representations.
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
which has demonstrated superior performance in the Reactive Synthesis
Competition (SYNTCOMP) through efficient parity game solving
algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix translates linear
temporal logic specifications into deterministic automata automatically while
maximizing generated automata quality. Once constructed, the automaton can be
implemented using standard programming control flow constructs. The graphical
representation enables inspection and facilitates communication with controls
programmers who lack formal methods expertise.
We will use discrete automata to represent the switching behavior of our hybrid
system. This approach yields an important theoretical guarantee: because the
discrete automaton is synthesized entirely through automated tools from design
requirements and operating procedures, the automaton---and therefore our hybrid
switching behavior---is \textit{correct by construction}. Correctness of the
switching controller 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 with capabilities extending beyond written procedures.
Autonomous control lacks this adaptive advantage. Instead, autonomous
controllers replacing human operators must not make switching errors between
continuous modes. Synthesizing controllers from logical specifications with
guaranteed correctness eliminates the possibility of switching errors.
While discrete system components will be synthesized with correctness
guarantees, they represent only half of the complete system. Autonomous
controllers like those we are developing exhibit continuous dynamics within
discrete states. These systems, called hybrid systems, combine continuous
dynamics (flows) with discrete transitions (jumps). These dynamics can be
formally expressed as~\cite{branicky_multiple_1998}:
\begin{equation}
\dot{x}(t) = f(x(t),q(t),u(t))
\end{equation}
\begin{equation}
q(k+1) = \nu(x(k),q(k),u(k))
\end{equation}
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
discrete transitions. The continuous states $x$, discrete state $q$, and
control input $u$ interact to produce hybrid behavior. The discrete state $q$
defines which continuous dynamics mode is currently active. Our focus centers
on continuous autonomous hybrid systems, where continuous states remain
unchanged during jumps---a property naturally exhibited by physical systems. For
example, a nuclear reactor switching from warm-up to load-following control
cannot instantaneously change its temperature or control rod position, but can
instantaneously change control laws.
The approach described for producing discrete automata yields physics-agnostic
specifications representing only half of a complete hybrid autonomous
controller. These automata alone cannot define the full behavior of the control
systems we aim to construct. The continuous modes will be developed after
discrete automaton construction, leveraging the automaton structure and
transitions to design multiple smaller, specialized continuous controllers.
Notably, translation into linear temporal logic creates barriers between
different control modes. Switching from one mode to another becomes a discrete
boolean variable. \(RodsInserted\) or \(HighTemp\) in the temporal
specifications are booleans, but in the real system they represent physical
features in the state space. These features mark where continuous control modes
end and begin; their definition is critical for determining which control mode
is active at any given time. Information about where in the state space these
conditions exist will be preserved from the original requirements and included
in continuous control mode development, but will not appear as numeric values in
discrete mode switching synthesis.
The discrete automaton transitions are key to the supervisory behavior of the
autonomous controller. These 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 based
on discrete mode transitions:
\begin{enumerate}
\item \textbf{Stabilizing:} A stabilizing control mode has one primary
objective: maintaining the hybrid system within its current discrete mode.
This corresponds to steady-state normal operating modes, such as a
full-power load-following controller in a nuclear power plant. Stabilizing
modes can be identified from discrete automata as nodes with only incoming
transitions.
\item \textbf{Transitory:} A transitory control mode has the primary goal of
transitioning the hybrid system from one discrete state to another. In
nuclear applications, this might represent a controlled warm-up procedure.
Transitory modes ultimately drive the system toward a stabilizing
steady-state mode. These modes may have secondary objectives within a
discrete state, such as maintaining specific temperature ramp rates before
reaching full-power operation.
\item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode
with additional safety constraints. Expulsory modes ensure the system is
directed to a safe stabilizing mode during failure conditions. For example,
if a transitory mode fails to achieve its intended transition, the
expulsory mode activates to immediately and irreversibly guide the system
toward a globally safe state. A reactor SCRAM exemplifies an expulsory
continuous mode: when initiated, it must reliably terminate the nuclear
reaction and direct the reactor toward stabilizing decay heat removal.
\end{enumerate}
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~\cite{branicky_multiple_1998}. Current techniques struggle with this
problem because dynamic discontinuities complicate
verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. This
work alleviates these problems by designing continuous controllers specifically
with transitions in mind. Decomposing continuous modes according to their
required behavior at transition points avoids solving trajectories through the
entire hybrid system. Instead, local behavior information at transition
boundaries suffices. To ensure continuous modes satisfy their requirements, we
employ three main techniques: reachability analysis, assume-guarantee contracts,
and barrier certificates.
Reachability analysis computes the reachable set of states for a given input
set. While trivial for linear continuous systems, recent advances have extended
reachability to complex nonlinear
systems~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We use
reachability to define continuous state ranges at discrete transition boundaries
and verify that requirements are satisfied within continuous modes.
Assume-guarantee contracts apply 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, enabling reachability analysis without global
system analysis. Finally, barrier certificates prove that mode transitions are
satisfied. Barrier certificates ensure that continuous modes on either side of a
transition behave appropriately by preventing system trajectories from crossing
a given barrier. Control barrier functions certify safety by establishing
differential inequality conditions that guarantee forward invariance of safe
sets~\cite{prajna_safety_2004}. For example, a barrier certificate can guarantee
that a transitory mode transferring control to a stabilizing mode will always
move away from the transition boundary, rather than destabilizing the target
stabilizing mode.
This compositional approach has several advantages. First, this approach breaks
down autonomous controller design into smaller pieces. For designers of future
autonomous control systems, the barrier to entry is low, and design milestones
are clear due to the procedural nature of this research plan. Second, measurable
design progress also enables measurement of regulatory adherence. Each step in
this development procedure generates an artifact that can be independently
evaluated as proof of safety and performance. Finally, the compositional nature
of this development plan enables incremental refinement between control system
layers. For example, difficulty developing a continuous mode may reflect a
discrete automaton that is too restrictive, prompting refinement of system
design requirements. This synthesis between levels promotes broader
understanding of the autonomous controller.
To demonstrate this methodology, we will develop an autonomous startup
controller for a Small Modular Advanced High Temperature Reactor (SmAHTR). We
have already developed a high-fidelity SmAHTR model in Simulink that captures
the thermal-hydraulic and neutron kinetics behavior essential for verifying
continuous controller performance under realistic plant dynamics. The
synthesized hybrid controller will be implemented on an Emerson Ovation control
system platform, representative of industry-standard control hardware deployed
in modern nuclear facilities. 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 interfacing
with a realistic reactor simulation, assessing computational performance,
real-time execution constraints, and communication latency effects.
Demonstrating autonomous startup control on this representative platform will
establish both the theoretical validity and practical feasibility of the
synthesis methodology for deployment in actual small modular reactor systems.
This unified approach addresses a fundamental gap in hybrid system design by
bridging formal methods and control theory through a systematic, tool-supported
methodology. Translating existing nuclear procedures into temporal logic,
synthesizing provably correct discrete switching logic, and developing verified
continuous controllers creates a complete framework for autonomous hybrid
control with mathematical guarantees. The result is an autonomous controller
that not only replicates human operator decision-making but does so with formal
assurance that switching logic is correct by construction and continuous
behavior satisfies safety requirements. This methodology transforms nuclear
reactor control from a manually intensive operation requiring constant human
oversight into a fully autonomous system with higher reliability than
human-operated alternatives. More broadly, this approach establishes a
replicable framework for developing high-assurance autonomous controllers in any
domain where operating procedures are well-documented and safety is paramount.

76
Writing/ERLM/4-metrics-of-success/v2.tex
View File

@ -1,12 +1,12 @@
\newpage
\section{Metrics for 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
section explains why TRL advancement provides the most appropriate success
metric and defines the specific criteria required to achieve TRL 5.
demonstration. The work presented in HARDENS begins at TRL 2-3 and aims to reach
TRL 5, where system components operate successfully in a relevant laboratory
environment. This section explains why TRL advancement provides the most
appropriate success metric and defines the specific criteria required to achieve
TRL 5.
Technology Readiness Levels provide the ideal success metric because they
explicitly measure the gap between academic proof-of-concept and practical
@ -30,18 +30,12 @@ uses TRLs for technology assessment, making this metric directly relevant to
potential adopters. Reaching TRL 5 provides a clear answer to industry questions
about feasibility and maturity in a way that academic publications alone cannot.
The work currently exists at TRL 2-3. Formal synthesis and hybrid control
verification principles have been established through prior research, placing
the fundamental approach at TRL 2. The SmAHTR simulation model and initial
procedure analysis place specific components at early TRL 3, where proof of
concept has been partially demonstrated for individual elements but not
integrated. The target state is TRL 5. Moving from current state to target
requires achieving three intermediate levels, each representing a distinct
validation milestone:
Moving from current state to target requires achieving three intermediate
levels, each representing a distinct validation milestone:
\paragraph{TRL 3 \textit{Critical Function and Proof of Concept}}
For this research, TRL 3 means demonstrating that each component of the
methodology works in isolation. SmAHTR startup procedures must be translated
methodology 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 reachability analysis proving that
@ -51,7 +45,7 @@ approach on a simplified startup sequence.
\paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
For this research, TRL 4 means demonstrating a complete integrated hybrid
controller in simulation. All SmAHTR startup procedures must be formalized with
controller in simulation. All startup procedures must be formalized with
a synthesized automaton covering all operational modes. Continuous controllers
must exist for all discrete modes. Verification must be complete for all mode
transitions using reachability analysis, barrier certificates, and
@ -60,28 +54,23 @@ startup sequences in software simulation with zero safety violations across
multiple consecutive runs. This proves that formal correctness guarantees can be
maintained throughout system integration.
\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
For this research, TRL 5 means demonstrating the verified controller on
industrial control hardware through hardware-in-the-loop testing. The discrete
automaton must be implemented on the Emerson Ovation control system and verified
to match synthesized specifications exactly. Continuous controllers must execute
at required rates. The ARCADE interface must establish stable real-time
communication between Ovation hardware and SmAHTR simulation. Complete
autonomous startup sequences must execute via hardware-in-the-loop across the
full operational envelope. The controller must handle off-nominal scenarios to
validate that expulsory modes function correctly. For example, simulated sensor
failures must trigger appropriate fault detection and mode transitions, and loss
of cooling scenarios must activate SCRAM procedures as specified. Graded
responses to minor disturbances are outside the scope of this work. Formal
verification results must remain valid with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable on
industrial hardware.
These levels define progressively more demanding demonstrations. TRL 3 proves
individual components work. TRL 4 proves they work together in simulation. TRL 5
proves they work on actual hardware in realistic conditions. Each level builds
on the previous while adding new validation requirements.
\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}} For this
research, TRL 5 means demonstrating the verified controller on industrial
control hardware through hardware-in-the-loop testing. The discrete automaton
must be implemented on the Emerson Ovation control system and verified to match
synthesized specifications exactly. Continuous controllers must execute at
required rates. The ARCADE interface must establish stable real-time
communication between the Emerson Ovation hardware and SmAHTR simulation.
Complete autonomous startup sequences must execute via hardware-in-the-loop
across the full operational envelope. The controller must handle off-nominal
scenarios to validate that expulsory modes function correctly. For example,
simulated sensor failures must trigger appropriate fault detection and mode
transitions, and loss of cooling scenarios must activate SCRAM procedures as
specified. Graded responses to minor disturbances are outside the scope of this
work. Formal verification results must remain valid with discrete behavior
matching specifications and continuous trajectories remaining within verified
bounds. This proves that the methodology produces verified controllers
implementable on industrial hardware.
Progress will be assessed quarterly through collection of specific data
comparing actual results against TRL advancement criteria. Specification
@ -89,18 +78,9 @@ development status indicates progress toward TRL 3. Synthesis results and
verification coverage indicate progress toward TRL 4. Simulation performance
metrics and hardware integration milestones indicate progress toward TRL 5. The
research plan will be revised only when new data invalidates fundamental
assumptions. Unrealizable specifications indicate procedure conflicts requiring
refinement or alternative reactor selection. Unverifiable dynamics suggest model
simplification or alternative verification methods are needed. Unachievable
real-time performance requires controller simplification or hardware upgrades.
Any revision will document the invalidating data, the failed assumption, and the
modified pathway with adjusted scope.
This research succeeds if it achieves TRL 5 by demonstrating a complete
assumptions. This research succeeds if it achieves TRL 5 by demonstrating a complete
autonomous hybrid controller with formal correctness guarantees operating on
industrial control hardware through hardware-in-the-loop testing in a relevant
laboratory environment. This establishes both theoretical validity and practical
feasibility, proving that the methodology produces verified controllers and that
implementation is achievable with current technology. It provides a clear
pathway for nuclear industry adoption and broader application to safety-critical
autonomous systems.
implementation is achievable with current technology.

88
Writing/ERLM/4-metrics-of-success/v3.tex Normal file
View File

@ -0,0 +1,88 @@
\section{Metrics for Success}
This research will be measured by advancement through Technology Readiness
Levels, progressing from fundamental concepts to validated prototype
demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
system components operate successfully in a relevant laboratory environment.
This section explains why TRL advancement provides the most appropriate success
metric and defines the specific criteria required to achieve TRL 5.
Technology Readiness Levels provide the ideal success metric because they
explicitly measure the gap between academic proof-of-concept and practical
deployment---precisely what this work aims to bridge. Academic metrics like
papers published or theorems proved cannot capture practical feasibility.
Empirical metrics like simulation accuracy or computational speed cannot
demonstrate theoretical rigor. TRLs measure both dimensions simultaneously.
Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
progressively demonstrating practical feasibility. Formal verification must
remain valid as the system moves from individual components to integrated
hardware testing.
The nuclear industry requires extremely high assurance before deploying new
control technologies. Demonstrating theoretical correctness alone is
insufficient for adoption; conversely, showing empirical performance without
formal guarantees fails to meet regulatory requirements. TRLs capture this dual
requirement naturally. Each level represents both increased practical maturity
and sustained theoretical validity. Furthermore, TRL assessment forces explicit
identification of remaining barriers to deployment. The nuclear industry already
uses TRLs for technology assessment, making this metric directly relevant to
potential adopters. Reaching TRL 5 provides a clear answer to industry questions
about feasibility and maturity that academic publications alone cannot.
Moving from current state to target requires achieving three intermediate
levels, each representing a distinct validation milestone:
\paragraph{TRL 3 \textit{Critical Function and Proof of Concept}}
For this research, TRL 3 means demonstrating that each component of the
methodology 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 reachability analysis proving
transition requirements are satisfied. Independent review must confirm that
specifications match intended procedural behavior. This proves the fundamental
approach on a simplified startup sequence.
\paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
For this research, TRL 4 means demonstrating a complete integrated hybrid
controller in simulation. All startup procedures must be formalized with a
synthesized automaton covering all operational modes. Continuous controllers
must exist for all discrete modes. Verification must be complete for all mode
transitions using reachability analysis, barrier certificates, and
assume-guarantee contracts. The integrated controller must execute complete
startup sequences in software simulation with zero safety violations across
multiple consecutive runs. This proves that formal correctness guarantees can be
maintained throughout system integration.
\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
For this research, TRL 5 means demonstrating the verified controller on
industrial control hardware through hardware-in-the-loop testing. The discrete
automaton must be implemented on the Emerson Ovation control system and verified
to match synthesized specifications exactly. Continuous controllers must execute
at required rates. The ARCADE interface must establish stable real-time
communication between the Emerson Ovation hardware and SmAHTR simulation.
Complete autonomous startup sequences must execute via hardware-in-the-loop
across the full operational envelope. The controller must handle off-nominal
scenarios to validate that expulsory modes function correctly. For example,
simulated sensor failures must trigger appropriate fault detection and mode
transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
specified. Graded responses to minor disturbances are outside this work's scope.
Formal verification results must remain valid, with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable on
industrial hardware.
Progress will be assessed quarterly through collection of specific data
comparing actual results against TRL advancement criteria. Specification
development status indicates progress toward TRL 3. Synthesis results and
verification coverage indicate progress toward TRL 4. Simulation performance
metrics and hardware integration milestones indicate progress toward TRL 5. The
research plan will be revised only when new data invalidates fundamental
assumptions. This research succeeds if it achieves TRL 5 by demonstrating a
complete autonomous hybrid controller with formal correctness guarantees
operating on industrial control hardware through hardware-in-the-loop testing in
a relevant laboratory environment. This establishes both theoretical validity
and practical feasibility, proving that the methodology produces verified
controllers and that implementation is achievable with current technology.

78
Writing/ERLM/5-risks-and-contingencies/v2.tex
View File

@ -1,4 +1,3 @@
\newpage
\section{Risks and Contingencies}
This research relies on several critical assumptions that, if invalidated,
@ -30,7 +29,7 @@ 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
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.
@ -45,24 +44,6 @@ 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
@ -121,7 +102,7 @@ computational resources where they matter most for safety assurance.
\subsection{Procedure Formalization Completeness}
The third assumption is that existing SmAHTR startup procedures contain
The third assumption is that existing 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
@ -175,58 +156,5 @@ 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.
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.

158
Writing/ERLM/5-risks-and-contingencies/v3.tex Normal file
View File

@ -0,0 +1,158 @@
\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, creating 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 complete procedures are intractable. Generated automata containing
more than 1,000 discrete states would indicate 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.
\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
requiring 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 the interface between discrete guards and continuous
invariants is too complex. Failure to construct barrier certificates proving
safety across mode transitions would reveal that 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 the synthesized discrete controller is
incompatible with achievable continuous behavior.
The primary contingency for interface complexity is restricting 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 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 procedures do not form a complete
specification. Multiple valid interpretations of procedural steps with no clear
resolution would demonstrate 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 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 specific
quirks.

1
Writing/ERLM/6-broader-impacts/v2.tex
View File

@ -1,4 +1,3 @@
\newpage
\section{Broader Impacts}
Nuclear power presents both a compelling application domain and an urgent

71
Writing/ERLM/6-broader-impacts/v3.tex Normal file
View File

@ -0,0 +1,71 @@
\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 (SMRs), particularly
for hyperscale datacenters requiring hundreds of megawatts of continuous power.
Deploying SMRs at datacenter sites would minimize transmission losses and
eliminate emissions from hydrocarbon-based alternatives. However, nuclear power
economics at this scale demand careful attention to operating costs.
According to the U.S. Energy Information Administration's Annual Energy Outlook
2022, advanced nuclear power entering service in 2027 is projected to cost
\$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is
projected to reach 1,050 terawatt-hours annually by
2030~\cite{eesi_datacenter_2024}. If this demand were supplied by nuclear power,
the total annual cost of power generation would exceed \$92 billion. Within this
figure, operations and maintenance represents a substantial component. The EIA
estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour,
with additional variable O\&M costs embedded in fuel and operating
expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
approximately 23--30\% of the total levelized cost of electricity, translating
to \$21--28 billion annually for projected datacenter demand.
This research directly addresses the multi-billion-dollar O\&M cost challenge
through high-assurance autonomous control. Current nuclear operations require
full control room staffing for each reactor, whether large conventional units or
small modular designs. These staffing requirements drive the high O\&M costs
that make nuclear power economically challenging, particularly for smaller
reactor designs where the same staffing overhead must be spread across lower
power output. Synthesizing provably correct hybrid controllers from formal
specifications 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 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. Formally verifying both the
discrete mode-switching logic and the continuous control behavior, this research
will produce controllers with mathematical proofs of correctness. These
guarantees enable automation to safely handle routine operations---startup
sequences, power level changes, and normal operational transitions---that
currently require human operators to follow written procedures. Operators will
remain in supervisory roles to handle off-normal conditions and provide
authorization for major operational changes, but the routine cognitive burden of
procedure execution shifts to provably correct automated systems that are much
cheaper to operate.
SMRs represent an ideal deployment target for this technology. Nuclear
Regulatory Commission certification requires extensive documentation of control
procedures, operational requirements, and safety analyses written in structured
natural language. As described in our approach, these regulatory documents can
be translated into temporal logic specifications using tools like FRET, then
synthesized into discrete switching logic using reactive synthesis tools, and
finally verified using reachability analysis and barrier certificates for the
continuous control modes. The infrastructure of requirements and specifications
already exists as part of the licensing process, creating a direct pathway from
existing regulatory documentation to formally verified autonomous controllers.
Beyond reducing operating costs for new reactors, 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, where similar economic and safety considerations favor increased
autonomy with provable correctness guarantees. Demonstrating this approach in
nuclear power---one of the most regulated and safety-critical domains---will
establish both the technical feasibility and regulatory pathway for broader
adoption across critical infrastructure.

4
Writing/ERLM/7-budget/v1.tex
View File

@ -145,7 +145,7 @@ Materials and Supplies (Section G).
and faculty advisor to attend one major control systems conference annually to
disseminate research results. The budget assumes domestic conference attendance
with costs including: airfare, hotel, meals and incidentals, ground
transportation , and registration for both attendees per conference.
transportation, and registration for both attendees per conference.
\paragraph{Industry Collaboration Visits (\$1,500 per year)} Funds are requested
for travel to industry partner sites and potential nuclear facilities to: (1)
validate reactor operating procedures with domain experts; (2) present research
@ -254,7 +254,7 @@ project, significant in-kind contributions will support the research:
\paragraph{Emerson Process Management Partnership} Through the University of
Pittsburgh Cyber Energy Center, Emerson Process Management will provide access
to Ovation distributed control system hardware and ARCADE hardware-in- the-loop
to Ovation distributed control system hardware and ARCADE hardware-in-the-loop
interface software. This equipment is essential for TRL 5 validation and
represents industry-standard control systems deployed in nuclear facilities.
Emerson will also provide technical consultation and domain expertise for

182
Writing/ERLM/7-budget/v2.tex Normal file
View File

@ -0,0 +1,182 @@
% Required packages:
% \usepackage{booktabs}
% \usepackage{tabularx}
% \usepackage{multirow}
% \usepackage{array}
% \usepackage[table]{xcolor} % optional, for alternating row colors
\section{Budget and Budget Justification}
\subsection{Budget Summary}
The proposed research will be conducted over three (3) years,
corresponding to the expected completion timeline for the PhD
dissertation. Table~\ref{tab:budget} provides a detailed breakdown
of costs by category and year.
\begin{table}[htbp]
\centering
\caption{Proposed Budget by Year and Category}
\label{tab:budget}
\small
\begin{tabular}{@{}lrrrr@{}}
\toprule
\textbf{Category} & \textbf{Year 1} & \textbf{Year 2} &
\textbf{Year 3} & \textbf{Total} \\
\midrule
\multicolumn{5}{l}{\textbf{Senior Personnel}} \\
\quad Faculty (PI Advisor, 1 mo.) & \$12,083 & \$12,566 &
\$13,069 & \$37,718 \\
\addlinespace
\multicolumn{5}{l}{\textbf{Other Personnel}} \\
\quad Graduate Research Assistant & \$38,000 & \$39,520 &
\$41,101 & \$118,621 \\
\addlinespace
\multicolumn{5}{l}{\textbf{Fringe Benefits}} \\
\quad Faculty Fringe Benefits (29.6\%) & \$3,577 & \$3,720 &
\$3,868 & \$11,165 \\
\quad GRA Fringe Benefits (50\%) & \$19,000 & \$19,760 &
\$20,551 & \$59,311 \\
\cmidrule{2-5}
\quad \textit{Fringe Benefits Subtotal} & \$22,577 & \$23,480 &
\$24,419 & \$70,476 \\
\addlinespace
\multicolumn{5}{l}{\textbf{Equipment}} \\
\quad (No equipment over \$5,000) & --- & --- & --- & --- \\
\addlinespace
\multicolumn{5}{l}{\textbf{Travel}} \\
\quad Conference Travel (Domestic) & \$4,000 & \$4,000 &
\$4,000 & \$12,000 \\
\quad Industry Collaboration Visits & \$1,500 & \$1,500 &
\$1,500 & \$4,500 \\
\cmidrule{2-5}
\quad \textit{Travel Subtotal} & \$5,500 & \$5,500 &
\$5,500 & \$16,500 \\
\addlinespace
\multicolumn{5}{l}{\textbf{Participant Support Costs}} \\
\quad (Not applicable) & --- & --- & --- & --- \\
\addlinespace
\multicolumn{5}{l}{\textbf{Other Direct Costs}} \\
\quad \textit{Materials and Supplies:} & & & & \\
\quad \quad High-Performance Workstation & \$3,500 & --- &
--- & \$3,500 \\
\quad \quad Laboratory Materials \& Supplies & \$1,500 & \$1,000 &
\$1,000 & \$3,500 \\
\quad \textit{Publication Costs} & \$1,000 & \$1,500 &
\$2,000 & \$4,500 \\
\quad \textit{Computing/Cloud Services} & \$1,500 & \$1,500 &
\$1,500 & \$4,500 \\
\cmidrule{2-5}
\quad \textit{Other Direct Costs Subtotal} & \$7,500 & \$4,000 &
\$4,500 & \$16,000 \\
\addlinespace
\midrule
\textbf{Total Direct Costs} & \$85,660 & \$85,066 &
\$88,589 & \$259,315 \\
\addlinespace
\multicolumn{5}{l}{\textbf{H. Indirect Costs (F\&A)}} \\
\quad On-Campus Research (56\% MTDC) & \$35,326 & \$34,488 &
\$35,935 & \$105,749 \\
\addlinespace
\midrule
\textbf{TOTAL PROJECT COST} & \$120,986 & \$119,554 &
\$124,524 & \$365,064 \\
\bottomrule
\end{tabular}
\end{table}
\subsection{Budget Justification}
\subsubsection{Senior Personnel}
\paragraph{Faculty Advisor}
Funds are requested to support one month of summer salary per year
for the faculty advisor (estimated at Associate Professor level,
\$96,459/year base salary for 8 academic months = \$12,083/month).
A 4\% annual salary increase is applied in subsequent years.
\subsubsection{Other Personnel}
\paragraph{Graduate Research Assistant (Principal Investigator)}
Funds are requested to support one full-time graduate research
assistant (the PI) for the entire duration of the project at
\$38,000 per year in Year 1. This represents a standard graduate
research assistantship stipend at the University of Pittsburgh for
a PhD student in the Swanson School of Engineering. A 4\% annual
salary increase is included in Years 2 and 3 to account for
cost-of-living adjustments.
\subsubsection{Fringe Benefits}
\paragraph{Faculty Fringe Benefits}
Faculty fringe benefits are calculated at 29.6\%, the University of
Pittsburgh's approved rate for academic year faculty, covering
retirement contributions, health insurance, and other benefits.
\paragraph{Graduate Research Assistant Fringe Benefits}
Fringe benefits for the GRA are calculated at 50\% of salary,
consistent with University of Pittsburgh rates for graduate students
on research assistantships.
\subsubsection{Travel}
\paragraph{Conference Travel (\$4,000 per year)} Funds are requested for the PI
and faculty advisor to attend one major control systems conference annually to
disseminate research results. The budget assumes domestic conference attendance
with costs including: airfare, hotel, meals and incidentals, ground
transportation, and registration for both attendees per conference.
\paragraph{Industry Collaboration Visits (\$1,500 per year)} Funds are requested
for travel to industry partner sites and potential nuclear facilities to: (1)
validate reactor operating procedures with domain experts; (2) present research
progress to industry stakeholders; (3) gather feedback on practical
implementation considerations; and (4) explore deployment pathways for the
developed technology.
\subsubsection{Other Direct Costs}
\paragraph{Materials and Supplies}
\textit{High-Performance Workstation (\$3,500, Year 1):} A dedicated
high-performance workstation is required for computationally intensive tasks
including. The workstation specifications include: Intel Core i9 or AMD Ryzen 9
processor (minimum 16 cores), 64 GB RAM, 2 TB NVMe SSD storage, and NVIDIA GPU
for potential acceleration of numerical computations.
\textit{Laboratory Materials and Supplies (\$1,500 Year 1; \$1,000 Years 2--3):}
Funds are requested for laboratory supplies and materials including: electronic
components and sensors for hardware integration, cables and connectors for
hardware-in-the-loop setup, and miscellaneous computing accessories such as
external storage devices and backup media.
\paragraph{Publication Costs}
Funds are requested to cover publication fees for disseminating
research results in high-quality peer-reviewed venues. Budget
includes:
\begin{itemize}
\item Year 1 (\$1,000): Conference proceedings fees and one journal
submission
\item Year 2 (\$1,500): Open-access publication charges for first
major journal paper
\item Year 3 (\$2,000): Open-access publication charges for
dissertation-culminating journal papers
\end{itemize}
Open-access publication is prioritized to maximize research impact
and accessibility, particularly important for work with potential
nuclear safety applications. Many high-impact journals (IEEE
Transactions on Automatic Control, Automatica) charge
\$1,000--\$2,000 for open access.
\paragraph{Computing and Cloud Services} Funds are requested for cloud computing
resources and online services. Cloud computing provides scalable
computational resources for particularly demanding verification problems without
requiring additional capital equipment purchases.
\subsubsection{H. Indirect Costs (Facilities \& Administrative)}
Indirect costs are calculated at 56\% of Modified Total Direct Costs
(MTDC), which is the University of Pittsburgh's federally negotiated
rate for on-campus research. MTDC includes all direct costs except
equipment purchases over \$5,000, tuition remission, and certain
other exclusions. The calculation base includes all personnel costs,
travel, and other direct costs as shown in the budget table.

2
Writing/ERLM/8-schedule/v1.tex
View File

@ -70,7 +70,7 @@ Six major milestones mark critical validation points throughout the research. M1
translated to temporal logic using FRET with realizability analysis
demonstrating consistent and complete specifications. Domain expert review
validates that formalized specifications accurately capture procedural intent.
This milestone delivers an internal technical report documenting the t ranslation methodology and complete specification set.
This milestone delivers an internal technical report documenting the translation methodology and complete specification set.
M2 (Month 8) validates computational tractability by demonstrating that Strix
can synthesize a complete discrete automaton from the formalized specifications.

96
Writing/ERLM/8-schedule/v2.tex Normal file
View File

@ -0,0 +1,96 @@
\section{Schedule, Milestones, and Deliverables}
This research will be conducted over six trimesters (24 months) of full-time
effort following the proposal defense in Spring 2026. The work progresses
sequentially through three main research thrusts before culminating in
integrated demonstration and validation.
The first semester (Spring 2026) focuses on Thrust 1, translating startup
procedures into formal temporal logic specifications using FRET. This
establishes the foundation for automated synthesis by converting natural
language procedures into machine-readable requirements. The second semester
(Summer 2026) addresses Thrust 2, using Strix to synthesize the discrete
automaton that defines mode-switching behavior. With the discrete structure
established, the third semester (Fall 2026) develops the continuous controllers
for each operational mode through Thrust 3, employing reachability analysis and
barrier certificates to verify that each mode satisfies its transition
requirements. Integration and validation occupy the remaining three semesters.
Figure \ref{fig:gantt} shows the complete project schedule including research thrusts, major milestones, and planned publications.
\begin{figure}[htbp]
\centering
\begin{ganttchart}[
hgrid,
vgrid={*{4}{draw=none}, dotted},
x unit=0.4cm,
y unit title=0.6cm,
y unit chart=0.4cm,
title/.append style={fill=gray!30},
title height=1,
bar/.append style={fill=blue!50},
bar height=0.5,
bar label font=\small,
milestone/.append style={fill=red, shape=diamond},
milestone height=0.5
]{1}{24}
% Timeline headers
\gantttitle{2026}{12}
\gantttitle{2027}{12} \\
\gantttitle{Spring}{4}
\gantttitle{Summer}{4}
\gantttitle{Fall}{4}
\gantttitle{Spring}{4}
\gantttitle{Summer}{4}
\gantttitle{Fall}{4} \\
% Major thrusts
\ganttbar{Thrust 1: Procedure Translation}{1}{5} \\
\ganttbar{Thrust 2: Discrete Synthesis}{4}{10} \\
\ganttbar{Thrust 3: Continuous Control}{9}{15} \\
\ganttbar{Integration \& Simulation (TRL 4)}{13}{17} \\
\ganttbar{Hardware-in-Loop Testing (TRL 5)}{16}{21} \\
\ganttbar{Dissertation Writing}{18}{24} \\[grid]
% Milestones row
\ganttbar[bar/.append style={fill=orange!50}]{Milestones}{1}{24}
\ganttmilestone{}{4}
\ganttmilestone{}{8}
\ganttmilestone{}{12}
\ganttmilestone{}{16}
\ganttmilestone{}{20}
\ganttmilestone{}{24} \\
% Publications row
\ganttbar[bar/.append style={fill=green!50}]{Publications}{1}{24}
\ganttmilestone{}{8}
\ganttmilestone{}{16}
\ganttmilestone{}{20}
\end{ganttchart}
\caption{Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}
\label{fig:gantt}
\end{figure}
\subsection{Milestones and Deliverables}
Six major milestones mark critical validation points throughout the research. M1
(Month 4) confirms that startup procedures have been successfully translated to
temporal logic using FRET with realizability analysis demonstrating consistent
and complete specifications. M2 (Month 8) validates computational tractability
by demonstrating that Strix can synthesize a complete discrete automaton from
the formalized specifications. This milestone delivers a conference paper
submission to NPIC\&HMIT documenting the procedure-to-specification translation
methodology. M3 (Month 12) achieves TRL 3 by proving that continuous controllers
can be designed and verified to satisfy discrete transition requirements. This
milestone delivers an internal technical report demonstrating component-level
verification. M4 (Month 16) achieves TRL 4 through integrated simulation
demonstrating that component-level correctness composes to system-level
correctness. This milestone delivers a journal paper submission to IEEE
Transactions on Automatic Control presenting the complete hybrid synthesis
methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
implementability on industrial hardware. This milestone delivers a conference
paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
experimental validation. M6 (Month 24) completes the dissertation documenting
the entire methodology, experimental results, and research contributions.

BIN
Writing/ERLM/ERLM_Request_for_Proposals.pdf Normal file
View File

Binary file not shown.

BIN
Writing/ERLM/SABO_FINAL_ERLM_PROPOSAL.pdf Normal file
View File

Binary file not shown.

2
Writing/ERLM/dane_proposal_format.cls
View File

@ -95,7 +95,7 @@
\newcommand{\emphitem}[1]{\item \emph{#1:}}
% Default document metadata (can be overridden)
\title{From Cold Start to Critical:\\ Formal Synthesis of Hybrid Controllers}
\title{From Cold Start to Critical:\\ Formal Synthesis of Autonomous Hybrid Controllers}
\author{%
PI: Dane A. Sabo\\
dane.sabo@pitt.edu\\

87
Writing/ERLM/main.aux
View File

@ -1,5 +1,6 @@
\relax
\providecommand \oddpage@label [2]{}
\@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
\citation{NUREG-0899,10CFR50.34}
\citation{10CFR55.59}
@ -13,33 +14,36 @@
\citation{WNA2020}
\citation{hogberg_root_2013}
\citation{zhang_analysis_2025}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent }
\citation{katis_capture_2022}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
\citation{baier_principles_2008}
\citation{meyer_strix_2018,jacobs_reactive_2024}
\citation{a}
\citation{branicky_multiple_1998}
\citation{branicky_multiple_1998}
\citation{bansal_hamilton-jacobi_2017,guernic_reachability_2009}
\citation{frehse_spaceex_2011,mitchell_time-dependent_2005}
\citation{prajna_safety_2004}
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{9}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{12}{}\protected@file@percent }
\citation{eia_lcoe_2022}
\citation{eesi_datacenter_2024}
\citation{eia_lcoe_2022}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}\protected@file@percent }
\gtt@chartextrasize{0}{164.1287pt}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{15}{}\protected@file@percent }
\newlabel{fig:gantt}{{1}{15}{Schedule, Milestones, and Deliverables}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{15}{}\protected@file@percent }
\bibstyle{ieeetr}
\bibdata{references}
\bibcite{NUREG-0899}{1}
@ -59,7 +63,7 @@
\bibcite{baier_principles_2008}{15}
\bibcite{meyer_strix_2018}{16}
\bibcite{jacobs_reactive_2024}{17}
\@writefile{toc}{\contentsline {section}{References}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{References}{16}{}\protected@file@percent }
\bibcite{branicky_multiple_1998}{18}
\bibcite{bansal_hamilton-jacobi_2017}{19}
\bibcite{guernic_reachability_2009}{20}
@ -68,41 +72,28 @@
\bibcite{prajna_safety_2004}{23}
\bibcite{eia_lcoe_2022}{24}
\bibcite{eesi_datacenter_2024}{25}
\@writefile{toc}{\contentsline {section}{\numberline {7}Budget and Budget Justification}{19}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Budget Summary}{19}{}\protected@file@percent }
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{19}{}\protected@file@percent }
\newlabel{tab:budget}{{1}{19}{Budget Summary}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2}Budget Justification}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.1}Senior Personnel}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Faculty Advisor}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.2}Other Personnel}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.3}Fringe Benefits}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Faculty Fringe Benefits}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.4}Equipment}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.5}Travel}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Conference Travel (\$4,000 per year)}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Industry Collaboration Visits (\$1,500 per year)}{20}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.6}Participant Support Costs}{21}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.7}Other Direct Costs}{21}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Materials and Supplies}{21}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Publication Costs}{21}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Computing and Cloud Services}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.8}H. Indirect Costs (Facilities \& Administrative)}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.9}Cost Sharing}{22}{}\protected@file@percent }
\newlabel{sec:cost-sharing}{{7.2.9}{22}{Cost Sharing}{}{}}
\@writefile{toc}{\contentsline {paragraph}{Emerson Process Management Partnership}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{University Infrastructure}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Total In-Kind Contributions}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.10}Budget Inflation and Escalation}{22}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {8}Schedule, Milestones, and Deliverables}{23}{}\protected@file@percent }
\gtt@chartextrasize{0}{164.1287pt}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{23}{}\protected@file@percent }
\newlabel{fig:gantt}{{1}{23}{Schedule, Milestones, and Deliverables}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {8.1}Milestones and Deliverables}{23}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {9}Supplemental Sections}{25}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.1}Biosketch}{25}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.2}Data Management Plan}{28}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.3}Facilities}{32}{}\protected@file@percent }
\gdef \@abspage@last{33}
\@writefile{toc}{\contentsline {section}{\numberline {8}Budget and Budget Justification}{I}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {8.1}Budget Summary}{I}{}\protected@file@percent }
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{I}{}\protected@file@percent }
\newlabel{tab:budget}{{1}{I}{Budget Summary}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {8.2}Budget Justification}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.1}Senior Personnel}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Faculty Advisor}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.2}Other Personnel}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.3}Fringe Benefits}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Faculty Fringe Benefits}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.4}Travel}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Conference Travel (\$4,000 per year)}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Industry Collaboration Visits (\$1,500 per year)}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.5}Other Direct Costs}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Materials and Supplies}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Publication Costs}{II}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{Computing and Cloud Services}{III}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.6}H. Indirect Costs (Facilities \& Administrative)}{III}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {9}Supplemental Sections}{III}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.1}Biosketch}{III}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.2}Data Management Plan}{VI}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {9.3}Facilities}{X}{}\protected@file@percent }
\gdef \@abspage@last{31}

5
Writing/ERLM/main.blg
View File

@ -11,7 +11,6 @@ Warning--entry type for "10CFR50.54" isn't style-file defined
--line 59 of file references.bib
Warning--entry type for "guernic_reachability_2009" isn't style-file defined
--line 221 of file references.bib
Warning--I didn't find a database entry for "a"
Warning--empty author in WRPS.Description
Warning--empty year in WRPS.Description
Warning--empty journal in hogberg_root_2013
@ -30,7 +29,7 @@ Warning--empty year in mitchell_time-dependent_2005
Warning--empty year in prajna_safety_2004
You've used 25 entries,
1876 wiz_defined-function locations,
609 strings with 7729 characters,
608 strings with 7728 characters,
and the built_in function-call counts, 5612 in all, are:
= -- 511
> -- 249
@ -69,4 +68,4 @@ warning$ -- 16
while$ -- 53
width$ -- 27
write$ -- 210
(There were 21 warnings)
(There were 20 warnings)

33
Writing/ERLM/main.fdb_latexmk
View File

@ -1,13 +1,13 @@
# Fdb version 4
["bibtex main"] 1764980933.98858 "main.aux" "main.bbl" "main" 1764982133.83346 0
["bibtex main"] 1764990267.80751 "main.aux" "main.bbl" "main" 1764990468.02866 0
"./references.bib" 1764980611.90841 14069 2a4f74c587187a8a71049043171eb0fe ""
"/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex"
"main.aux" 1764990467.86727 6961 b67c1d53687261878883c1352f4b1410 "pdflatex"
(generated)
"main.bbl"
"main.blg"
(rewritten before read)
["pdflatex"] 1764982132.94482 "main.tex" "main.pdf" "main" 1764982133.83364 0
["pdflatex"] 1764990467.13431 "main.tex" "main.pdf" "main" 1764990468.02883 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 ""
@ -242,23 +242,26 @@
"/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1760105440.02229 5312232 f3296911be9cc021788f3f879cf0a47d ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
"1-goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 ""
"2-state-of-the-art/v6.tex" 1764975691.95583 13373 7b26a8331e52f6fdbd3c6203283d61a8 ""
"3-research-approach/v4.tex" 1764982131.29739 17588 1f9490df80ab110e8accd0d34a67ef15 ""
"4-metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
"5-risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
"6-broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 ""
"7-budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
"8-schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d ""
"1-goals-and-outcomes/research_statement_v2.tex" 1764988975.93677 4450 070caee751214eaddffa6b3403f8ed43 ""
"1-goals-and-outcomes/v8.tex" 1764987710.74095 5825 07f6fba24cfa050a3b2b00c416f0f45f ""
"2-state-of-the-art/v7.tex" 1764987725.29096 10609 44863eb08e23052a1623ef3ebcb1e3ae ""
"3-research-approach/v5.tex" 1764987711.02695 17228 76776c8f57e50cca2efc146c8bbe301e ""
"4-metrics-of-success/v3.tex" 1764987211.44054 5586 e5fb80ced00bcdc318ffe3861b0064bc ""
"5-risks-and-contingencies/v3.tex" 1764987320.59343 10412 17e755aa8451c45198372af7afe3c500 ""
"6-broader-impacts/v3.tex" 1764987383.35954 4834 418aae223b778759691eaf9124a5360c ""
"7-budget/v2.tex" 1764989376.54455 7317 5cdea8ea5ec67b0fc00884e406429935 ""
"8-schedule/v2.tex" 1764989806.19871 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 ""
"9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
"9-supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
"9-supplemental-sections/v1.tex" 1764975820.90587 2306 2e5bf084cf72f93d80cf9138d1569d6f ""
"dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c ""
"main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex"
"main.bbl" 1764980934.02731 5012 668a266823d48f68a9ac1ddb0c83466e "bibtex main"
"main.tex" 1764979384.78263 822 20061a5e271518c18336f9c3c88b120c ""
"dane_proposal_format.cls" 1764990266.03918 2581 ff22f600587ffbc4d06e6b2a42f70c6e ""
"main.aux" 1764990467.86727 6961 b67c1d53687261878883c1352f4b1410 "pdflatex"
"main.bbl" 1764990267.84655 5012 668a266823d48f68a9ac1ddb0c83466e "bibtex main"
"main.tex" 1764990070.94187 979 6111485af35d67a2918f2bc5ac1beeb0 ""
"main.toc" 1764990467.86827 3034 1f2c010ba6afb7a4edffb1989ad7b820 "pdflatex"
(generated)
"main.aux"
"main.log"
"main.pdf"
"main.toc"
(rewritten before read)

316
Writing/ERLM/main.fls
View File

@ -260,3 +260,319 @@ INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT ./main.aux
INPUT ./main.aux
INPUT main.aux
OUTPUT main.aux
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
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
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
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/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/tfm/adobe/times/ptmr7t.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 /var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map
INPUT /usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc
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 ./1-goals-and-outcomes/research_statement_v2.tex
INPUT ./1-goals-and-outcomes/research_statement_v2.tex
INPUT 1-goals-and-outcomes/research_statement_v2.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.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/ptmri7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT ./main.toc
INPUT ./main.toc
INPUT main.toc
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
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
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/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/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/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/ptmr8c.vf
OUTPUT main.toc
INPUT ./1-goals-and-outcomes/v8.tex
INPUT ./1-goals-and-outcomes/v8.tex
INPUT ./1-goals-and-outcomes/v8.tex
INPUT ./1-goals-and-outcomes/v8.tex
INPUT 1-goals-and-outcomes/v8.tex
INPUT ./2-state-of-the-art/v7.tex
INPUT ./2-state-of-the-art/v7.tex
INPUT ./2-state-of-the-art/v7.tex
INPUT ./2-state-of-the-art/v7.tex
INPUT 2-state-of-the-art/v7.tex
INPUT ./3-research-approach/v5.tex
INPUT ./3-research-approach/v5.tex
INPUT ./3-research-approach/v5.tex
INPUT ./3-research-approach/v5.tex
INPUT 3-research-approach/v5.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 /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/public/rsfs/rsfs10.tfm
INPUT ./4-metrics-of-success/v3.tex
INPUT ./4-metrics-of-success/v3.tex
INPUT ./4-metrics-of-success/v3.tex
INPUT ./4-metrics-of-success/v3.tex
INPUT 4-metrics-of-success/v3.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm
INPUT ./5-risks-and-contingencies/v3.tex
INPUT ./5-risks-and-contingencies/v3.tex
INPUT ./5-risks-and-contingencies/v3.tex
INPUT ./5-risks-and-contingencies/v3.tex
INPUT 5-risks-and-contingencies/v3.tex
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 ./6-broader-impacts/v3.tex
INPUT ./6-broader-impacts/v3.tex
INPUT ./6-broader-impacts/v3.tex
INPUT ./6-broader-impacts/v3.tex
INPUT 6-broader-impacts/v3.tex
INPUT ./8-schedule/v2.tex
INPUT ./8-schedule/v2.tex
INPUT ./8-schedule/v2.tex
INPUT ./8-schedule/v2.tex
INPUT 8-schedule/v2.tex
INPUT ./main.bbl
INPUT ./main.bbl
INPUT main.bbl
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm
INPUT ./7-budget/v2.tex
INPUT ./7-budget/v2.tex
INPUT ./7-budget/v2.tex
INPUT ./7-budget/v2.tex
INPUT 7-budget/v2.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.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/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/adobe/times/ptmr8c.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/ptmr8c.vf
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/ptmb8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb8c.vf
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri8c.vf
INPUT ./9-supplemental-sections/v1.tex
INPUT ./9-supplemental-sections/v1.tex
INPUT ./9-supplemental-sections/v1.tex
INPUT ./9-supplemental-sections/v1.tex
INPUT 9-supplemental-sections/v1.tex
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/cv-1786798.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
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/public/amsfonts/symbols/msam10.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

555
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 19:50
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 5 DEC 2025 22:07
entering extended mode
restricted \write18 enabled.
file:line:error style messages enabled.
@ -491,4 +491,555 @@ File: tikzlibrarychains.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfdecoratedinputsegmentremainingdistance=\dimen274
\pgf@decorate@distancetomove=\dimen275
\pgf@decorate@repeatstate=\count321
\pgfdecorationsegmentamplitude=\
\pgfdecorationsegmentamplitude=\dimen276
\pgfdecorationsegmentlength=\dimen277
)
\tikz@lib@dec@box=\box86
) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex
File: tikzlibraryshadows.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex
File: tikzlibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex
File: pgflibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10)
))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
File: pgflibraryarrows.meta.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfarrowinset=\dimen278
\pgfarrowlength=\dimen279
\pgfarrowwidth=\dimen280
\pgfarrowlinewidth=\dimen281
) (/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty
Package: standalone 2022/10/10 v1.3b Package to include TeX sub-files with preambles
(/usr/share/texlive/texmf-dist/tex/latex/tools/shellesc.sty
Package: shellesc 2023/07/08 v1.0d unified shell escape interface for LaTeX
Package shellesc Info: Restricted shell escape enabled on input line 77.
) (/usr/share/texlive/texmf-dist/tex/latex/currfile/currfile.sty
Package: currfile 2022/10/10 v0.8 Provides the file path elements of the current input file
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty
Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO)
) (/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
)) (/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook.sty
Package: filehook 2022/10/25 v0.8b Hooks for input files
(/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook-2020.sty
Package: filehook-2020 2022/10/25 v0.8b Hooks for input files
))
\c@currfiledepth=\count322
) (/usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty (/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
Package: svn-prov 2010/04/24 v3.1862 Package Date/Version from SVN Keywords
)
Package: gincltex 2011/09/04 v0.3 Include external LaTeX files like graphics
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
Package: adjustbox 2022/10/17 v1.3a Adjusting TeX boxes (trim, clip, ...)
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
Package: adjcalc 2012/05/16 v1.1 Provides advanced setlength with multiple back-ends (calc, etex, pgfmath)
) (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
Package: trimclip 2020/08/19 v1.2 Trim and clip general TeX material
(/usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
Package: collectbox 2022/10/17 v0.4c Collect macro arguments as boxes
\collectedbox=\box87
)
\tc@llx=\dimen282
\tc@lly=\dimen283
\tc@urx=\dimen284
\tc@ury=\dimen285
Package trimclip Info: Using driver 'tc-pdftex.def'.
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
File: tc-pdftex.def 2019/01/04 v2.2 Clipping driver for pdftex
))
\adjbox@Width=\dimen286
\adjbox@Height=\dimen287
\adjbox@Depth=\dimen288
\adjbox@Totalheight=\dimen289
\adjbox@pwidth=\dimen290
\adjbox@pheight=\dimen291
\adjbox@pdepth=\dimen292
\adjbox@ptotalheight=\dimen293
(/usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection
\c@checkoddpage=\count323
)
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
Package: varwidth 2009/03/30 ver 0.92; Variable-width minipages
\@vwid@box=\box88
\sift@deathcycles=\count324
\@vwid@loff=\dimen294
\@vwid@roff=\dimen295
))
\gincltex@box=\box89
) (/usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
Package: filemod-expmin 2011/09/19 v1.2 Get and compare file modification times (expandable; minimal)
)) (/usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
Package: booktabs 2020/01/12 v1.61803398 Publication quality tables
\heavyrulewidth=\dimen296
\lightrulewidth=\dimen297
\cmidrulewidth=\dimen298
\belowrulesep=\dimen299
\belowbottomsep=\dimen300
\aboverulesep=\dimen301
\abovetopsep=\dimen302
\cmidrulesep=\dimen303
\cmidrulekern=\dimen304
\defaultaddspace=\dimen305
\@cmidla=\count325
\@cmidlb=\count326
\@aboverulesep=\dimen306
\@belowrulesep=\dimen307
\@thisruleclass=\count327
\@lastruleclass=\count328
\@thisrulewidth=\dimen308
) (/usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
Package: tabularx 2023/07/08 v2.11c `tabularx' package (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
Package: array 2023/10/16 v2.5g Tabular extension package (FMi)
\col@sep=\dimen309
\ar@mcellbox=\box90
\extrarowheight=\dimen310
\NC@list=\toks43
\extratabsurround=\skip57
\backup@length=\skip58
\ar@cellbox=\box91
)
\TX@col@width=\dimen311
\TX@old@table=\dimen312
\TX@old@col=\dimen313
\TX@target=\dimen314
\TX@delta=\dimen315
\TX@cols=\count329
\TX@ftn=\toks44
) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
Package: makecell 2009/08/03 V0.1e Managing of Tab Column Heads and Cells
\rotheadsize=\dimen316
\c@nlinenum=\count330
\TeXr@lab=\toks45
) (/usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
Package: dcolumn 2023/07/08 v1.06 decimal alignment package (DPC)
) (/usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
Package: multirow 2021/03/15 v2.8 Span multiple rows of a table
\multirow@colwidth=\skip59
\multirow@cntb=\count331
\multirow@dima=\skip60
\bigstrutjot=\dimen317
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
Package: lscape 2020/05/28 v3.02 Landscape Pages (DPC)
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2023/05/13 v2.17o AMS math features
\@mathmargin=\skip61
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2021/08/26 v2.01 AMS text
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen318
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names
)
\inf@bad=\count332
LaTeX Info: Redefining \frac on input line 234.
\uproot@=\count333
\leftroot@=\count334
LaTeX Info: Redefining \overline on input line 399.
LaTeX Info: Redefining \colon on input line 410.
\classnum@=\count335
\DOTSCASE@=\count336
LaTeX Info: Redefining \ldots on input line 496.
LaTeX Info: Redefining \dots on input line 499.
LaTeX Info: Redefining \cdots on input line 620.
\Mathstrutbox@=\box92
\strutbox@=\box93
LaTeX Info: Redefining \big on input line 722.
LaTeX Info: Redefining \Big on input line 723.
LaTeX Info: Redefining \bigg on input line 724.
LaTeX Info: Redefining \Bigg on input line 725.
\big@size=\dimen319
LaTeX Font Info: Redeclaring font encoding OML on input line 743.
LaTeX Font Info: Redeclaring font encoding OMS on input line 744.
\macc@depth=\count337
LaTeX Info: Redefining \bmod on input line 905.
LaTeX Info: Redefining \pmod on input line 910.
LaTeX Info: Redefining \smash on input line 940.
LaTeX Info: Redefining \relbar on input line 970.
LaTeX Info: Redefining \Relbar on input line 971.
\c@MaxMatrixCols=\count338
\dotsspace@=\muskip17
\c@parentequation=\count339
\dspbrk@lvl=\count340
\tag@help=\toks46
\row@=\count341
\column@=\count342
\maxfields@=\count343
\andhelp@=\toks47
\eqnshift@=\dimen320
\alignsep@=\dimen321
\tagshift@=\dimen322
\tagwidth@=\dimen323
\totwidth@=\dimen324
\lineht@=\dimen325
\@envbody=\toks48
\multlinegap=\skip62
\multlinetaggap=\skip63
\mathdisplay@stack=\toks49
LaTeX Info: Redefining \[ on input line 2953.
LaTeX Info: Redefining \] on input line 2954.
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\symAMSa=\mathgroup6
\symAMSb=\mathgroup7
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
Package: enumitem 2019/06/20 v3.9 Customized lists
\labelindent=\skip64
\enit@outerparindent=\dimen326
\enit@toks=\toks50
\enit@inbox=\box94
\enit@count@id=\count344
\enitdp@description=\count345
) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
\lst@mode=\count346
\lst@gtempboxa=\box95
\lst@token=\toks51
\lst@length=\count347
\lst@currlwidth=\dimen327
\lst@column=\count348
\lst@pos=\count349
\lst@lostspace=\dimen328
\lst@width=\dimen329
\lst@newlines=\count350
\lst@lineno=\count351
\lst@maxwidth=\dimen330
(/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz)
\c@lstnumber=\count352
\lst@skipnumbers=\count353
\lst@framebox=\box96
) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
File: listings.cfg 2023/02/27 1.9 listings configuration
))
Package: listings 2023/02/27 1.9 (Carsten Heinz)
(/usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
Package: pgfgantt 2018/01/10 v5.0 Draw Gantt diagrams with TikZ
(/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
File: tikzlibrarybackgrounds.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgf@layerbox@background=\box97
\pgf@layerboxsaved@background=\box98
) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
File: tikzlibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
File: pgflibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10)
)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
File: pgfcalendar.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfcalendarcurrentjulian=\count354
\pgf@cal@easter@Y=\count355
\pgf@cal@easter@G=\count356
\pgf@cal@easter@C=\count357
\pgf@cal@easter@X=\count358
\pgf@cal@easter@Z=\count359
\pgf@cal@easter@D=\count360
\pgf@cal@easter@E=\count361
\pgf@cal@easter@N=\count362
\pgf@cal@easter@M=\count363
\pgf@cal@easter@julianday=\count364
))
\gtt@currentline=\count365
\gtt@lasttitleline=\count366
\gtt@currgrid=\count367
\gtt@chartwidth=\count368
\gtt@lasttitleslot=\count369
\gtt@elementid=\count370
\gtt@today@slot=\count371
\gtt@startjulian=\count372
\gtt@endjulian=\count373
\gtt@chartid=\count374
\gtt@vrule@slot=\count375
\gtt@calendar@slots=\count376
\gtt@calendar@weeknumber=\count377
\gtt@calendar@startofweek=\count378
\gtt@left@slot=\count379
\gtt@right@slot=\count380
)
\figurewidth=\skip65
\figureheight=\skip66
\c@task=\count381
) (/usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
Package: colortbl 2022/06/20 v1.0f Color table columns (DPC)
\everycr=\toks52
\minrowclearance=\skip67
\rownum=\count382
)
LaTeX Font Info: Trying to load font information for OT1+ptm on input line 10.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-01-04 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count383
\l__pdf_internal_box=\box99
) (./main.aux)
\openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
*geometry* driver: auto-detecting
*geometry* detected driver: pdftex
*geometry* verbose mode - [ preamble ] result:
* driver: pdftex
* paper: <default>
* layout: <same size as paper>
* layoutoffset:(h,v)=(0.0pt,0.0pt)
* modes:
* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt)
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
* \paperwidth=614.295pt
* \paperheight=794.96999pt
* \textwidth=469.75502pt
* \textheight=650.43001pt
* \oddsidemargin=0.0pt
* \evensidemargin=0.0pt
* \topmargin=-37.0pt
* \headheight=12.0pt
* \headsep=25.0pt
* \topskip=12.0pt
* \footskip=30.0pt
* \marginparwidth=44.0pt
* \marginparsep=10.0pt
* \columnsep=10.0pt
* \skip\footins=10.8pt plus 4.0pt minus 2.0pt
* \hoffset=0.0pt
* \voffset=0.0pt
* \mag=1000
* \@twocolumnfalse
* \@twosidefalse
* \@mparswitchfalse
* \@reversemarginfalse
* (1in=72.27pt=25.4mm, 1cm=28.453pt)
(/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
File: fc-english.def 2016/01/12
) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count384
\scratchdimen=\dimen331
\scratchbox=\box100
\nofMPsegments=\count385
\nofMParguments=\count386
\everyMPshowfont=\toks53
\MPscratchCnt=\count387
\MPscratchDim=\dimen332
\MPnumerator=\count388
\makeMPintoPDFobject=\count389
\everyMPtoPDFconversion=\toks54
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 485.
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live
)) (/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF
(/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
Package: pdflscape-nometadata 2022-10-28 v0.13 Display of landscape pages in PDF (HO)
Package pdflscape Info: Auto-detected driver: pdftex on input line 81.
))
\c@lstlisting=\count390
LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 13.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm.
)
LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 13.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm.
)
LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 13.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm.
)
LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 13.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm.
)
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 13.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 13.
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 13.
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./1-goals-and-outcomes/research_statement_v2.tex) [1] (./main.toc
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 4.
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 4.
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 4.
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 31.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
) [2])
\tf@toc=\write4
\openout4 = `main.toc'.
[3] (./1-goals-and-outcomes/v8.tex [1]) (./2-state-of-the-art/v7.tex [2] [3] [4]) (./3-research-approach/v5.tex [5] [6] [7] [8]) (./4-metrics-of-success/v3.tex [9]) (./5-risks-and-contingencies/v3.tex [10] [11] [12]) (./6-broader-impacts/v3.tex [13]) (./8-schedule/v2.tex [14]
Missing character: There is no , in font nullfont!
) [15] (./main.bbl
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
[]
[16]) [17] (./7-budget/v2.tex
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 22.
[1] [2]) (./9-supplemental-sections/v1.tex
<9-supplemental-sections/cv-1786798.pdf, id=112, 614.295pt x 794.97pt>
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
<9-supplemental-sections/cv-1786798.pdf, id=115, page=1, 614.295pt x 794.97pt>
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[3]
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[4
<./9-supplemental-sections/cv-1786798.pdf>]
<9-supplemental-sections/cv-1786798.pdf, id=136, page=2, 614.295pt x 794.97pt>
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use 9-supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[5
<./9-supplemental-sections/cv-1786798.pdf>]
<9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=140, 614.295pt x 794.97pt>
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
<9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=143, page=1, 614.295pt x 794.97pt>
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[6]
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[7
<./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]
<9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=167, page=2, 614.295pt x 794.97pt>
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[8
<./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]
<9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=171, page=3, 614.295pt x 794.97pt>
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: 9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[9
<./9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]) [10] (./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:
26081 strings out of 476182
543588 string characters out of 5795595
1946975 words of memory out of 5000000
47491 multiletter control sequences out of 15000+600000
596976 words of font info for 119 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191
110i,17n,107p,1062b,952s 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/public/amsfonts/symbols/msam10.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 (31 pages, 257157 bytes).
PDF statistics:
224 PDF objects out of 1000 (max. 8388607)
132 compressed objects within 2 object streams
0 named destinations out of 1000 (max. 500000)
164 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
Writing/ERLM/main.pdf
View File

Binary file not shown.

0
Writing/ERLM/main.synctex(busy)
View File

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

Binary file not shown.

23
Writing/ERLM/main.tex
View File

@ -9,19 +9,26 @@
\begin{document}
\pagenumbering{roman}
\maketitle
\input{1-goals-and-outcomes/v7}
\input{2-state-of-the-art/v6}
\input{3-research-approach/v4}
\input{4-metrics-of-success/v2}
\input{5-risks-and-contingencies/v1}
\input{6-broader-impacts/v1}
\input{1-goals-and-outcomes/research_statement_v2.tex}
\newpage
\tableofcontents
\newpage
\pagenumbering{arabic}
\input{1-goals-and-outcomes/v8}
\input{2-state-of-the-art/v7}
\input{3-research-approach/v5}
\input{4-metrics-of-success/v3}
\input{5-risks-and-contingencies/v3}
\input{6-broader-impacts/v3}
\input{8-schedule/v2}
\newpage
\bibliographystyle{ieeetr}
\bibliography{references}
\newpage
\input{7-budget/v1}
\input{8-schedule/v1}
\pagenumbering{Roman}
\input{7-budget/v2}
\input{9-supplemental-sections/v1}

41
Writing/ERLM/main.toc Normal file
View File

@ -0,0 +1,41 @@
\contentsline {section}{Contents}{ii}{}%
\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}%
\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}%
\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}%
\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}%
\contentsline {section}{\numberline {3}Research Approach}{5}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{9}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{10}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{11}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{11}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{12}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{13}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{15}{}%
\contentsline {section}{References}{16}{}%
\contentsline {section}{\numberline {8}Budget and Budget Justification}{I}{}%
\contentsline {subsection}{\numberline {8.1}Budget Summary}{I}{}%
\contentsline {subsection}{\numberline {8.2}Budget Justification}{II}{}%
\contentsline {subsubsection}{\numberline {8.2.1}Senior Personnel}{II}{}%
\contentsline {paragraph}{Faculty Advisor}{II}{}%
\contentsline {subsubsection}{\numberline {8.2.2}Other Personnel}{II}{}%
\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{II}{}%
\contentsline {subsubsection}{\numberline {8.2.3}Fringe Benefits}{II}{}%
\contentsline {paragraph}{Faculty Fringe Benefits}{II}{}%
\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{II}{}%
\contentsline {subsubsection}{\numberline {8.2.4}Travel}{II}{}%
\contentsline {paragraph}{Conference Travel (\$4,000 per year)}{II}{}%
\contentsline {paragraph}{Industry Collaboration Visits (\$1,500 per year)}{II}{}%
\contentsline {subsubsection}{\numberline {8.2.5}Other Direct Costs}{II}{}%
\contentsline {paragraph}{Materials and Supplies}{II}{}%
\contentsline {paragraph}{Publication Costs}{II}{}%
\contentsline {paragraph}{Computing and Cloud Services}{III}{}%
\contentsline {subsubsection}{\numberline {8.2.6}H. Indirect Costs (Facilities \& Administrative)}{III}{}%
\contentsline {section}{\numberline {9}Supplemental Sections}{III}{}%
\contentsline {subsection}{\numberline {9.1}Biosketch}{III}{}%
\contentsline {subsection}{\numberline {9.2}Data Management Plan}{VI}{}%
\contentsline {subsection}{\numberline {9.3}Facilities}{X}{}%