M .task/backlog.data M .task/pending.data M .task/undo.data A Writing/ERLM/SaboRisksAndContingencies.pdf M Writing/ERLM/broader-impacts/v1.tex M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls
75 lines
4.8 KiB
TeX
75 lines
4.8 KiB
TeX
\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, the economics
|
|
of nuclear power deployment 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 implementations of 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. By synthesizing provably correct hybrid
|
|
controllers from formal specifications, we 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 can 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. By 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—such as 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
|
|
is already complete 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. By demonstrating this approach in
|
|
nuclear power—one of the most regulated and safety-critical domains—this
|
|
research will establish both the technical feasibility and regulatory pathway
|
|
for broader adoption across critical infrastructure.
|