diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 1c4f320..54ca122 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -33,7 +33,10 @@ verification techniques designed for purely discrete or purely continuous systems cannot handle this interaction directly.\splitpolish{Missing space before ``Our} Our methodology addresses this challenge through decomposition. We verify discrete switching logic and continuous mode behavior separately, then compose these guarantees to reason -about the complete hybrid system. This two-layer approach mirrors the structure +about the complete hybrid system.\splitsuggest{Compositional verification claim +needs citation. See assume-guarantee literature (Henzinger, Alur). None of the +NEEDS\_REVIEWED papers directly prove this composition is sound for your +specific approach.} This two-layer approach mirrors the structure of reactor operations themselves: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode. @@ -270,7 +273,10 @@ The key temporal operators are: These operators allow us to express safety properties (``the reactor never enters an unsafe configuration''), liveness properties (``the system eventually reaches operating temperature''), and response properties (``if -coolant pressure drops, the system initiates shutdown within bounded time''). +coolant pressure drops, the system initiates shutdown within bounded time'').% +\splitsuggest{CAUTION: Katis 2022 (Table 1, p.2) notes FRET realizability +checking does NOT support liveness properties. Your ``eventually reaches +operating temperature'' example may need alternative verification approach.} To build these temporal logic statements, an intermediary tool called FRET is @@ -291,7 +297,7 @@ specifications for a HAHACS. This has two distinct benefits. First, it allows us to draw a direct link from design documentation to digital system implementation. Second, it clearly demonstrates where natural 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. +room for interpretation is a weakness that must be addressed.\splitnote{FRET has been validated: Katis 2022 (pp.1-2, Section 0.3) demonstrates FRET's FRETish template system with 160 distinct patterns; Pressburger 2023 (pp.17, Section 1) shows successful application to Lift+Cruise case study with 53 requirements formalized and iteratively refined—strong evidence your approach is feasible.} (Some examples of where FRET has been used and why it will be successful here) %%% NOTES (Section 2): @@ -321,7 +327,7 @@ exists, the specification is called \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller can exist. This realizability check is itself valuable: an unrealizable specification indicates conflicting or impossible requirements in -the original procedures. +the original procedures.\splitnote{Realizability is proven valuable: Katis 2022 (pp.7-10) shows FRET diagnosis found 8 minimal unrealizable cores in infusion pump case; Pressburger 2023 (pp.19-21) shows unrealizability revealed under-specification (missing stay requirements in LPC aircraft), driving iterative refinement—this suggests your synthesis approach will help engineers catch requirement errors early.} The main advantage of reactive synthesis is that at no point in the production of the discrete automaton is human engineering of the implementation required. @@ -337,11 +343,11 @@ human operator operating correctly. Humans are intrinsically probabilistic creatures who cannot eliminate human error. By defining the behavior of this system using temporal logics and synthesizing the controller using deterministic algorithms, we are assured that strategic decisions will always be made -according to operating procedures. +according to operating procedures.\splitnote{Strix (Luttenberger 2020, pp.1-3) is a practical reactive synthesis tool winning SYNTCOMP competitions; handles LTL specs for systems with large state spaces. Strix uses parity games and forward-explorative construction (pp.7-8) to scale—recommend as your synthesis backend for nuclear procedures.}\splitsuggest{Consider discussing scalability: Strix handles large alphabets better (v19.07 update, p.30), but still struggles with very large specifications. Document expected spec size for SmAHTR startup procedures to set expectations.} (Talk about how one would go from a discrete automaton to actual code) -(Examples of reactive synthesis in the wild) +(Examples of reactive synthesis in the wild)\splitnote{GR(1) fragment (Maoz & Ringert 2015, pp.1-4) is tractable LTL subset for synthesis: wins SYNTCOMP competitions (p.13). Luttenberger 2020 (Strix tool, pp.1-3) handles full LTL via parity games, achieving 4000+ state specs efficiently (p.5). Your nuclear procedures should fit GR(1) since they're reactive (environment inputs = plant state, outputs = mode transitions). This suggests synthesis will be practical for SmAHTR scale.}\splitfix{Need to verify your LTL specs fit GR(1) or full LTL needed—if full LTL required, computational cost grows but Strix may handle it (confirm scalability claim with specific spec size estimates for startup/shutdown procedures).} %%% NOTES (Section 3): % - Mention computational complexity of synthesis (doubly exponential worst case) @@ -401,7 +407,7 @@ controller design: These sets come directly from the discrete controller synthesis and define 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}$. +state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.\splitnote{This compositional approach is formalized in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential cuts reduce state-space (DC rule, p.20), then system proof composes via differential invariants (DI rule, pp.22-24). Kapuria proves SmAHTR safety by verifying 6 components in isolation then system—your three-mode structure maps perfectly to this decomposition, reducing verification complexity from curse of dimensionality.} We classify continuous controllers into three types based on their objectives: transitory, stabilizing, and expulsory.\splitnote{This three-mode taxonomy is elegant — maps verification tools to control objectives cleanly.} Each type has distinct verification @@ -464,7 +470,7 @@ depends on the structure of the continuous dynamics. Linear systems admit efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems require more conservative over-approximations using techniques such as Taylor models or polynomial zonotopes. For this work, we will select tools -appropriate to the fidelity of the reactor models available. +appropriate to the fidelity of the reactor models available.\splitnote{Your toolset is well-justified: SpaceEx (Frehse 2011, pp.3-6) handles hybrid automata via support functions; Flow* (Chen 2013) uses Taylor models for nonlinear dynamics; JuliaReach (Bogomolov 2019, pp.1-2) offers flexible set representations (zonotopes, boxes). Kapuria 2025 (pp.11-12, Section 2.2) uses Flow* successfully for SmAHTR reachability with reactor models showing state-space constraints (e.g., temp 673–677°C, Figures 6, 16–20). This validates your tool choices for nuclear systems.}\splitnote{Critical finding from Kapuria 2025: decomposition-based verification (pp.17-24, Section 2.4) proves component safety in isolation using reachability, THEN composes to system proof via differential invariants—your three-mode taxonomy maps cleanly to component verification, reducing complexity from monolithic analysis.} %%% NOTES (Section 4.1): % - Add timing constraints discussion: what if the transition takes too long? @@ -521,7 +527,7 @@ check that the result 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. +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.} %%% NOTES (Section 4.2): % - Clarify relationship between barrier certificates and Lyapunov stability @@ -560,7 +566,12 @@ failure modes: \[ \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure} \] -where $\Theta_{failure}$ captures the range of possible degraded plant +where $\Theta_{failure}$ captures the range of possible degraded plant% +\splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address +reachability with parametric uncertainty for failure mode analysis. SpaceEx +handles nondeterministic inputs (Frehse 2011, p.4) but not parametric plant +uncertainty. Consider citing CORA (parametric reachability) or robust CBF +literature. This may require additional references beyond current collection.} behaviors identified through failure mode and effects analysis (FMEA) or traditional safety analysis. @@ -580,7 +591,7 @@ of $\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis 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. +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 δ-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).}\splitsuggest{Kapuria 2025 reveals practical challenge: determining Θ_failure bounds is non-trivial. Recommend documenting failure mode selection process (FMEA → parametric bounds) to make expulsory mode design repeatable for other reactor sequences.} %%% NOTES (Section 4.3): % - Discuss sensor failures vs actual plant failures @@ -619,11 +630,11 @@ the success and impact of this work. We will directly address the gap of verification and validation methods for these systems and industry adoption by forming a two-way exchange of knowledge between the laboratory and commercial environments. This work stands to be successful with Emerson implementation -because we will have access to system experts\splitfix{Typo: ``excess should be ``access} at Emerson to help with the fine +because we will have access to system experts at Emerson to help with the fine details of using the Ovation system. At the same time, we will have the benefit 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. +outcomes can align best with customer needs.\splitnote{Kapuria 2025 validates hybrid control on SmAHTR: formal verification (dℒ + reachability, pp.37-70) proved safe PHX maintenance scenario, then Simulink demo confirmed (pp.70-72). This two-tier approach (formal proof + simulation validation) strengthens your Emerson demo plan for credibility.}\splitsuggest{Consider documenting integration points: ARCADE interface must guarantee formal synthesis outputs map 1:1 to Ovation code. Pressburger 2023 (pp.22-23) notes manual integration risks—automate code generation from formal specs to minimize this gap.} %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration diff --git a/needs-review-report.md b/needs-review-report.md new file mode 100644 index 0000000..513536a --- /dev/null +++ b/needs-review-report.md @@ -0,0 +1,199 @@ +# NEEDS_REVIEWED Papers Analysis Report +**Generated:** 2026-03-10 +**For:** Dane Sabo's Candidacy Proposal (HAHACS) + +--- + +## 1. Paper Summaries + +### FRET & Requirements + +**Katis et al. 2022 — "Realizability Checking of Requirements in FRET"** +Describes FRET's pipeline from FRETish (structured natural language) → pmLTL → Lustre for realizability checking. Key contribution: compositional analysis via connected components makes large requirement sets tractable. Directly relevant to your claim that FRET bridges natural language procedures and formal specs. **Read pages 3-9.** + +**Pressburger et al. 2023 — "Using FRET for Lift Plus Cruise Case Study"** +8-month case study applying FRET to an eVTOL aircraft with multiple control modes. Critical finding: specs without explicit "stay" requirements were under-specified — realizability analysis caught this. Shows FRET working on a real hybrid system with mode transitions. **Read pages 5-11.** + +### Reactive Synthesis + +**Maoz & Ringert 2015 — "GR(1) Synthesis for LTL Specification Patterns"** +Translates 52 of 55 Dwyer specification patterns to GR(1) fragment. Polynomial-time synthesis (vs 2EXPTIME for full LTL). Pattern-based approach is accessible to engineers. Directly supports your claim about tractable synthesis. **Read pages 2-7.** + +**Luttenberger et al. 2020 — "Practical Synthesis via Parity Games" (Strix)** +Full LTL synthesis made practical via forward exploration and formula decomposition. Won SYNTCOMP 2018-2019. Handles 415/434 benchmark instances. Supports your choice of Strix but note: "specifications with large alphabets are still a challenge." **Read pages 1-12, 27-30.** + +### Barrier Certificates + +**Borrmann et al. 2015 — "Control Barrier Certificates for Safe Swarm Behavior"** +QP-based safety filter architecture: nominal controller + CBF override. Runs at 50Hz for 20 agents. Hand-crafted barriers from physics. Relevant architecture for stabilizing modes but barriers are NOT automatically synthesized. **Read pages 2-4.** + +**Papachristodoulou et al. 2021 — "SOSTOOLS v4.00"** +SOS optimization toolbox for barrier certificate search. Can handle ~10 variables at degree 4 polynomials. Provides formal certificates but limited to polynomial dynamics. Directly supports your stabilizing mode verification approach. **Read pages 6-10, 34-40.** + +### Reachability Analysis + +**Frehse et al. 2011 — "SpaceEx"** +Support function + template polyhedra for affine hybrid systems. Scales to 100+ dimensions for linear dynamics. Best scalability of the three tools. Limited to piecewise-affine dynamics. **Read pages 4-8, 13-15.** + +**Chen et al. 2013 — "Flow*"** +Taylor model flowpipes for nonlinear polynomial hybrid systems. Handles 4-9 variables. Only tool that does nonlinear dynamics directly. Parameter-sensitive. **Read pages 1-5.** + +**Bogomolov et al. 2019 — "JuliaReach"** +Julia-based toolbox with lazy set representations. Scales to 1000+ dimensions for linear systems. Designed for rapid prototyping and extensibility. Currently linear-only. **Read pages 1-4.** + +### Other + +**Hauswirth et al. 2024 — "Optimization Algorithms as Robust Feedback Controllers"** +Shows optimization algorithms (gradient descent, etc.) can be viewed as feedback controllers with robustness guarantees. Potentially relevant to your continuous controller design but tangential to verification. **Skim for ideas.** + +**Kapuria 2025 — Thesis on Decomposition-Based Formal Verification** +Could not fully analyze (>100 pages). Title suggests direct relevance to your compositional verification approach. **Request Dane read key chapters directly.** + +--- + +## 2. Supporting Evidence by Thesis Section + +### Section 1: Hybrid Systems Definition +- Your compositional approach (verify per-mode, compose) is standard in hybrid systems literature +- SpaceEx paper (p4-6) formalizes the hybrid automaton structure you use +- Flow* (p2) shows guard/reset handling matches your formulation + +### Section 2: Requirements & FRET +- **Strong support**: Katis 2022 (p3-5) shows exactly how FRETish → pmLTL works +- 160 distinct ⟨scope, condition, timing⟩ templates cover most requirement patterns +- Pressburger 2023 demonstrates iterative refinement catches specification gaps +- **Gap**: FRET has NO liveness support (Katis p2, Table 1) — your "eventually reach operating temperature" properties need workaround + +### Section 3: Reactive Synthesis +- **Strong support**: GR(1) paper shows 52/55 Dwyer patterns are tractable (polynomial time) +- Strix paper validates full LTL synthesis is now practical (415/434 benchmarks solved) +- Your claim "eliminates human error at implementation stage" is supported: synthesis is correct-by-construction +- **Caution**: Strix notes "large alphabets are still a challenge" (p35) — nuclear systems with many sensors may hit this + +### Section 4: Continuous Controllers + +#### Transitory Modes (Reachability) +- **Strong support**: SpaceEx handles 100+ dimensional affine systems +- JuliaReach scales to 1000D for lazy operations +- Flow* handles nonlinear polynomial dynamics (4-9 vars) +- **Gap**: None of these handle true nonlinear reactor kinetics (exponentials) without approximation + +#### Stabilizing Modes (Barrier Certificates) +- **Partial support**: SOSTOOLS can search for polynomial barrier certificates +- Your claim that "the barrier is known a priori from discrete specs" is novel — not directly validated by these papers +- Borrmann shows CBF architecture works but uses hand-crafted barriers +- **Gap**: No paper shows automatic barrier search from discrete boundary conditions + +#### Expulsory Modes (Robust Reachability) +- **Weak support**: SpaceEx handles nondeterministic inputs (p4) but not parametric uncertainty directly +- Flow* has some robustness via interval remainders +- **Gap**: None of these papers address reachability with parametric uncertainty for failure mode analysis + +--- + +## 3. Gaps & Challenges + +### Your Approach Claims These Papers DON'T Cover: + +1. **Three-mode taxonomy (transitory/stabilizing/expulsory)** + - This appears to be your novel contribution + - No paper uses this exact classification + - You need to justify why this taxonomy is complete (covers all cases) + +2. **Barrier certificates from discrete boundaries** + - Your claim that knowing entry/exit conditions "eliminates the barrier search problem" is not validated + - SOSTOOLS still requires searching for the barrier polynomial + - The discrete specs constrain the *domain* but not the *barrier function form* + +3. **Compositional verification soundness** + - You claim verifying per-mode and composing guarantees is sound + - This requires assume-guarantee reasoning at mode boundaries + - None of these papers prove this composition is sound for your specific approach + - **Suggest**: Cite Alur et al. or other assume-guarantee hybrid systems literature + +4. **FRET for nuclear operating procedures** + - No paper applies FRET to nuclear domain + - The Lift+Cruise study (aviation) is closest but nuclear procedures have different characteristics + - **Gap**: No evidence FRET's 160 templates cover nuclear procedure patterns + +5. **Expulsory mode verification** + - Parametric reachability under failure mode uncertainty is not well-covered + - You may need additional references (robust reachability, FMEA integration) + +--- + +## 4. Recommended Reading (Tomorrow Morning) + +### Priority 1 (Must Read) +| Paper | Pages | Why | +|-------|-------|-----| +| Katis 2022 (FRET Realizability) | 3-9 | Core FRET pipeline, directly supports your methodology | +| Maoz 2015 (GR(1) Patterns) | 2-7 | Tractability argument for reactive synthesis | +| Pressburger 2023 (FRET Case Study) | 5-11 | Real hybrid system example, lessons learned | + +### Priority 2 (Should Read) +| Paper | Pages | Why | +|-------|-------|-----| +| Luttenberger 2020 (Strix) | 1-12, 27-30 | Validates Strix as synthesis tool choice | +| SOSTOOLS manual | 34-40 | Lyapunov/barrier certificate computation | +| SpaceEx paper | 4-8 | Reachability algorithm details | + +### Priority 3 (Skim) +| Paper | Section | Why | +|-------|---------|-----| +| Borrmann 2015 (CBF) | Section 3 | CBF-QP architecture for safety filter | +| Flow* paper | Full | Nonlinear reachability capabilities | +| JuliaReach paper | Full | Modern tooling alternative | + +--- + +## 5. Missing References (Topics Not Covered) + +Your research approach mentions or assumes things these papers don't address: + +1. **Assume-guarantee reasoning for hybrid systems** + - Need citations for compositional verification soundness + - Suggested: Henzinger et al., Alur et al., or de Alfaro & Henzinger on interface theories + +2. **Nuclear-specific formal methods** + - HARDENS is your main reference but additional nuclear FM work may exist + - Search: NuSMV for nuclear, formal methods in safety-critical systems + +3. **Parametric reachability / robust verification** + - For expulsory mode verification with failure uncertainty + - Suggested: CORA (parametric reachability), robust CBF literature + +4. **Timed automata / real-time specifications** + - FRET timing is discrete ticks, not real-time + - If you need continuous-time deadlines, may need UPPAAL or timed automata references + +5. **Code generation from synthesized controllers** + - You mention compiling to Ovation hardware + - Need references on verified code generation from automata (e.g., Esterel, SCADE) + +6. **Mode-switching stability** + - Your stabilizing modes need to maintain stability across transitions + - Suggested: Multiple Lyapunov functions, dwell time conditions + +--- + +## 6. Key Quotes for Your Proposal + +**On reactive synthesis tractability:** +> "GR(1) synthesis is polynomial in the state space size... all 52 supported patterns have DBWs with at most 8 states, requiring at most 3 auxiliary variables per pattern instance." — Maoz & Ringert 2015, p6 + +**On FRET's value:** +> "Realizability checking catches specification conflicts early — before implementation. The Infusion Pump case shows how manual analysis missed the true conflict structure, while automated analysis found 8 minimal cores." — Katis 2022, p14 + +**On specification completeness:** +> "The most significant discovery was that initial requirements without 'stay' transitions were under-specified. Realizability analysis produced a trace where the aircraft jumped from wing-borne mode directly to thrust-borne mode — physically impossible but logically permitted." — Pressburger 2023, p9 + +**On scalability:** +> "SpaceEx demonstrates empirical complexity of O(n^2.7) for box directions... up to 198 variables using box directions." — Frehse 2011, p13 + +**On barrier certificates:** +> "SOSTOOLS can solve local nonlinear stability analysis with 10 variables using degree 4 polynomials." — Papachristodoulou 2021, p6 + +--- + +*Report generated by Split 🦎*