Dane Sabo
2497bb4aa5
M .task/backlog.data M .task/completed.data M .task/pending.data M .task/undo.data A PLAN_OF_STUDY_111225.pdf R Writing/202510270-Emerson-Pres/SaboOneSlide.pdf -> Presentations/202510270-Emerson-Pres/SaboOneSlide.pdf R Writing/202510270-Emerson-Pres/beamerthemedane.sty -> Presentations/202510270-Emerson-Pres/beamerthemedane.sty R Writing/202510270-Emerson-Pres/beamerthemedane_native.sty -> Presentations/202510270-Emerson-Pres/beamerthemedane_native.sty
441 lines
15 KiB
Markdown
441 lines
15 KiB
Markdown
# Speaker Notes: Formally Verified Autonomous Hybrid Control
|
||
|
||
**Presentation for Engineering PhDs**
|
||
**Audience:** General engineering background, not necessarily control/nuclear/formal methods experts
|
||
|
||
---
|
||
|
||
## Slide 1: Title & Roadmap
|
||
|
||
**Central Thesis:** Formally verified autonomous hybrid control is both *necessary* and *achievable* for next-generation nuclear power.
|
||
|
||
**Roadmap Overview:**
|
||
1. **The Problem:** Economic challenge + fundamental human reliability limits
|
||
2. **The Technical Challenge:** Hybrid systems and why current methods fall short
|
||
3. **The Solution:** Three-thrust approach with formal guarantees + hardware-in-the-loop
|
||
4. **The Impact:** Beyond nuclear applications
|
||
|
||
---
|
||
|
||
## Slide 2: Economic Challenge
|
||
|
||
### Small modular reactors face an unsustainable staffing cost problem
|
||
|
||
**The Economic Reality:**
|
||
- Current requirement: 2+ Reactor Operators + 1+ Senior Reactor Operator per unit
|
||
- Training timeline: up to 6 years to become licensed reactor operator
|
||
- Small modular reactors have same staffing overhead but lower power output
|
||
- Result: Higher per-megawatt O&M costs threaten economic viability
|
||
|
||
**The Market Opportunity:**
|
||
- Datacenter demand projected: 1,050 TWh annually by 2030
|
||
- Nuclear O&M costs: 23-30% of levelized cost ($88.24/MWh)
|
||
- Annual O&M for datacenter demand alone: **$21-28 billion**
|
||
|
||
**Key message:** Automation is not optional---it's economically essential
|
||
|
||
---
|
||
|
||
## Slide 3: Safety Imperative
|
||
|
||
### Human operators are the root cause of 70-80% of nuclear incidents
|
||
|
||
**The Human Error Problem:**
|
||
- 70-80% of events attributed to human error (multiple independent analyses)
|
||
- IAEA categorical statement: "Human error was the root cause of ALL severe accidents"
|
||
- Three Mile Island, Chernobyl, Fukushima
|
||
|
||
**Three Mile Island (1979):**
|
||
- 100+ simultaneous alarms overwhelmed operators
|
||
- Operators shut down emergency cooling based on incorrect assessment
|
||
- Result: 44% of fuel melted
|
||
- Risk assessment was off by **500-fold** (5% actual vs 0.01% predicted)
|
||
|
||
**Fundamental Cognitive Limitations:**
|
||
- Working memory: 7±2 items (Miller, 1956)
|
||
- Human Error Probability degrades under stress:
|
||
- Optimal conditions: 0.001-0.01 (0.1-1%)
|
||
- Accident conditions: **0.1-1.0 (10-100%)** = essentially guaranteed failure
|
||
- **Four decades of training improvements haven't changed the 70-80% ratio**
|
||
|
||
---
|
||
|
||
## Slide 4: The Paradox
|
||
|
||
### Nuclear control faces a fundamental tension
|
||
|
||
**The Paradox:** Human operators are both essential for flexibility and the primary source of failure
|
||
|
||
**Why We Need Humans:**
|
||
- Strategic decision-making
|
||
- Procedure interpretation
|
||
- Handling novel situations
|
||
- Adaptive judgment
|
||
- Legal authority (10 CFR 55)
|
||
|
||
**Why Humans Fail:**
|
||
- Working memory: 7±2 items
|
||
- Response time: seconds vs milliseconds
|
||
- Cognitive biases (confirmation, anchoring)
|
||
- Stress degrades performance 10-50x
|
||
- Error rates: 0.001 → 1.0 under accident conditions
|
||
|
||
**Current Division of Labor:**
|
||
- **Automated:** Emergency protection (trip systems, ECCS) = terminal operations
|
||
- **Manual:** Strategic operations (startup, mode transitions, power changes) = routine operations
|
||
- **Problem:** This is backwards! We automate terminal ops but manually handle routine ops.
|
||
|
||
**Goal:** Combine the reliability of automation with the sophistication of human decision-making
|
||
|
||
---
|
||
|
||
## Slide 5: Hybrid Systems
|
||
|
||
### Hybrid systems combine continuous dynamics with discrete mode switching
|
||
|
||
**Nuclear plants are inherently hybrid systems**
|
||
|
||
**Continuous Dynamics:**
|
||
- Reactor temperature, neutron flux, pressure, flow rates, heat transfer
|
||
- Governed by differential equations: ẋ(t) = f(x(t), q(t), u(t))
|
||
|
||
**Discrete Decisions:**
|
||
- Mode transitions, control strategy changes, safety system actuation, procedure steps
|
||
- Governed by logic: q(k+1) = ν(x(k), q(k), u(k))
|
||
|
||
**Example: Reactor Startup**
|
||
- Cold Shutdown → Heatup → Approach Criticality → Low Power
|
||
- Each mode has continuous dynamics; transitions are discrete strategic decisions
|
||
- **This is exactly what human operators do today**
|
||
|
||
---
|
||
|
||
## Slide 6: Current Gaps
|
||
|
||
### Existing methods can handle either continuous or discrete, but not both
|
||
|
||
**Formal Methods (HARDENS):**
|
||
- Can verify discrete logic (requirements → verified binaries)
|
||
- Achieved in 9 months, low cost
|
||
- **BUT:** Cannot handle continuous dynamics
|
||
|
||
**Control Theory:**
|
||
- Can verify continuous stability (Lyapunov, LQR, robust control)
|
||
- **BUT:** Cannot verify discrete transitions or mode switching
|
||
|
||
**THE GAP:** Hybrid system verification with formal guarantees spanning both continuous and discrete
|
||
|
||
**HARDENS Achievement:**
|
||
- Complete RTS verification (discrete only)
|
||
- TRL 3-4, no experimental validation
|
||
- Requirements → formal specs → verified implementation
|
||
- But: No continuous dynamics, no closed-loop verification
|
||
|
||
**We need to bridge this gap.**
|
||
|
||
---
|
||
|
||
## Slide 7: Approach Overview
|
||
|
||
### Unifying discrete synthesis and continuous verification enables end-to-end guarantees
|
||
|
||
**Three-Thrust Integrated Approach:**
|
||
|
||
**Thrust 1 (Procedures → Temporal Logic):**
|
||
- Use NASA FRET to translate written procedures to formal specifications
|
||
- Example: "If high temp, insert rods until reset" becomes G(T_high → X(rods ∧ ...))
|
||
- Realizability checking catches errors in procedures *before* implementation
|
||
|
||
**Thrust 2 (Temporal Logic → Discrete Automaton):**
|
||
- Reactive synthesis generates correct-by-construction state machine
|
||
- Discrete controller is mathematically guaranteed to follow specifications
|
||
|
||
**Thrust 3 (Continuous Controllers):**
|
||
- Use reachability analysis and barrier certificates
|
||
- Compositional verification: local proofs, global guarantees
|
||
|
||
**Innovation:** Each piece uses state-of-the-art tools; innovation is in the integration
|
||
|
||
---
|
||
|
||
## Slide 8: Thrust 1 - Procedures to Logic
|
||
|
||
### NASA's FRET tool translates procedures into unambiguous logic
|
||
|
||
**The Challenge:** Natural language is ambiguous; machines need precise specifications
|
||
|
||
**Example Translation:**
|
||
- **Natural:** "If a high temperature alarm triggers, control rods must immediately insert and remain inserted until operator reset."
|
||
- **Logic:** G(HighTemp → X(RodsInserted ∧ (¬RodsWithdrawn U OpReset)))
|
||
|
||
**FRETish Structure:** 6 components eliminate ambiguity
|
||
- [Scope] [Condition] [Component] SHALL [Timing] [Response]
|
||
|
||
**Realizability Checking:** Catches errors *before* implementation
|
||
- Detects conflicting requirements
|
||
- Identifies undefined behaviors (gaps left to human judgment)
|
||
- These are "bugs in the procedures"---better to find them early!
|
||
|
||
**Output:** Unambiguous temporal logic ready for synthesis
|
||
|
||
---
|
||
|
||
## Slide 9: Thrust 2 - Reactive Synthesis
|
||
|
||
### Reactive synthesis generates provably correct discrete controllers
|
||
|
||
**What is Reactive Synthesis?**
|
||
- **Input:** Temporal logic formula (what *should* happen)
|
||
- **Output:** Finite state machine (how to *make it* happen)
|
||
- **Guarantee:** If a solution exists, it is correct by construction
|
||
|
||
**Example: Simplified Reactor Automaton**
|
||
- **Nodes** = discrete modes (what control strategy to use)
|
||
- **Edges** = transition conditions (when to switch)
|
||
- No switching errors possible---the automaton is mathematically guaranteed to satisfy specifications
|
||
|
||
**This is the "Operator's Decision-Making" Automated**
|
||
|
||
**Tool:** Strix (SYNTCOMP competition winner)
|
||
|
||
**Output:** Discrete controller with formal correctness guarantee
|
||
|
||
---
|
||
|
||
## Slide 10: Thrust 3 - Continuous Verification
|
||
|
||
### Continuous controllers verified using three complementary techniques
|
||
|
||
**Three Types of Continuous Modes:**
|
||
1. **Stabilizing:** Stay in current mode (e.g., full-power operation)
|
||
2. **Transitory:** Drive toward next mode (e.g., startup heatup)
|
||
3. **Expulsory:** Force to safe mode (e.g., SCRAM)
|
||
|
||
**Three Verification Techniques:**
|
||
|
||
1. **Reachability Analysis:**
|
||
- Compute reachable state sets
|
||
- Verify boundary conditions met
|
||
- Recent advances: Neural Hamilton-Jacobi for high dimensions
|
||
|
||
2. **Assume-Guarantee:**
|
||
- Local verification, global guarantees
|
||
- Each mode verified independently
|
||
|
||
3. **Barrier Certificates:**
|
||
- Prove safe set forward invariance
|
||
- Guarantee transitions occur correctly
|
||
|
||
**Key Innovation:** Design continuous controllers *after* synthesizing automaton
|
||
- Automaton defines transition boundaries
|
||
- Design each mode to satisfy its local transitions
|
||
- Compositional verification avoids intractable global analysis
|
||
|
||
**Output:** Verified continuous modes + discrete automaton = Complete hybrid controller
|
||
|
||
---
|
||
|
||
## Slide 11: Key Insight
|
||
|
||
### Automaton-first design makes verification tractable
|
||
|
||
**Traditional Approach (Intractable):**
|
||
- Design everything at once
|
||
- Verify entire trajectory through all modes
|
||
- Computationally intractable for complex systems
|
||
|
||
**Our Approach (Tractable):**
|
||
1. **Synthesize Discrete Automaton** (tells us what boundaries to verify)
|
||
2. **Define Transition Boundaries** (from automaton structure)
|
||
3. **Design Continuous Modes Locally** (each controller designed for its specific job)
|
||
4. **Verify Each Mode Independently** (local verification is tractable)
|
||
5. **Compose via Assume-Guarantee** (interface contracts guarantee composition)
|
||
|
||
**Key Message:** Decomposition is the key to tractable verification
|
||
|
||
---
|
||
|
||
## Slide 12: Demonstration
|
||
|
||
### SmAHTR autonomous startup provides a rigorous test case
|
||
|
||
**Small Modular Advanced High Temperature Reactor (SmAHTR):**
|
||
- Liquid-salt cooled reactor design
|
||
- Well-documented startup procedures
|
||
- Representative of next-generation SMR designs
|
||
|
||
**Startup Sequence:**
|
||
Cold → Controlled Heating → Approach Criticality → Low-Power Physics → Full Power
|
||
|
||
Each mode has different control objective:
|
||
- Temp control → Ramp rate → Reactivity → Neutron flux → Load following
|
||
|
||
**Implementation Platform:**
|
||
- **Simulation:** High-fidelity Simulink model (thermal-hydraulics + neutron kinetics)
|
||
- **Hardware:** Emerson Ovation control system (industry standard)
|
||
- **Integration:** ARCADE platform (hardware-in-the-loop)
|
||
- **Validation:** Real-time performance on actual control equipment
|
||
|
||
**Why This Matters:**
|
||
- Multiple coordinated subsystems
|
||
- Strict timing/temperature constraints
|
||
- Complex nonlinear dynamics
|
||
- **This is not a toy problem**---it's representative of deployment challenges
|
||
|
||
---
|
||
|
||
## Slide 13: Expected Outcomes
|
||
|
||
### Success measured by progression to TRL 5
|
||
|
||
**Technology Readiness Level Progression:**
|
||
- **Current:** TRL 2-3 (basic concepts, HARDENS precedent)
|
||
- **Target:** TRL 5 (validated prototype in relevant environment)
|
||
- **Gap:** Experimental validation with continuous dynamics
|
||
|
||
**Three Concrete Deliverables:**
|
||
|
||
**1. Procedure Translation Methodology**
|
||
- Engineers generate verified controllers from regulatory procedures
|
||
- No formal methods expertise required
|
||
|
||
**2. Continuous Verification Framework**
|
||
- Standard control design + iterative verification
|
||
- Mathematical proof of safe mode transitions
|
||
|
||
**3. SmAHTR Hardware-in-the-Loop Demonstration**
|
||
- Autonomous startup on industrial control hardware
|
||
- Real-time performance validation
|
||
- Clear path to deployment
|
||
|
||
**Key Message:** TRL 5 proves both theoretical validity and practical implementability
|
||
|
||
---
|
||
|
||
## Slide 14: Broader Impact
|
||
|
||
### This methodology generalizes to any safety-critical hybrid system
|
||
|
||
**Common Pattern Across Domains:**
|
||
- Written procedures exist
|
||
- Continuous dynamics + discrete decisions
|
||
- Safety is paramount
|
||
- Autonomy has economic benefits
|
||
|
||
**Application Domains:**
|
||
- **Chemical Process:** Batch processes, safety interlocks
|
||
- **Aerospace:** Flight phases, emergency procedures
|
||
- **Autonomous Transport:** Driving modes, emergency maneuvers
|
||
- **Medical Devices:** Therapy modes, patient monitoring
|
||
- **Power Grid:** Generation modes, fault response
|
||
|
||
**Economic Multiplier:**
|
||
- Nuclear O&M (datacenter demand): $21-28B annually
|
||
- Broader safety-critical infrastructure: **Much larger**
|
||
|
||
**Regulatory Pathway:**
|
||
- Proving concept in nuclear (highest safety bar)
|
||
- Establishes precedent: mathematical proof as regulatory evidence
|
||
- Easier adoption in other industries
|
||
|
||
**Key Message:** Nuclear is the proving ground; impact extends far beyond
|
||
|
||
---
|
||
|
||
## Slide 15: Innovation Summary
|
||
|
||
### The innovation is systematic integration to bridge a fundamental gap
|
||
|
||
**What's NOT New (but state-of-the-art):**
|
||
- Temporal logic
|
||
- Reactive synthesis
|
||
- Reachability analysis
|
||
- Barrier certificates
|
||
- Hardware-in-the-loop
|
||
|
||
These are mature techniques from computer science and control theory.
|
||
|
||
**What IS New:**
|
||
- **Integration:** Unifying discrete and continuous verification
|
||
- **Methodology:** Systematic tool-supported workflow
|
||
- **Decomposition:** Automaton-first design enables tractable verification
|
||
- **Practical:** Targets existing industrial hardware
|
||
|
||
**Comparison to HARDENS:**
|
||
| Feature | HARDENS (2022) | This Work |
|
||
|---------|----------------|-----------|
|
||
| Discrete verification | ✓ | ✓ |
|
||
| Continuous verification | ✗ | ✓ |
|
||
| Hybrid system verification | ✗ | ✓ |
|
||
| Experimental validation | TRL 3-4 | TRL 5 |
|
||
| Hardware-in-the-loop | ✗ | ✓ |
|
||
|
||
**Key Enabling Insight:**
|
||
Automaton-first design makes continuous verification tractable by decomposing the problem into local verifications with compositional guarantees
|
||
|
||
---
|
||
|
||
## Slide 16: Conclusion
|
||
|
||
### Formally verified autonomous hybrid control: necessary, achievable, timely
|
||
|
||
**Three Converging Imperatives:**
|
||
|
||
**1. Economic:** SMRs need autonomy to be viable
|
||
- $21-28B annual O&M for datacenter demand alone
|
||
- Per-megawatt staffing costs threaten SMR economics
|
||
|
||
**2. Safety:** Human error causes 70-80% of incidents
|
||
- Training can't overcome fundamental cognitive limits
|
||
- Error probability: 0.001 → 1.0 under accident conditions
|
||
|
||
**3. Technical:** Tools now exist to verify hybrid systems
|
||
- HARDENS proved discrete verification is feasible
|
||
- Control theory provides continuous verification tools
|
||
- **We can now bridge the gap**
|
||
|
||
**This Research Closes the Gap:**
|
||
HARDENS (Discrete) + Continuous Verification = Complete Hybrid System
|
||
|
||
**Vision:** Control engineers generate high-assurance autonomous controllers from procedures.
|
||
- No formal methods PhD required
|
||
- Mathematical proof included
|
||
- Deployable on existing industrial hardware
|
||
|
||
---
|
||
|
||
## Slide 17: Questions
|
||
|
||
**Contact Information:**
|
||
- Dane A. Sabo: dane.sabo@pitt.edu
|
||
- Dr. Dan G. Cole: dgcole@pitt.edu
|
||
- University of Pittsburgh, Cyber Energy Center
|
||
|
||
---
|
||
|
||
## Key Talking Points to Remember
|
||
|
||
### Opening (Slides 1-4)
|
||
- Hook with economics: $21-28B annual market
|
||
- Pivot to safety: 70-80% human error is a fundamental problem
|
||
- The paradox: We need human sophistication but can't tolerate human unreliability
|
||
|
||
### Technical Middle (Slides 5-11)
|
||
- Hybrid systems are how nuclear plants actually operate
|
||
- Current tools only handle half the problem
|
||
- Our innovation: integration of existing tools with automaton-first decomposition
|
||
- Emphasize "correct by construction" throughout
|
||
|
||
### Demonstration & Impact (Slides 12-16)
|
||
- SmAHTR is real, not toy problem
|
||
- TRL 5 means practical feasibility, not just theory
|
||
- Nuclear is proving ground, but impact is much broader
|
||
- Now is the right time: economics + safety + technical maturity converge
|
||
|
||
### Anticipate Questions
|
||
- **"Why not just train operators better?"** → 40 years of improvements haven't changed 70-80% ratio; cognitive limits are fundamental
|
||
- **"How does this compare to ML/AI approaches?"** → We provide mathematical proofs, not statistical confidence
|
||
- **"What about edge cases?"** → That's the point! Realizability checking finds specification gaps; formal verification proves all cases
|
||
- **"Timeline?"** → HARDENS did discrete in 9 months; we're building on that foundation
|
||
- **"Why nuclear first?"** → Highest safety bar + best documented procedures + huge economic driver
|