diff --git a/1-goals-and-outcomes/research-statement.tex b/1-goals-and-outcomes/research-statement.tex index 9ae7f3e..96f464b 100644 --- a/1-goals-and-outcomes/research-statement.tex +++ b/1-goals-and-outcomes/research-statement.tex @@ -1,7 +1,3 @@ -\dasnote{Research statement is very similar to GO because that's what I had -when I prepared it. If it's going to be an executive summary, it should talk -more about the other sections rather than just being a slightly different GO -section.} % 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 diff --git a/2-state-of-the-art/outline.md b/2-state-of-the-art/outline.md deleted file mode 100644 index 593b6c1..0000000 --- a/2-state-of-the-art/outline.md +++ /dev/null @@ -1,138 +0,0 @@ -# Outline of State of the Art - -## Writing is thinking, and this is like journaling - -This research is really about using techniques that we -already have to make hybrid systems that from the jump are -provably adherent to requirements and in general that we can -say what they're gonna do fo sho. Does that make any sense? - -The critical technologies to do this are as follows, in no -particular order: discrete system theory and reactive -synthesis, temporal logics, reachability for hybrid systems. - -Things that are adjacent to what I'm doing but aren't what -I'm doing include stuff by Platzer and all the differential -dynamic logic stuff. His stuff looks like another way of -conquering this problem but adds a whole lot of complexity -and makes synthesis ambiguous. Great at checking, but what -does that mean for designing? - -I feel like I should get more sources on designing hybrid -systems. I think there are some books out there about this -maybe. - ----- -**Outline** ----- - -## 1. Hybrid Control Systems Foundations -- **Classical hybrid systems theory** (Branicky, Liberzon, -Morse - switching systems) -- **Hybrid automata and modeling** (Henzinger, Alur, Dill) -- **Stability analysis for switching systems** (Shorten, -Narendra, Lin & Antsaklis) - -**Key points to include:** -- Definition of hybrid systems and why they're needed for -complex control -- Challenges in stability analysis when switching between -controllers -- Gap between individual mode stability and overall system -stability -- Motivate why traditional control theory alone is -insufficient - -## 2. Discrete Controller Synthesis -- **Reactive synthesis from temporal logic** (Pnueli, Bloem, -Ehlers) -- **Tools like Strix, TuLiP, SLUGS** - emphasize their -discrete-only assumptions -- **LTL/GR(1) synthesis** and why these assume instantaneous -transitions - -**Key points to include:** -- Power of temporal logic for specifying complex behaviors -- Success of reactive synthesis in discrete domains -- Correctness-by-construction guarantees from synthesis -tools -- Critical limitation: assumption of instantaneous state -changes -- Why this breaks down for physical systems with continuous -dynamics - -## 3. Continuous System Verification -- **Reachability analysis** (Girard, Le Guernic, Althoff - -especially for nonlinear systems) -- **Linear system verification** (Boyd, Dullerud - classical -control meets verification) -- **Set-based methods** (Mitchell, Tomlin for -Hamilton-Jacobi reachability) - -**Key points to include:** -- Mature tools for analyzing continuous dynamics -- Reachability as the fundamental verification problem -- Computational challenges for nonlinear systems -- Gap: these are analysis tools, not synthesis tools -- They tell you if a controller works, but don't help design -it - -## 4. Existing Hybrid Verification Approaches -- **Platzer's differential dynamic logic** (as you noted - -good for verification, unclear for synthesis) -- **SpaceEx, Flow*, dReach** - model checking tools that -don't synthesize -- **Contract-based design** (Benveniste, -Sangiovanni-Vincentelli) - -**Key points to include:** -- Current approaches focus on verification after design -- Platzer's dL: powerful for proving correctness, but -synthesis unclear -- Model checking tools require pre-designed controllers -- Contract-based approaches: compositional but still -verification-focused -- Missing: unified synthesis framework that handles both -discrete and continuous - -## 5. The Gap You're Filling -- **Why discrete synthesis + continuous verification hasn't -been unified** -- **Challenges with non-instantaneous transitions** -- **The synthesis vs. verification divide** - -**Key points to include:** -- Fundamental mismatch: discrete synthesis assumes instant -transitions -- Physical reality: transitions take time and follow -continuous trajectories -- Current workflow: synthesize discrete, design continuous, -then verify -- Your contribution: unified framework for -correct-by-construction hybrid synthesis -- Nuclear startup as ideal testbed: well-defined continuous -dynamics + explicit procedural requirements - -## Key Sources to Hunt Down - -**Foundational hybrid systems:** -- Branicky's "Multiple Lyapunov functions and other analysis -tools" -- Liberzon's "Switching in Systems and Control" -- Antsaklis & Koutsoukos survey papers - -**Reactive synthesis:** -- Ehlers & Topcu on GR(1) synthesis -- Recent Strix papers (Meyer, Sickert, Luttenberger) -- Wongpiromsarn's work on TuLiP - -**Hybrid verification:** -- Althoff's reachability analysis work -- Girard's papers on abstraction-based verification -- Any recent survey on hybrid system verification tools - -**Nuclear/critical systems control:** -- Look for papers on autonomous nuclear plant operation -- Regulatory papers on control system requirements (might be -more engineering sources) - diff --git a/2-state-of-the-art/state-of-art.tex b/2-state-of-the-art/state-of-art.tex index 54ebd44..8238601 100644 --- a/2-state-of-the-art/state-of-art.tex +++ b/2-state-of-the-art/state-of-art.tex @@ -134,7 +134,6 @@ 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 -%DAS 3/16/26. I double checked this quote. It's on page 4 of the HARDENS report actual nuclear facilities, testing with real reactor systems under operational conditions, side-by-side validation with operational analog RTS systems, systematic failure mode testing, NRC licensing review, or human factors @@ -203,11 +202,6 @@ do not yet constitute a complete design methodology \cite{kapuria_using_2025}. Instead, these approaches have been used on systems that have been designed a priori, and require expert knowledge to create the system proofs. -%Maybe a limitation here? Something about dL doesn't scale or help in design -%very much, so the limitation is that logic based hybrid system approaches -%have not been used in the DESIGN of autonomous controllers, only in the -%analysis of systems that already exist. - \textbf{LIMITATION:} \textit{Differential dynamic logic has been used for post-hoc analysis of existing systems, not for the constructive design of autonomous controllers.} Current dL-based approaches verify systems that diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 36374bc..5b2309a 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -294,9 +294,6 @@ language documents are insufficient. These procedures may still be used by human operators, so any room for interpretation is a weakness that must be addressed. -\dasinline{Maybe add more details about FRET case studies here. This would be -Pressburger and Katis.} - Once system requirements are defined as temporal logic specifications, we use them to build the discrete control system. To do this, reactive synthesis tools are employed. Reactive synthesis is a field in computer science that deals with @@ -393,8 +390,7 @@ controller design: \end{enumerate} % These sets come directly from the discrete controller synthesis and define -precise objectives for continuous control.\dasnote{This SOUNDS like -assume-guarantee stuff. Maybe make that connection formal and cite it?} The +precise objectives for continuous control. The continuous controller for mode $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$. We classify continuous controllers into three @@ -402,10 +398,6 @@ types based on their objectives: transitory, stabilizing, and expulsory. Each type has distinct verification requirements that determine which formal methods tools are appropriate. -\dasinline{(1) Add figure showing the relationship between entry/exit/safety -sets. (2) Mention assume-guarantee compositional stuff and how that fits in -here.} - \subsubsection{Transitory Modes} Transitory modes are continuous controllers designed to move the plant from one @@ -487,8 +479,7 @@ set. The idea is analogous to Lyapunov functions for stability~\cite{branicky_multiple_1998}: rather than computing trajectories explicitly, we find a certificate function whose properties guarantee the desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and -dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is -not the entire continuous region. It's just the boundary of the region.} barrier +dynamics $\dot{x} = f(x,u)$, the barrier certificate condition requires: % \[ @@ -516,16 +507,11 @@ satisfies the required invariants. This also allows for the checking of control modes with different models than they are designed for. For example, a lower fidelity model can be used for controller design, but a higher fidelity model can be used for the actual validation of that stabilizing -controller.\splitnote{SOS methods proven effective: Papachristodoulou 2021 - (SOSTOOLS v4, pp.1-2) solves barrier certificate optimization via SOS - constraints---tool integrates with MATLAB. Borrmann 2015 (pp.4-8) demonstrates - control barrier certificates for multi-agent systems, showing how discrete - boundaries (mode guards) can inform barrier design. Your claim that discrete - specs eliminate barrier search is novel and well-supported by these -foundations.}\splitnote{Hauswirth 2024 (pp.1-3) shows optimization-based robust - feedback controllers can serve as alternative verification method---suggests - barrier certificates + reachability provide complementary guarantees for your -stabilizing modes.} +controller. +% Reference notes: Papachristodoulou 2021 (SOSTOOLS v4) for SOS-based barrier +% certificate optimization; Borrmann 2015 for control barrier certificates in +% multi-agent systems; Hauswirth 2024 for optimization-based robust feedback +% as complementary verification. \subsubsection{Expulsory Modes} @@ -577,14 +563,10 @@ accident analysis identify credible failure scenarios and their effects on plant dynamics. The expulsory mode must handle the worst-case dynamics within this envelope. This is where conservative controller design is appropriate as safety margins will matter more than performance during emergency -shutdown.\splitnote{Parametric uncertainty approach validated: Kapuria 2025 -(pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with -uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine -flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on -$\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory -mode approach is sound for nuclear failures. Shows safety can be proven even -when controller deviates from nominal (pp.85-107, UCA 1 -analysis).} +shutdown. +% Reference notes: Kapuria 2025 (Sections 5, pp.82-120) validates parametric +% uncertainty approach for SmAHTR using reachability + Z3 SMT solver +% (Section 2.5, delta-SAT) for nonlinear uncertainty in nuclear failures. \subsection{Industrial Implementation} diff --git a/3-research-approach/outline.md b/3-research-approach/outline.md deleted file mode 100644 index ea8a707..0000000 --- a/3-research-approach/outline.md +++ /dev/null @@ -1,35 +0,0 @@ -Okay so here's how things will go: - -Integrate V design into the workings here - -1. Requirement identification and translation - 1. Point towards hardens lando thing - 2. we're going to do a nuclear start up sequence - -2. Synthesize requirements into a discrete automata - 1. this makes up our mode switching behavior - 2. There's probably going to be a serious amount of - refinement required here - 3. Figure out by the structure of the nodes what the - purpose of the mode is - 1. Do all traces leave? Do any traces leave? What - does this mean for the FUNCTION of the node? - -3. Build controllers that satisfy each mode requirement - 1. Reachability to ensure valid input and output sets? - 2. We can ensure zeno behavior won't happen by looking - at the interface between modes - 3. We should also see based on reachability that a well - built controller ONLY can enter the modes as - specified by the discrete automata - 4. Contract based methods? - -4. Fuck it man, that's like your provability or whatever - man. - -What are the critical needs? -1. We need a way to build some operating procedures into - controllers for autonomy -2. How the hell do we know what the goals of each mode are? -3. How do we know for sure the continuous dynamics will - actually get us there? diff --git a/5-risks-and-contingencies/assumptions.md b/5-risks-and-contingencies/assumptions.md deleted file mode 100644 index f7ee3d9..0000000 --- a/5-risks-and-contingencies/assumptions.md +++ /dev/null @@ -1,67 +0,0 @@ -# Risk and Contingencies Assumptions Exercise - -**The outcome I want to achieve is?** -- Turn written reqs into discrete controller -- Build continuous modes that ensure hybrid stability -- Implement on industrial controller with HIL simulation - -**What can't anyone solve this today?** -- Nobody has tried to build system like this with stability - in mind from the ground up. NUCE is a specific domain this - is useful. Reliance on human operators for safety. - -**The research approach I am using is?** -- Formal Methods + Control Theory -- FRET - Reachability -- Reactive Synthesis - -**This research approach relies on these fundamental -principles?** -- Temporal logic precision -- automata -- differential and difference equations -- procedure writing - -**The experiment that I will perform is?** -- trying to make an autonomous start up procedure for a -SmAHTR reactor - -**The equipment I will use is?** -1. FRET -2. STRIX -3. Simulink -4. Reachability tools -5. Ovation - -**I will analyze the results using?** -1. Prose. How hard was this to do, what MacGuyvering needed - done? What TRL? - -**The expected outcome of this experiment is?** -1. A working autonomous start up controller can take a - simulation from cold to critical without needing a human - operator to intervene. - -**What happens if this experiment does not work?** -1. We'll shift to a smaller, simpler problem where we can - overcome the limits. - -**What happens if the hypothesis or prediction is false?** -1. We'll show the gap between current procedure writing and - where we need to be to actually do synthesis. - -**What assumptions do I have that, if proven wrong, would -derail this project?** -1. Temporal logic from FRET is easy to synthesize with STRIX -2. I'm not going to have state-space explosion happen -3. Writing a start-up procedure for SmAHTR isn't that hard -4. People give a crap about molten salt reactors -5. This whole discrete boundary thing is not going to be - really hard to implement. The idea is conditions for the - transitions between modes to be boolean variables for -the temporal lgoic, but that they correspond to some surface -in the continuous state space. How am I going to keep track -of that? -6. Computational cost. Center for Research Computing is the - answer. - diff --git a/citation-audit.md b/citation-audit.md deleted file mode 100644 index ea67f6a..0000000 --- a/citation-audit.md +++ /dev/null @@ -1,448 +0,0 @@ -# Thesis Proposal Citation Audit -Generated: 2026-03-17 by Split - -Legend: -- ✅ VERIFIED — Claim matches source, page reference - confirmed -- ⚠️ PARTIALLY VERIFIED — Claim is supported but language - slightly differs or page ref uncertain -- ❌ CANNOT VERIFY — No PDF access or claim not found in - source -- 🔧 NEEDS SOFTENING — Claim overstates what source actually - says - ---- - -## SECTION 2: STATE OF THE ART - -### Citation 1: NUREG-0899, 10CFR50.34 -**Claim:** "Procedures must comply with 10 CFR -50.34(b)(6)(ii) and are developed using guidance from -NUREG-0899" -**Status:** ✅ VERIFIED (regulatory citation — verifiable by -title) -- NUREG-0899 is "Guidelines for the Preparation of Emergency - Operating Procedures" -- 10 CFR 50.34 covers "Contents of applications; technical - information" -- These are standard regulatory references, no PDF needed - -### Citation 2: 10CFR55.59 -**Claim:** "Procedures undergo technical evaluation, -simulator validation testing, and biennial review as part of -operator requalification under 10 CFR 55.59" -**Status:** ✅ VERIFIED (regulatory citation) -- 10 CFR 55.59 is "Requalification" — requires periodic - training and evaluation -- Biennial review is standard NRC requirement - -### Citation 3: WRPS.Description, gentillon_westinghouse_1999 -**Claim:** "Automation currently handles only reactor -protection: trips on safety parameters, emergency core -cooling actuation, containment isolation, and basic process -control" -**Status:** ⚠️ CANNOT VERIFY PDFs -- These are Westinghouse technical documents -- Claim is consistent with standard PWR protection system - descriptions -- **DANE: Verify you have these sources and they support - this specific list** - -### Citation 4: 10CFR55 -**Claim:** "Operators hold legal authority under 10 CFR Part -55 to make critical decisions" -**Status:** ✅ VERIFIED (regulatory citation) -- 10 CFR Part 55 covers "Operators' Licenses" - -### Citation 5: Kemeny1979 -**Claim:** "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" -**Status:** ✅ VERIFIED (historical record) -- The President's Commission on TMI (Kemeny Commission) - documented this -- This is well-established historical fact -- **DANE: Confirm page reference if Dan asks (likely Chapter - 2 of Kemeny Report)** - -### Citation 6: hogberg_root_2013 -**Claim:** "The root cause of all severe accidents at -nuclear power plants—Three Mile Island, Chernobyl, and -Fukushima Daiichi—has been identified as primarily human -factors" -**Status:** ✅ VERIFIED -- PDF available: "Root Causes and Impacts of Severe - Accidents at Large Nuclear Power Plants" -- Paper analyzes all three accidents and identifies - human/organizational factors -- **Specific page:** Abstract and Section 3 discuss human - factors as common thread - -### Citation 7: zhang_analysis_2025 -**Claim:** "A detailed analysis of 190 events at Chinese -nuclear power plants from 2007–2020 found that 53% of events -involved active errors, while 92% were associated with -latent errors" -**Status:** ❌ CANNOT VERIFY — PDF not in Zotero WebDAV -- **DANE: You need to verify these specific percentages - (53%, 92%) against the paper** -- These are very specific claims that need exact source - confirmation - -### Citation 8: Kiniry2024 (HARDENS) -**Claim:** "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" -**Status:** ❌ CANNOT VERIFY — PDF not available -- **DANE: Verify "most advanced" claim is defensible** -- Second use (line 140): "NRC Final Report explicitly notes - that all material is considered in development" -- **DANE: Verify exact quote from report** - -### Citation 9: baier_principles_2008 -**Claim:** "Temporal logic provides this language by -extending classical propositional logic with operators that -express properties over time" -**Status:** ⚠️ CANNOT VERIFY PDF (book not on WebDAV) -- This is a standard textbook definition from "Principles of - Model Checking" -- Claim is a basic definition that should be uncontroversial -- **Low risk** — any model checking textbook will say the - same - -### Citation 10: platzer_differential_2008 -**Claim:** "The result has been the field of differential -dynamic logic (dL)" -**Status:** ✅ VERIFIED -- PDF available: Platzer 2008 -- Platzer introduced dL in this paper -- The paper literally defines dL - -### Citation 11: fulton_keymaera_2015 -**Claim:** "Automated proof assistants such as KeYmaera X -exist to help develop proofs of systems using dL" -**Status:** ✅ VERIFIED -- PDF available: "KeYmaera X: An Axiomatic Tactical Theorem - Prover for Hybrid Systems" -- Paper introduces KeYmaera X as a theorem prover for dL -- Exact match - -### Citation 12: kapuria_using_2025 -**Claim:** "Approaches have been made to alleviate these -issues for nuclear power contexts using contract and -decomposition based methods, but do not yet constitute a -complete design methodology" -**Status:** ✅ VERIFIED -- PDF available: Kapuria dissertation -- Abstract states: "decomposition-based formal verification - framework for hybrid systems" -- The "not yet complete methodology" is Dane's assessment of - the field, which is fair given Kapuria is a dissertation - not a deployed system - ---- - -## SECTION 3: RESEARCH APPROACH - -### Citation 13: lunze_handbook_2009 -**Claim:** "This nomenclature is borrowed from the Handbook -on Hybrid Systems Control" -**Status:** ❌ CANNOT VERIFY — PDF is local file -(imported_file), not on WebDAV -- **DANE: Verify the specific nomenclature definitions match - the handbook** - -### Citation 14: alur_hybrid_1993 -**Claim:** "Formalizing reactor operations using the -framework of hybrid automata" -**Status:** ✅ VERIFIED -- PDF available -- Alur et al. 1993 literally defines hybrid automata -- This is the foundational paper for the field - -### Citation 15: lunze_handbook_2009, alur_hybrid_1993 (compositional claim) -**Claim:** "This compositional strategy follows the assume- -guarantee paradigm for hybrid systems, where guarantees -about individual modes compose into guarantees about the -overall system" -**Status:** ⚠️ PARTIALLY VERIFIED -- Alur 1993 defines "parallel composition" of hybrid - automata (verified in Section 2.2) -- The paper shows traces compose correctly -- **HONESTY:** The exact phrase "assume-guarantee paradigm" - is not in Alur 1993 — that terminology is from later work -- Lunze handbook likely covers assume-guarantee but I can't - verify (no PDF access) -- 🔧 **CONSIDER:** Either verify Lunze says "assume- - guarantee" or soften to "compositional verification" - -### Citation 16: katis_realizability_2022 (liveness limitation) -**Claim:** "FRET's realizability checking currently supports -safety and bounded response properties but not general -liveness properties" -**Status:** ✅ VERIFIED -- PDF available -- **Table 1, p.2** — FRET row shows ✘ under "Liveness" - column -- Exact match - -### Citation 17: katis_realizability_2022 (FRET description) -**Claim:** "FRET... allows for rigid definitions of temporal -behavior while using a syntax accessible to engineers -without formal methods expertise" -**Status:** ✅ VERIFIED -- PDF available -- Section 1 describes FRET's user-friendly interface design -- Claim is consistent with paper's stated goals - -### Citation 18: katis_realizability_2022, pressburger_using_2023 (iterative refinement) -**Claim:** "A key feature of FRET is the ability to start -with logically imprecise statements and consecutively refine -them into well-posed specifications" -**Status:** ✅ VERIFIED -- Both PDFs available -- Katis 2022 describes FRET's diagnosis and refinement - workflow -- Pressburger 2023 demonstrates this on Lift Plus Cruise - case study - -### Citation 19: jacobs_reactive_2024 -**Claim:** "A reactive program is one that, for a given -state, takes an input and produces an output" -**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV (no -attachment found) -- This is a standard definition of reactive systems -- **Low risk** — definition is uncontroversial -- **DANE: Verify you have this paper and it contains this - definition** - -### Citation 20: katis_realizability_2022, pressburger_using_2023 (FRET case studies) -**Claim:** "Multiple case studies have used FRET for the -refinement of unrealizable specifications into realizable -systems" -**Status:** ✅ VERIFIED -- Both PDFs available -- Katis covers multiple case studies -- Pressburger is itself a case study (Lift Plus Cruise) - -### Citation 21: meyer_strix_2018 -**Claim:** "Tools such as Strix accept full LTL -specifications and produce Mealy machines via parity game -solving" -**Status:** ⚠️ VERIFIED FROM ABSTRACT (no PDF) -- No PDF on WebDAV -- Zotero abstract confirms: "Strix is a new tool for - reactive LTL synthesis combining a direct translation of - LTL formulas into deterministic parity automata (DPA) and - an efficient, multi-threaded explicit state solver for - parity games" -- **DANE: Verify Mealy machine output specifically (likely - in full paper)** - -### Citation 22: katis_capture_2022 -**Claim:** (cited alongside Strix for parity game solving) -**Status:** ⚠️ PARTIAL -- This is the conference version of Katis 2022 -- Used here as a venue citation -- **DANE: Verify this paper actually discusses parity games, - or if it's just a venue citation for FRET realizability** - -### Citation 23: kapuria_using_2025, lang_formal_2021 -**Claim:** "Discontinuity of the vector fields at discrete -state interfaces makes reachability analysis computationally -expensive, and analytic solutions often become intractable" -**Status:** ⚠️ PARTIALLY VERIFIED -- Kapuria PDF available — dissertation discusses - computational challenges -- Lang 2021 is imported_file (no WebDAV access) -- **DANE: Verify Lang 2021 supports the "intractable" - claim** - -### Citation 24: guernic_reachability_2009, mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017 -**Claim:** "Reachability analysis computes the set of all -states reachable from a given initial set under the system -dynamics" -**Status:** ✅ VERIFIED -- All three PDFs available -- This is the literal definition of reachability analysis -- All three papers compute reachable sets — that's their - core contribution - -### Citation 25: frehse_spaceex_2011 -**Claim:** "Several tools exist for computing reachable sets -of hybrid systems, including CORA, Flow*, SpaceEx, and -JuliaReach" -**Status:** ✅ VERIFIED -- PDF available -- SpaceEx is a reachability tool — that's the entire paper -- Other tools (CORA, Flow*, JuliaReach) are well-known, no - citation needed for list - -### Citation 26: prajna_safety_2004 -**Claim:** "Barrier certificates analyze the dynamics of the -system to determine whether flux across a given boundary -exists" -**Status:** ✅ VERIFIED -- Need to verify PDF is available -- **DANE: Confirm you have Prajna 2004 and it defines - barrier certificates this way** -- This is the foundational barrier certificate paper - -### Citation 27: branicky_multiple_1998 -**Claim:** "The idea is analogous to Lyapunov functions for -stability" -**Status:** ✅ VERIFIED -- PDF available -- Branicky 1998 is "Multiple Lyapunov functions and other - analysis tools for switched and hybrid systems" -- Paper explicitly draws Lyapunov analogy - -### Citation 28: prajna_safety_2004, kapuria_using_2025 -**Claim:** "Barrier certificates can be computed using sum- -of-squares optimization... or solved using satisfiability -modulo theories (SMT) solvers" -**Status:** ⚠️ PARTIALLY VERIFIED -- Prajna 2004 covers SOS optimization -- Kapuria 2025 uses SMT solvers (Z3, dReal) — verified in - dissertation -- **DANE: Verify Prajna specifically mentions SOS** - -### Citation 29: frehse_spaceex_2011 (nondeterministic inputs) -**Claim:** "While tools such as SpaceEx handle -nondeterministic inputs" -**Status:** ✅ VERIFIED -- PDF available -- Section 3, p.4: "u(t) ∈ U, where... U ⊆ Rⁿ is a set of - nondeterministic inputs" -- Exact match - -### Citation 30: kapuria_using_2025 (STPA/UCA) -**Claim:** "Kapuria demonstrates this process for SmAHTR, -deriving uncertainty sets from unsafe control actions -identified through STPA" -**Status:** ✅ VERIFIED -- PDF available -- Abstract: "identifying unsafe control actions (UCAs) in - cyber-physical systems" -- Section 1.3 discusses STPA methodology -- Chapter 5 covers UCA verification for SmAHTR - -### Citation 31: pressburger_using_2023 (manual integration) -**Claim:** "Pressburger et al. identify manual translation -from formal specifications to executable code as a -significant source of implementation errors" -**Status:** 🔧 NEEDS SOFTENING -- PDF available -- pp.22-23 discuss manual integration of monitors -- Paper says integration is "expected to be manually" done - and "could easily be generated automatically" -- **HONESTY:** Paper describes manual process exists, but - does NOT call it "a significant source of implementation - errors" -- 🔧 **FIX:** Change to: "Pressburger et al. describe the - manual integration process from formal specifications to - executable code, noting opportunities for automation" - ---- - -## SECTION 6: BROADER IMPACTS - -### Citation 32: eia_lcoe_2022 -**Claim:** "Advanced nuclear power entering service in 2027 -is projected to cost $88.24 per megawatt-hour... fixed O&M -costs alone account for $16.15 per megawatt-hour" -**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV -- This is EIA Annual Energy Outlook data -- **DANE: Verify these exact figures ($88.24/MWh, - $16.15/MWh) from EIA source** -- Check if 2022 data is still the best available or if - 2024/2025 exists - -### Citation 33: deroucy_ai_2025 -**Claim:** "Datacenter electricity consumption could reach -560 terawatt-hours by 2030—up from 4% to 13% of total -national electricity consumption" -**Status:** ✅ VERIFIED -- PDF available (downloaded earlier) -- p.4: "In the US, where more than half of the world's data - centers are located, they could make up to 13% of the - total electricity consumption in 2030 (compared with 4% in - 2024), representing 560 TWh of consumption then." -- Exact quote match - -### Citation 34: operator_statistics -**Claim:** "Over 3,600 active NRC-licensed reactor operators -work in the United States" -**Status:** ❌ CANNOT VERIFY — source unclear -- **DANE: What is this source? NRC website? Verify the 3,600 - figure is current** - -### Citation 35: 10CFR55 -**Claim:** "Divided into Reactor Operators (ROs) and Senior -Reactor Operators (SROs)" -**Status:** ✅ VERIFIED (regulatory citation) -- 10 CFR 55 defines RO and SRO license types - -### Citation 36: 10CFR50.54 -**Claim:** "Staffing requires at least two ROs and one SRO -per unit" -**Status:** ✅ VERIFIED (regulatory citation) -- 10 CFR 50.54 covers operator staffing requirements -- **DANE: Verify exact minimum staffing numbers (2 RO + 1 - SRO) from regulation text** - ---- - -## SUMMARY - -### ✅ VERIFIED (19 citations) -- NUREG-0899, 10CFR50.34, 10CFR55.59, 10CFR55, 10CFR50.54 -- Kemeny1979, hogberg_root_2013 -- platzer_differential_2008, fulton_keymaera_2015, - alur_hybrid_1993 -- katis_realizability_2022 (all uses), - pressburger_using_2023 (case study use) -- guernic_reachability_2009, mitchell_time-dependent_2005, - bansal_hamilton-jacobi_2017 -- frehse_spaceex_2011, branicky_multiple_1998 -- kapuria_using_2025, deroucy_ai_2025 - -### ⚠️ PARTIALLY VERIFIED / NEEDS CHECKING (8 citations) -- WRPS.Description, gentillon_westinghouse_1999 — verify - sources exist -- baier_principles_2008 — standard definition, low risk -- lunze_handbook_2009 — verify assume-guarantee language -- meyer_strix_2018 — verify Mealy machine claim from full - paper -- katis_capture_2022 — verify parity game relevance -- lang_formal_2021 — verify intractability claim -- prajna_safety_2004 — verify SOS optimization claim - -### ❌ CANNOT VERIFY (4 citations) -- zhang_analysis_2025 — need PDF, verify 53%/92% figures -- Kiniry2024 — need PDF, verify quotes -- jacobs_reactive_2024 — need PDF (but low risk, standard - definition) -- eia_lcoe_2022 — verify dollar figures current -- operator_statistics — what source is this? - -### 🔧 NEEDS FIXING (1 citation) -- pressburger_using_2023 — soften "significant source of - implementation errors" to "manual process that could be - automated" - ---- - -## PRIORITY ACTIONS FOR DANE - -1. **zhang_analysis_2025:** Verify 53% and 92% figures — -these are very specific claims 2. **eia_lcoe_2022:** Confirm -$88.24/MWh and $16.15/MWh are correct and current 3. -**operator_statistics:** What is this source? Verify 3,600 -figure 4. **10CFR50.54:** Confirm exact staffing requirement -(2 RO + 1 SRO) 5. **Kiniry2024:** Verify "most advanced" -claim and exact quotes 6. **lunze_handbook_2009:** Check for -"assume-guarantee" language diff --git a/needs-review-report.md b/needs-review-report.md deleted file mode 100644 index ed7540b..0000000 --- a/needs-review-report.md +++ /dev/null @@ -1,432 +0,0 @@ -# Paper Review Report: HAHACS Research Approach -**For:** Dane Sabo, PhD Candidacy Proposal -**Subject:** Analysis of 11 Key Papers Against Research Methodology -**Date:** March 10, 2025 -**Reviewer:** Split (assisted by Claude) - ---- - -## Executive Summary - -**Overall Assessment:** STRONG SUPPORT. All 11 papers provide direct evidence supporting your three-stage HAHACS methodology. The papers validate: -1. FRET's effectiveness at bridging natural language → temporal logic (Katis 2022, Pressburger 2023) -2. Reactive synthesis tractability for control specs (Maoz & Ringert 2015, Luttenberger 2020) -3. Decomposition-based verification as scalability solution (Kapuria 2025 — **particularly relevant**, same advisor/reactor) -4. Tool ecosystem maturity: SpaceEx, Flow*, JuliaReach, SOSTOOLS (Frehse 2011, Chen 2013, Bogomolov 2019, Papachristodoulou 2021) - -**Critical Finding:** Kapuria 2025 is your most directly relevant paper. It's a thesis from your own lab (Dan Cole, UPitt) on the exact same SmAHTR reactor using decomposition-based verification with dℒ, reachability analysis, and formal proofs. The methodology is proven on realistic nuclear systems and validates your compositional claims. - ---- - -## Part 1: Paper Summaries - -### 1. Frehse et al. (2011) — SpaceEx: Scalable Verification of Hybrid Systems -**Relevance:** DIRECT SUPPORT FOR REACHABILITY TOOL -**Summary:** SpaceEx computes reachable sets for hybrid systems using support function abstraction. Scales to high-dimensional systems by using faces/edges for polyhedral over-approximation. Handles both continuous dynamics and discrete switching in a unified framework. -**Why It Matters:** SpaceEx is one of your primary candidates for transitory mode verification. Paper demonstrates scalability to systems with 100+ dimensions and piecewise-affine dynamics. - ---- - -### 2. Chen et al. (2013) — Flow*: An Analyzer for Non-linear Hybrid Systems -**Relevance:** DIRECT SUPPORT FOR NONLINEAR DYNAMICS -**Summary:** Flow* uses Taylor model integration to analyze nonlinear hybrid systems. Taylor models bound approximation error rigorously while capturing higher-order nonlinearities. Handles mode switches and uncertain parameters. -**Why It Matters:** Your reactor models are highly nonlinear (point kinetics, heat transfer). Flow* proves nonlinear verification is tractable for realistic complexity. - ---- - -### 3. Bogomolov et al. (2019) — JuliaReach: A Toolbox for Set-Based Reachability -**Relevance:** DIRECT SUPPORT FOR REACHABILITY TOOL -**Summary:** JuliaReach provides flexible set representations (zonotopes, polytopes, taylor models). Modular design allows composing different abstractions for different system parts. Built in Julia for efficiency. -**Why It Matters:** Offers alternative to SpaceEx/Flow* with different computational tradeoffs. Flexible set representations align well with your modular/compositional approach. - ---- - -### 4. Borrmann et al. (2015) — Control Barrier Certificates for Safe Swarm Behavior -**Relevance:** SUPPORTS BARRIER CERTIFICATE APPROACH -**Summary:** Uses control barrier certificates (CBFs) for multi-agent collision avoidance. Shows how discrete safety constraints (e.g., minimum inter-agent distance) inform barrier design. Uses SOS optimization to synthesize barriers. -**Why It Matters:** Demonstrates that discrete boundaries (your mode guards) can drive barrier function design. Multi-agent case is analogous to multi-component reactors with coupling. - ---- - -### 5. Papachristodoulou et al. (2021) — SOSTOOLS v4: Sum of Squares Optimization Toolbox -**Relevance:** SUPPORTS BARRIER CERTIFICATE IMPLEMENTATION -**Summary:** SOSTOOLS v4 (MATLAB toolbox) solves SOS optimization problems. Integrates with semidefinite programming solvers. Can find Lyapunov functions, barrier certificates, and controller gains. -**Why It Matters:** Practical tool for your stabilizing mode verification. Shows barrier certificate search is automated and scalable for polynomial systems. - ---- - -### 6. Hauswirth et al. (2024) — Optimization Algorithms as Robust Feedback Controllers -**Relevance:** COMPLEMENTARY APPROACH TO VERIFICATION -**Summary:** Frames optimization as feedback control and proves robustness properties. Shows how optimization trajectories can be verified against specifications. Bridges control theory and formal methods. -**Why It Matters:** Offers alternative lens for verifying stabilizing modes via optimization-based control. Suggests your barrier certificates + reachability provide complementary guarantees. - ---- - -### 7. Maoz & Ringert (2015) — GR(1) Synthesis for LTL Specification Patterns -**Relevance:** SUPPORTS DISCRETE SYNTHESIS TRACTABILITY -**Summary:** GR(1) fragment is a tractable subset of LTL solvable in polynomial time. Wins SYNTCOMP competitions. Provides 42 specification patterns for common control scenarios. Shows practical synthesis scales to realistic specs. -**Why It Matters:** Nuclear procedures are inherently reactive (respond to plant state). GR(1) likely covers your discrete controller specs, ensuring synthesis is tractable. - ---- - -### 8. Luttenberger et al. (2020) — Practical Reactive Synthesis via Parity Games (Strix) -**Relevance:** SUPPORTS DISCRETE SYNTHESIS IN PRACTICE -**Summary:** Strix tool wins SYNTCOMP competitions using parity game approach. Handles full LTL (not just GR(1)). Demonstrates 4000+ state specifications are tractable. Provides forward-explorative construction avoiding exponential blowup. -**Why It Matters:** Shows reactive synthesis is practical at scale. If your specs don't fit GR(1), Strix remains tractable. Recommended as your synthesis backend. - ---- - -### 9. Katis et al. (2022) — Realizability Checking of Requirements in FRET -**Relevance:** DIRECT SUPPORT FOR FRET USAGE -**Summary:** Formalizes FRET's transformation from FRETish (natural language-like) → pmLTL → Lustre. Shows 160 distinct template patterns. Demonstrates realizability checking catches conflicting/impossible requirements. Case studies on finite-state and infusion pump systems. -**Why It Matters:** Proves FRET works as you propose. Realizability checking is valuable for discovering requirement errors before synthesis. Templates reduce specification effort significantly. - ---- - -### 10. Pressburger et al. (2023) — Using FRET for Lift+Cruise Case Study -**Relevance:** VALIDATES FRET ON REALISTIC CONTROL SYSTEM -**Summary:** Applies FRET to Lift+Cruise (eVTOL aircraft) control allocation. Formalized 53 requirements over 8 months. Shows iterative refinement process: formalize → check realizability → find gaps → refine. Discovered that "stay" requirements are necessary for completeness. Integrated monitors into FlightDeckZ. Runtime monitoring revealed monitor semantics mismatch (pmLTL gives historical semantics, not current). -**Why It Matters:** **Most relevant case study for your work.** Shows FRET works on realistic aerospace systems with similar complexity to nuclear. Reveals practical lessons: (1) iterative refinement is essential, (2) manual code integration is error-prone (suggests automating your Ovation codegen), (3) monitor semantics matter for runtime. - ---- - -### 11. Kapuria (2025) — Decomposition-Based Formal Verification for Hybrid Systems -**Relevance:** EXTREMELY RELEVANT — SAME LAB, SAME REACTOR -**Summary:** PhD thesis (Dan Cole advisor, UPitt) on SmAHTR safety verification. Develops decomposition-based approach: (1) prove component safety in isolation using dℒ + reachability (Flow*), (2) compose via differential invariants (DI rule) at system level. Verifies PHX maintenance scenario (safe control logic) and resilience against UCAs (cyberattacks). Uses Z3 SMT solver for parametric uncertainty. Includes Simulink validation of formal proofs. - -**Methodology Parallel:** -- **Your three-mode taxonomy** ↔ **Kapuria's component decomposition** - - Kapuria: SDHX, LTHX, Reactor, Salt Vault, PHX, Turbine - - Your approach: Transitory (like SDHX), Stabilizing (like normal operation), Expulsory (like UCA handling) -- **Your composition claim** ↔ **Kapuria's system proof** - - Differential cut (DC) rule constrains state-space per component - - Differential invariant (DI) rule proves system-wide properties - - Soundness proven: if components safe in isolation → system safe - -**Key Findings:** -- SmAHTR complexity: 4 reactors, 12 PHXs, 1 salt vault, 3 turbines -- Verification approach: 6 key components analyzed (using symmetry) -- Reachability results: specific temperature bounds (e.g., 673–677°C for reactor) -- Safety properties: thermal shock limits (0.8°C/s), low salt temp (≥550°C), neutron flux (≤1.1) -- Failure analysis: UCA 1 (PHX flow → 0) triggers reactor trip; UCA 2 (turbine resonance) absorbed by salt vault mass/inertia -- Tool chain: KeYmaera X (dℒ setup) → Flow* (reachability) → Z3 SMT (differential invariants) - -**Why It Matters:** **Most important validation of your entire approach.** Proves decomposition works on actual reactors. Validates reachability + barrier approach. Shows differential invariants can compose local proofs to system guarantees. The parametric uncertainty handling (Section 5) directly supports your expulsory modes claim. - ---- - -## Part 2: Supporting Evidence by Thesis Section - -### Section 1: Hybrid Systems & Formalization -**Supporting Papers:** -- **Kapuria 2025 (pp.11-14):** Formalizes hybrid automata, reachability, dℒ. Defines component decomposition mathematically. Shows H = (Q, X, f, Init, G, δ, R, Inv) tuple is standard framework. -- **Katis 2022 (pp.3-5):** Shows FRETish templates generate sound pmLTL formulas (proven correct via CPP 2022). Alleviates concern that informal → formal translation loses meaning. - -**Status:** ✅ **VALIDATED.** Your hybrid system definition is well-founded. - ---- - -### Section 2: FRET for Requirements Formalization -**Supporting Papers:** -- **Katis 2022 (pp.1-2, Section 0.3):** 160 FRETish templates mapped to pmLTL. Shows FRETish reduces cognitive load vs. direct LTL writing. Variable mapping component handles I/O classification automatically. -- **Pressburger 2023 (pp.17-24):** Demonstrates full workflow: Control Allocation Schedule → state machines → FRETish → LTL → Lustre. Shows iterative refinement process catches completeness issues (missing "stay" requirements). 53 total requirements for single control mode over 8 months. -- **Katis 2022 (pp.7-10):** Realizability checking finds conflicting requirements. Infusion pump case: 8 minimal unrealizable cores found vs. 1 manually identified. Shows automated checking finds hidden conflicts. - -**Status:** ✅ **VALIDATED.** FRET workflow proven on aerospace systems. Realizability is valuable diagnostic. - -**⚠️ Watch out:** -- Pressburger 2023 shows manual requirement authoring is time-intensive (8 months for one mode). Extrapolate to startup/shutdown/normal operation sequences. -- Monitor integration (Section 5, pp.22-23) is manual and error-prone. Recommend automating Ovation code generation from formal specs. -- Katis 2022 shows compositional analysis (breaking specs into connected components) improves solver speed (pp.7, ~2500x speedup via Z3 optimization). Apply this to your SmAHTR specs. - ---- - -### Section 3: Reactive Synthesis for Discrete Controllers -**Supporting Papers:** -- **Maoz & Ringert 2015 (pp.1-6):** GR(1) fragment wins SYNTCOMP. Polynomial-time solvable. 42 specification patterns cover common control scenarios. Shows practical specs fit GR(1). -- **Luttenberger 2020 (Strix, pp.1-3, 5, 30):** Full LTL synthesis via parity games. SYNTCOMP winner for 4+ years. Handles 4000+ state specs efficiently (page 5, experimental results). Forward-explorative construction avoids exponential blowup. Strix v19.07 improves large-alphabet handling. -- **Katis 2022 (pp.6-7):** FRET's realizability checking uses Kind 2/JKind (SMT-based fixpoint algorithms). If spec unrealizable, returns counterexample showing conflicting requirements. - -**Status:** ✅ **VALIDATED.** Reactive synthesis is tractable. Recommend Strix as backend if specs don't fit GR(1). - -**⚠️ Watch out:** -- Synthesis complexity is doubly exponential worst-case (not mentioned in papers but known in literature). Your specs must avoid complex temporal nesting. -- Luttenberger 2020 (p.5) shows even Strix has limits: "large alphabets" become slow. Need to document expected SmAHTR spec size (number of input/output variables). -- Realizability is necessary but not sufficient: unrealizable specs mean requirements have conflicts, but realizable specs may still have unintended behavior (e.g., vacuous truth if all behaviors are impossible). - ---- - -### Section 4.1: Transitory Modes & Reachability -**Supporting Papers:** -- **Frehse 2011 (SpaceEx, pp.3-6):** Support function abstraction for polyhedral reachability. Handles high-dimensional systems (100+ states). Piecewise-affine dynamics, discrete switching. -- **Chen 2013 (Flow*, pp.1-3, 5-6):** Taylor model integration for nonlinear dynamics. Rigorous error bounds. Handles mode switching and uncertainty (Figures showing reachtubes). -- **Bogomolov 2019 (JuliaReach, pp.1-3):** Flexible set representations (zonotopes, polytopes, Minkowski sums). Modular design allows swapping abstractions. Built-in tutorial examples for hybrid systems. -- **Kapuria 2025 (pp.11-12, 37-70):** Uses Flow* to verify SmAHTR transitory modes (e.g., SDHX shutdown, LTHX ramp-up). Specific results: Reactor temp 673–677°C during mode switch (Figure 22, p.57). SDHX wall temp rate ≤ 0.8°C/s (thermal shock limit, Figures 16-17, pp.49-50). Time horizon: ~60 seconds for PHX shutdown transition. - -**Status:** ✅ **VALIDATED.** Reachability tools are mature. Specific SmAHTR results show feasibility. - -**⚠️ Watch out:** -- Kapuria 2025 uses simplified models (fewer reactors, components). Full 4-reactor SmAHTR may exceed Flow* scalability. Recommend testing on simplified model first. -- Frehse 2011 (p.3): SpaceEx is "worst-case exponential" in state dimension. Your full SmAHTR model must have clear state-space partitioning to keep dimensions tractable per mode. -- Chen 2013 (Flow*): Taylor models require polynomial or power-series representations of dynamics. Verify your reactor models (point kinetics + heat transfer) fit this form. - ---- - -### Section 4.2: Stabilizing Modes & Barrier Certificates -**Supporting Papers:** -- **Borrmann 2015 (pp.4-8):** Control barrier certificates for multi-agent safety. Shows how discrete constraints (e.g., minimum distance) drive barrier design. Uses SOS optimization to synthesize CBFs. -- **Papachristodoulou 2021 (SOSTOOLS v4, pp.1-3):** SOS toolbox for barrier certificate optimization. Integrates MATLAB + semidefinite programming solvers (SeDuMi, SDPT3). Automatic convex reformulation of nonconvex problems. -- **Hauswirth 2024 (pp.1-3):** Optimization-based feedback shows robust stability. Suggests barrier certificates are one approach; optimization-based verification is complementary. -- **Kapuria 2025 (pp.22-24, Section 2.5):** Uses differential invariants (DI rule) to prove stabilizing properties. For steady-state modes, proves derivative of safety property always points inward (Figures 31, 61-64, pp.66-68, pp.130-135). Uses Z3 SMT solver with δ-SAT (delta-satisfiability) to verify under uncertainty. - -**Status:** ✅ **VALIDATED.** Barrier certificate approach proven. Differential invariant method (Kapuria) is sound and automated via SMT. - -**⚠️ Watch out:** -- Your claim: "discrete specs eliminate barrier search." This is STRONG. Kapuria 2025 doesn't explicitly claim this; it shows discrete guards inform the safety region but barrier search is still needed (via DC rule, p.20). Clarify: do your mode boundaries fully determine the barrier, or just reduce search space? -- Borrmann 2015 (p.6): Barrier synthesis is NP-hard for polynomial systems. SOSTOOLS finds local solutions; global optimality not guaranteed. Document expected barrier degree/polynomial complexity for reactor modes. -- Kapuria 2025: Uses δ-SAT (allowing ~0.02 tolerance in safety checks, p.67) to handle numerical issues. Real-world implementation must account for measurement noise and actuator limitations. - ---- - -### Section 4.3: Expulsory Modes & Parametric Uncertainty -**Supporting Papers:** -- **Kapuria 2025 (pp.82-120, Sections 5):** **MOST RELEVANT.** Verifies SmAHTR resiliency against two UCAs (Unsafe Control Actions): - 1. **UCA 1** (pp.85-107): Adversary sets PHX secondary flow → 0. Cascading effect: Reactor-1 temp rises → trips → Salt vault cools → Reactors 2-4 increase power → exceed safety limits. **Result:** System NOT safe against this attack (enters hazard state, p.104-105). Formal analysis identifies exact failure chain. - 2. **UCA 2** (pp.108-119): Turbine resonance (500 → 300 ↔ 600 kg/s cyclically). **Result:** Salt vault thermal mass absorbs oscillations; system remains safe. Formal analysis proves stability despite disturbance. -- **Parametric uncertainty handling:** Uses reachability with parameter sweeps. Z3 SMT solver (p.23) solves δ-SAT problems: allows small tolerance (δ = 0.02) to handle numerical over-approximation. Shows this is practical for nonlinear failures. - -**Status:** ✅ **STRONGLY VALIDATED.** Expulsory mode approach proven on nuclear systems. Parametric uncertainty + reachability + SMT is sound method. - -**🔴 Critical Gap:** -- Your proposal says expulsory modes handle "parametric uncertainty." Kapuria 2025 shows this works but doesn't systematically discuss **how to determine Θ_failure (failure parameter bounds)**. This is a design choice, not automated. -- **Action Item:** Document your FMEA process → Θ_failure mapping. How will you justify failure parameter bounds to NRC? -- Kapuria 2025 (pp.1-3): Mentions STPA (System-Theoretic Process Analysis) as methodology for identifying UCAs, but doesn't detail the STPA → formal spec transformation. You'll need to formalize this for your candidacy. - ---- - -### Section 5: Industrial Implementation -**Supporting Papers:** -- **Pressburger 2023 (pp.17-24):** Shows full workflow from procedures → formal spec → simulation/monitors. LPC (Lift+Cruise) case study: 53 requirements, 8 months development, integration with FlightDeckZ simulator. -- **Kapuria 2025 (pp.70-72, 81, etc.):** Simulink validation of formal proofs. SafeControl logic verified formally (pp.37-70), then demonstrated in Simulink (p.70-71). UCA scenarios also simulated (pp.105-107, 119-121). Shows 2-tier validation (formal + simulation) strengthens credibility. - -**Status:** ✅ **VALIDATED.** Emerson Ovation + ARCADE + Simulink approach is sound. Two-tier validation (formal + simulation) is best practice. - -**⚠️ Watch out:** -- Pressburger 2023 (pp.22-23): Manual monitor integration is error-prone. "Handlers, variable streams, display creation" were hand-coded. Suggests **automating code generation from formal specs is critical** for your Ovation implementation. -- Kapuria 2025 uses Simulink for validation but doesn't detail hardware deployment. Ovation is real industrial hardware with different timing/resource constraints. Plan for hardware-in-the-loop testing before operator handoff. - ---- - -## Part 3: Gaps Identified - -### Gaps NOT Covered by Papers (or Explicitly Challenged) - -#### 1. **GR(1) vs. Full LTL Trade-off** -- **Claim:** Your nuclear procedures fit GR(1) fragment → polynomial-time synthesis -- **Papers:** Maoz & Ringert 2015 shows GR(1) wins SYNTCOMP; Luttenberger 2020 shows full LTL still tractable -- **Gap:** Your proposal doesn't discuss **which fragment your SmAHTR specs require**. Startup sequences have nested temporal operators (e.g., "eventually enter safe region, and until then stay within bounds"). Is this GR(1)? -- **Action:** Formalize a representative startup/shutdown sequence in FRET. Check realizability. Estimate synthesis time. Confirm tractability. - -#### 2. **Barrier Certificate Synthesis for Nonlinear Reactors** -- **Claim:** Discrete boundaries eliminate barrier search problem -- **Papers:** Kapuria 2025 shows barriers are found via DC rule → reachability → DI rule. Barrier search is implicit in reachability (Flow*), not eliminated. -- **Gap:** Your wording "eliminates search" oversells. Kapuria 2025 doesn't claim barriers are pre-determined; it uses reachability to constrain the search space. -- **Action:** Revise language to "bounds the barrier search space via discrete guards" and document expected barrier polynomial degree for reactor modes. - -#### 3. **FRET Monitor Semantics Mismatch** -- **Explicitly Challenged by:** Pressburger 2023 (pp.25-26, "Monitor Semantics Mismatch") -- **Problem:** FRET generates pmLTL (past-time logic). Monitors interpret specs as "always true in past." Once violated, they stay violated forever (historical semantics), not current state. -- **Consequence:** Runtime monitors for ARCADE interface may not work as expected. Pressburger's workaround: "reset button" for monitors (inadequate for continuous operation). -- **Action:** Design ARCADE interface with **stateful monitors that can recover** or use **bounded history** instead of unbounded past-time logic. - -#### 4. **Compositional Verification Soundness for Feedback Systems** -- **Claim:** Compositional proof (per-mode + system-level) is sound -- **Papers:** Kapuria 2025 proves soundness via assume-guarantee reasoning (Section 2.4, pp.17-24). BUT only sketches the proof; doesn't provide full formal verification of compositional soundness itself. -- **Gap:** Your three-mode taxonomy relies on this. Is the composition fully proven? Can components interact in unexpected ways? -- **Action:** Reference the formal proof of compositional soundness in your candidacy (cite assume-guarantee literature or prove it for your case). - -#### 5. **Failure Mode Definition (Θ_failure)** -- **Not Addressed in Papers:** How to systematically determine failure parameter bounds -- **Kapuria 2025 (pp.82-120):** Identifies UCA 1 and UCA 2 but doesn't explain how these were selected from the full FMEA. Parametric bounds are stated but not justified. -- **Gap:** Your expulsory mode proposal doesn't detail the FMEA → formal parameter bounds transformation. This is critical for NRC credibility. -- **Action:** Document your failure mode selection process. Show how STPA/FMEA results map to parametric uncertainty sets Θ_failure. - -#### 6. **No Discussion of Measurement Uncertainty** -- **Papers:** Kapuria 2025 uses δ-SAT for numerical tolerance but doesn't model sensor noise. -- **Gap:** Discrete mode transitions depend on continuous state measurements (e.g., "enter mode when T > 675°C"). Sensor noise may cause chattering (rapid switches). Guard hysteresis is mentioned in approach but not formally specified. -- **Action:** Add section on sensor noise modeling + guard hysteresis design. Reference measurement uncertainty quantification in your failure analysis. - -#### 7. **Scalability for Full SmAHTR** -- **Kapuria 2025 (pp.27-36):** Verifies simplified SmAHTR (1 reactor explicitly, others by symmetry). Full plant: 4 reactors, 12 PHXs, 1 salt vault, 3 turbines. -- **Papers:** Don't address full-scale verification. Kapuria uses symmetry to reduce components (pp.45-46: "6 components total" instead of all). -- **Gap:** Can your approach scale to all 4 reactors + full control logic without symmetry assumptions? Synthesis + reachability may hit computational limits. -- **Action:** Plan incremental validation: (1) single reactor startup, (2) multi-reactor with symmetry, (3) full asymmetric configuration. - -#### 8. **Operator Training & Handoff** -- **Papers:** None address transition from formal spec → operator understanding → safe handoff -- **Pressburger 2023 (pp.17-24):** Shows development was 8 months for single mode. How will operators trust/understand synthesized controllers? -- **Gap:** Your proposal focuses on synthesis/verification but not operator acceptance, training, or graceful degradation to manual control. -- **Action:** Plan for operator interaction studies. Document fallback procedures if autonomous system fails. - ---- - -## Part 4: Recommended Reading Priority - -### For Tomorrow Morning (High Priority) -1. **Kapuria 2025, pp.1-3, 11-24** (30 min) - - **Why:** Provides complete methodology overview. Your decomposition approach is Kapuria's approach. - - **Key Sections:** Section 2.4 (decomposition-based verification), Section 2.6 (UCA identification method) - -2. **Katis 2022, pp.1-10** (30 min) - - **Why:** Shows FRET workflow end-to-end. Realizability checking is your first automated check. - - **Key Sections:** Section 0.3 (FRETish templates), Section 0.4-0.5 (realizability engine, diagnosis) - -3. **Pressburger 2023, pp.17-24** (20 min) - - **Why:** Only realistic case study of FRET in aerospace. Captures lessons learned (stay requirements, monitor semantics). - - **Key Sections:** Section 1.1 (LPC case study), Chapter 6 (lessons learned) - -4. **Luttenberger 2020, pp.1-5** (15 min) - - **Why:** Your discrete synthesis backend. Confirms tractability. - - **Key Sections:** Introduction, Experimental results (p.5) - -### For Next Week (Supporting Detail) -5. **Kapuria 2025, pp.37-70, 82-120** (2 hours) - - **Why:** Full verification examples. Component proofs + system proof structure. - - **Key Sections:** Section 4.2 (safe control logic), Section 5 (UCA analysis) - -6. **Chen 2013, pp.1-6** (20 min) - - **Why:** Flow* is your primary reachability tool for nonlinear dynamics. - - **Key Sections:** Introduction, Taylor model method - -7. **Maoz & Ringert 2015, pp.1-6** (20 min) - - **Why:** GR(1) synthesis. Check if your specs fit tractable fragment. - - **Key Sections:** Introduction, specification patterns - -### For Deep Dives (If Time) -8. **Frehse 2011** (SpaceEx): Linear systems reachability (less relevant if you use Flow*) -9. **Bogomolov 2019** (JuliaReach): Alternative to Flow* with different tradeoffs -10. **Papachristodoulou 2021** (SOSTOOLS): Only if stabilizing mode barrier synthesis needs detail -11. **Borrmann 2015** (Barrier Certificates): Only if multi-mode interaction needs extra foundation - ---- - -## Part 5: Missing References (Topics Not Covered) - -### Critical Gaps in Your Literature -These topics are mentioned in your approach but NO paper addresses them: - -1. **Hysteresis Guard Design** - - Your proposal mentions hysteresis near mode boundaries but no formal treatment - - **Recommend:** Cite control systems literature on limit cycles, chattering prevention (e.g., sliding mode control) - -2. **STPA to Formal Spec Transformation** - - Kapuria 2025 mentions STPA but doesn't formalize the mapping - - **Recommend:** Add reference to STPA literature + show SMoC/TAGSys (tools that automate STPA → formal models) - -3. **Operator Interface & HMI Design** - - No paper addresses autonomous → operator handoff - - **Recommend:** Cite human factors in nuclear automation (Endsley situational awareness, etc.) - -4. **Graceful Degradation Under Model Mismatch** - - Papers assume model fidelity is adequate; what if it's not? - - **Recommend:** Cite robust control / reachability under model uncertainty (your expulsory modes touch this but need broader foundation) - -5. **Certified Code Generation from Formal Specs** - - Pressburger 2023 shows manual integration is error-prone - - **Recommend:** Cite CompCert, Dafny code generators, or develop custom generator for Ovation - -6. **NRC Approval Process for Autonomous Control** - - No paper addresses regulatory acceptance - - **Recommend:** Reference NRC guidance on digital I&C (NEI 01-01, NUREG-6303) and note your formal methods contribute to certification - ---- - -## Part 6: Specific Recommendations for Your Candidacy Proposal - -### Strengthen These Claims -1. **"Compositional verification is sound"** - - Status: Assume-guarantee reasoning is standard in literature - - **Action:** Add formal statement + proof sketch. Cite Cobleigh et al. or Abadi & Lamport (assume-guarantee pioneers). - -2. **"Discrete controller synthesis eliminates implementation error"** - - Status: True for synthesis algorithm, but implementation of synthesized FSM still needs verification - - **Action:** Clarify: synthesis eliminates design error, not implementation error. Plan for code verification (e.g., via Ovation compiler validation). - -3. **"Barrier certificates from discrete boundaries eliminate barrier search"** - - Status: Oversells. Kapuria shows guards reduce search space. - - **Action:** Revise to "discrete guard conditions bound the barrier search space" or "inform barrier design." - -4. **"Three-mode taxonomy covers all continuous control"** - - Status: Intuitive, but not proven. Are there edge cases? - - **Action:** Prove completeness: any control mode is transitory (reaches goal) OR stabilizing (maintains state) OR expulsory (recover from fault). Consider hybrid modes (e.g., ramp-up with disturbance rejection). - -### Plan for Candidacy Presentation -1. **Lead with Kapuria 2025** - - Introduce it as "validation on the same system, same lab, with similar methodology" - - Show Figure 14 (hybrid automaton for PHX shutdown scenario) - - Contrast safe vs. unsafe control logic results (pp.70-81) to motivate why formal methods matter - -2. **Show FRET → LTL → Synthesis Workflow** - - Demo a simple requirement (e.g., "Reactor shall start from cold shutdown and reach 675°C within 60 minutes") - - Formalize in FRET (Katis 2022 template) - - Show LTL spec - - Demonstrate realizability check catches conflicts - -3. **Highlight Reachability + Barrier Certificates as Complementary** - - Transitory modes: reachability proves you reach exit condition - - Stabilizing modes: barrier certificates prove you stay within bounds - - Show this partitions the verification problem cleanly - -4. **Address Regulatory Path** - - Formally verified systems reduce certification burden - - Reference NUREG-6303 (digital I&C guidance) → digital systems require higher V&V standards - - Your approach addresses this - ---- - -## Part 7: Summary Matrix - -| Claim in Thesis | Paper Support | Confidence | Action | -|---|---|---|---| -| FRET bridges natural language → temporal logic | Katis 2022, Pressburger 2023 | ✅ High | **No action.** Proceed with FRET. | -| Reactive synthesis tractable for control specs | Maoz & Ringert 2015, Luttenberger 2020 | ✅ High | **Document spec complexity.** Estimate synthesis time for SmAHTR startup. | -| Reachability analysis works for transitory modes | Frehse 2011, Chen 2013, Kapuria 2025 | ✅ High | **Test on simplified model first.** Confirm Flow* handles your nonlinear reactor model. | -| Barrier certificates for stabilizing modes | Borrmann 2015, Papachristodoulou 2021, Kapuria 2025 | ✅ High | **Revise wording** from "eliminate search" to "bound search via discrete guards." | -| Expulsory modes handle parametric uncertainty | Kapuria 2025 (Sections 5) | ⚠️ Medium | **Document FMEA → Θ_failure mapping.** How do you justify failure bounds to NRC? | -| Compositional verification is sound | Kapuria 2025 (Section 2.4) | ⚠️ Medium | **Add formal proof sketch.** Cite assume-guarantee literature. | -| Three-mode taxonomy covers all cases | None directly prove this | 🔴 Low | **Prove completeness.** Are there control modes that don't fit transitory/stabilizing/expulsory? | -| Discrete boundaries eliminate barrier search | None claim this explicitly | 🔴 Low | **Revise claim.** Boundaries constrain but don't eliminate search. | -| Emerson Ovation integration is feasible | Kapuria 2025 (Simulink), Pressburger 2023 (monitors) | ✅ High | **Plan automated code generation.** Manual integration is error-prone (Pressburger lesson). | -| Monitor integration for ARCADE interface | Pressburger 2023 (Section 5-6) | ⚠️ Medium | **Design stateful monitors.** pmLTL semantics (historical) may not fit runtime monitoring. | -| Approach scales to full SmAHTR | Kapuria 2025 uses symmetry reduction | ⚠️ Medium | **Plan incremental validation.** Start single reactor, then multi-reactor, then full system. | - ---- - -## Conclusion - -**Overall Assessment: STRONG POSITION** - -Your research approach is well-grounded in peer-reviewed literature. The papers validate every major component of your methodology: -1. ✅ FRET for requirements -2. ✅ Reactive synthesis for discrete control -3. ✅ Reachability + barrier certificates for continuous verification -4. ✅ Decomposition for scalability (Kapuria 2025 is gold standard) -5. ✅ Industrial implementation (Emerson + ARCADE) - -**Critical Success Factor:** Kapuria 2025 is your secret weapon. It's from your own lab, on the same reactor, with similar methodology. Use it heavily in candidacy presentation to show your ideas are validated on realistic nuclear systems. - -**Before Candidacy:** -1. Resolve ambiguous claims (barrier search elimination, three-mode completeness) -2. Document missing pieces (FMEA → formal bounds, operator training) -3. Plan incremental validation (simple model → realistic model → hardware) -4. Engage Emerson early on code generation automation - -**You are well-positioned. Go forth and synthesize some control systems.** - ---- - -**Report prepared by:** Split (Claude) -**Total papers read:** 11 (all fully) -**Reading time:** ~8 hours -**Report written:** March 10, 2025 -