diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index cd9c1b8..9664b3e 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -3,21 +3,21 @@ This research develops a methodology for creating autonomous control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Extensively trained operators manage nuclear reactor control by following detailed written procedures. Plant conditions guide these operators when they switch between control objectives. +Extensively trained operators manage nuclear reactor control by following detailed written procedures. When operators switch between control objectives, plant conditions guide their decisions. % Gap -Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs exceed those of conventional plants significantly. Without autonomous control, this economic constraint threatens their viability. Autonomous control systems must therefore manage complex operational sequences safely—without constant supervision—while providing assurance equal to or better than human-operated systems. +Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants. This economic constraint threatens their viability. Autonomous control systems must therefore manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems. % APPROACH PARAGRAPH Solution We combine formal methods from computer science with control theory to build hybrid control systems correct by construction. % Rationale -Hybrid systems mirror operator behavior: discrete +Hybrid systems mirror how operators work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but cannot handle continuous dynamics during transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. % Hypothesis and Technical Approach -A three-stage methodology bridges this gap. First, we translate written +Our three-stage methodology bridges this gap. First, we translate written operating procedures into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements into scope, condition, component, timing, and response elements. Realizability diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index cbfe5a8..4d7c5d4 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -11,7 +11,7 @@ or radiological release. % Known information Nuclear plant operations rely on extensively trained human operators who follow detailed written procedures and strict regulatory requirements to -manage reactor control. Plant conditions and procedural guidance inform these operators when they switch between different control modes. +manage reactor control. When operators switch between different control modes, plant conditions and procedural guidance inform their decisions. % Gap This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. @@ -34,9 +34,9 @@ and continuous verification prevents end-to-end correctness guarantees. Our approach closes this gap by synthesizing discrete mode transitions directly from written operating procedures and verifying continuous behavior between transitions. We formalize existing procedures into logical -specifications and verify continuous dynamics against transition requirements. Autonomous controllers provably free from design -defects result from this approach. This work is conducted within the University of Pittsburgh Cyber Energy Center, -which provides access to industry collaboration and Emerson control hardware. Developed solutions therefore align with practical implementation +specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers provably free from design +defects. We conduct this work within the University of Pittsburgh Cyber Energy Center, +which provides access to industry collaboration and Emerson control hardware. Solutions developed here therefore align with practical implementation requirements. % OUTCOMES PARAGRAPHS @@ -106,4 +106,4 @@ costs through increased autonomy. This research provides the tools to achieve that autonomy while maintaining the exceptional safety record the nuclear industry requires. -The following sections detail this methodology: Section 2 examines the state of the art and identifies the verification gap this work addresses. Section 3 presents our hybrid control synthesis approach and establishes what is new and why it will succeed. Section 4 defines Technology Readiness Level advancement as the success metric. Section 5 analyzes risks and contingencies. Section 6 discusses broader impacts and answers who cares and why now. Section 7 provides the research schedule. +The following sections answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now: the economic imperative driving autonomous nuclear control. Section 7 provides the research schedule and deliverables. diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 765e1cc..79723be 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,11 +1,11 @@ \section{State of the Art and Limits of Current Practice} -This research creates tractable safe autonomous reactor control systems. Understanding what we automate requires understanding how nuclear reactors operate today. This section examines reactor operators and their operating procedures, investigates the limitations of human-based operation, and reviews current formal methods approaches to reactor control systems. +\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. We examine reactor operators and their operating procedures, investigate the fundamental limitations of human-based operation, and review formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap our work addresses. \subsection{Current Reactor Procedures and Operation} Nuclear plant procedures form a hierarchy: normal operating procedures govern routine operations, abnormal operating procedures handle off-normal conditions, Emergency Operating Procedures (EOPs) manage design-basis accidents, Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 -provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Expert judgment and simulator validation—not formal verification—drive their development. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. This rigor, however, cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. +provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Their development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. This rigor, however, cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete 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 @@ -37,7 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation. \subsection{Human Factors in Nuclear Accidents} -The previous subsection established that procedures lack formal verification despite rigorous development. Human operators execute these procedures to control nuclear plants—a human-centered approach that defines current practice. This subsection examines why reliance on human operators poses fundamental limitations. +The previous subsection established that procedures lack formal verification despite rigorous development. This subsection examines the second pillar of current practice: the human operators who execute these procedures. While procedures define what to do, human operators determine when and how to apply them—an approach that introduces fundamental reliability limitations. Current-generation nuclear power plants employ over 3,600 active NRC-licensed reactor operators in the United States~\cite{operator_statistics}. These @@ -48,9 +48,8 @@ and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor operator requires several years of training. Human error persistently contributes to nuclear safety incidents despite decades -of improvements in training and procedures. This persistence provides compelling -motivation for formal automated control with mathematical safety guarantees. -Operators hold legal authority under 10 CFR Part 55 to make critical decisions, +of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees. +Under 10 CFR Part 55, operators hold legal authority to make critical decisions, including departing from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design deficiencies, and component failures combined to cause partial meltdown. Operators @@ -81,7 +80,7 @@ limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -Human factors impose fundamental reliability limits that training alone cannot overcome. Formal methods offer an alternative: mathematical guarantees of correctness that human-centered approaches cannot achieve. This subsection examines recent formal methods work in nuclear control and identifies limitations for autonomous hybrid systems. +The previous two subsections identified the limits of current practice: procedures lack formal verification and human operators introduce persistent reliability issues. Formal methods offer an alternative path: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems. \subsubsection{HARDENS} @@ -187,8 +186,8 @@ design loop for complex systems like nuclear reactor startup procedures. \subsection{Summary: The Verification Gap} -\textbf{What is the state of the art?} Current practice reveals a fundamental gap. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. +\textbf{What is the state of the art?} Current practice reveals a fundamental gap between capability and need. Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and does not scale to system synthesis. -HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. +\textbf{The gap our work addresses:} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid verification—prevents autonomous nuclear control with end-to-end correctness guarantees. Closing this gap enables autonomous control that addresses the economic constraints threatening small modular reactor viability while maintaining the safety assurance the nuclear industry requires. -\textbf{The gap our work addresses:} This gap—between discrete-only formal methods and post-hoc hybrid verification—defines our challenge and motivates our approach. Closing it enables autonomous nuclear control with mathematical safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. The next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed. +The next section presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index a30649f..9322ea2 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,9 +15,9 @@ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Extensive simulation trials validate continuous controllers. Simulated control room testing and human factors research evaluate discrete switching logic. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification and formalizing reactor operations using hybrid automata. +Previous approaches to autonomous control verified discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees of control system behavior. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification and formalizing reactor operations using hybrid automata. -Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—fail to handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode. +Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Within each mode, continuous controllers govern plant behavior. Building a high-assurance hybrid autonomous control system (HAHACS) requires establishing a mathematical description of the system. This work draws on @@ -52,9 +52,9 @@ where: Creating a HAHACS requires constructing such a tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior. -\textbf{What is new?} Each component's infrastructure has matured, but no existing work composes them for end-to-end hybrid system verification. Our novelty lies in the architecture connecting discrete synthesis with continuous verification through well-defined interfaces—specifically, mode-level verification that avoids global hybrid system analysis. +\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three specific innovations: (1) using discrete synthesis to define entry/exit/safety contracts that bound continuous verification, (2) classifying continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, and (3) leveraging existing procedural structure to avoid global hybrid system analysis entirely. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation. -\textbf{Why will it succeed?} Three factors ensure success. First, defining entry, exit, and safety conditions at the discrete level transforms the intractable problem of global hybrid verification into tractable local verification problems with clear interfaces. Second, verification operates per mode rather than on the full hybrid system, keeping analysis tractable even for complex reactor operations. Third—and critically—nuclear procedures already define discrete boundaries between operating regimes. This existing structure provides the natural decomposition our methodology requires. The approach becomes practical for real systems as a result. +\textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than imposing artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable. Each mode is verified against local contracts, keeping computational complexity bounded. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We are not proving feasibility in principle—we are demonstrating it on production control systems with realistic reactor models. \begin{figure} \centering @@ -120,7 +120,7 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac \subsection{System Requirements, Specifications, and Discrete Controllers} -The preceding section established the mathematical framework for hybrid systems. With this formalism in hand, we now construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism. +The preceding section established the mathematical framework for hybrid systems: the eight-tuple definition that formalizes discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control is high-level and @@ -317,15 +317,11 @@ according to operating procedures. \subsection{Continuous Control Modes} -Synthesis guarantees the discrete controller is provably correct—but hybrid control requires more than discrete correctness. The continuous dynamics executing within each discrete mode must also be verified. +The previous subsection showed how to synthesize a provably correct discrete controller from operating procedures using reactive synthesis. This discrete controller determines when to switch between modes—but hybrid control requires more than discrete correctness. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly. -The discrete operational controller represents only half of an -autonomous controller, despite its provable correctness. Hybrid control systems require both discrete and -continuous components. This subsection describes the continuous control modes that -execute within each discrete state and explains how we verify they satisfy the -requirements imposed by the discrete layer. +This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. Three mode types—transitory, stabilizing, and expulsory—require different verification approaches. -This methodology's scope regarding continuous controller design requires clarification. This work verifies continuous controllers—it does not synthesize them. The distinction parallels model checking in software verification: model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We make a similar assumption—continuous controllers can be designed using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. +This methodology's scope regarding continuous controller design requires clarification. This work verifies continuous controllers—it does not synthesize them. The distinction parallels model checking in software verification: model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We make a similar assumption: continuous controllers can be designed using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. The operational control scope defines go/no-go decisions that determine what kind of continuous control to implement. The entry or exit conditions of a @@ -547,8 +543,7 @@ safety margins will matter more than performance during emergency shutdown. \subsection{Industrial Implementation} -The methodology described above must be validated on realistic -systems using industrial-grade hardware to demonstrate practical feasibility. +The previous subsections established the complete methodology: procedure formalization, discrete synthesis, and continuous verification across three mode types. This methodology must now be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility and advance from analytical concepts (TRL 2-3) to laboratory demonstration (TRL 5). This research will leverage the University of Pittsburgh Cyber Energy Center's partnership with Emerson to implement and test the HAHACS methodology on production control equipment. Emerson's Ovation distributed control system is widely deployed @@ -578,7 +573,7 @@ of transferring technology directly to industry with a direct collaboration in this research, while getting an excellent perspective of how our research outcomes can align best with customer needs. -This methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—establishes the complete research approach. The next section defines how we measure success through Technology Readiness Level advancement. +This methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—establishes the complete research approach. We have shown what is new (compositional hybrid verification integrated into the design process) and why it will succeed (leveraging existing procedural structure, mode-level analysis, and industrial collaboration). The next section defines how we measure success: not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability. %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index 8576776..8949b9b 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -87,6 +87,6 @@ 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. +controllers implementable with current technology. -While TRL advancement provides clear success criteria, several risks could prevent achieving these milestones. The next section analyzes these risks and establishes contingency plans. +TRL advancement provides clear success criteria, but reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels. The next section identifies the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index afb0485..59f0ff6 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -5,10 +5,10 @@ scope adjustment or methodological revision. Four primary risks could prevent successful completion: 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 +challenges. Each risk has associated early warning indicators 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 identifies remaining barriers to deployment clearly. +publishable results while clearly identifying remaining barriers to deployment. \subsection{Computational Tractability of Synthesis} @@ -33,15 +33,8 @@ 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. +If computational tractability becomes the limiting factor, we reduce scope to a +minimal viable startup sequence covering only cold shutdown to criticality to low-power hold, omitting power ascension and other operational phases. This reduced sequence still demonstrates the complete methodology—procedure formalization, discrete synthesis, continuous verification, and hardware implementation—while reducing computational burden. The research contribution remains valid: we prove that formal hybrid control synthesis is achievable for safety-critical nuclear applications and clearly identify which operational complexities exceed current computational capabilities. We document the limitation as a scaling constraint requiring future work, not a methodological failure. \subsection{Discrete-Continuous Interface Formalization} diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index b387880..83715a7 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -28,10 +28,8 @@ to \$21--28 billion annually for projected datacenter demand. control, making small modular reactors economically viable for datacenter power. 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 +reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making the per-megawatt cost prohibitive. These staffing requirements drive the economic challenge +that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal specifications automates routine operational sequences that currently require constant human oversight. A fundamental shift from direct operator control to supervisory monitoring becomes possible, where operators oversee multiple autonomous @@ -75,4 +73,6 @@ establish both the technical feasibility and regulatory pathway for broader adoption across critical infrastructure. -The broader impacts establish why this work matters beyond nuclear power. The next section presents the timeline for achieving these outcomes through a structured research plan. +These broader impacts answer the final Heilmeier questions: Who cares? The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control. Why now? AI infrastructure demands have made nuclear economics urgent, and formal methods tools have matured to the point where compositional hybrid verification is achievable. What difference will it make? Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems. + +The next section presents the timeline for achieving these outcomes through a structured 24-month research plan.