design: Track D research — TSN/Ethernet WCTT design space (#149)

[avrabe]

Summary

Research-and-design report for #149 — TSN/Ethernet WCTT analysis with first-class switch modelling. No production code changes; the implementation lands as separate PRs.

The report (docs/designs/track-d-tsn-wctt-research.md, ~1260 lines, ~50 inline citations) covers seven axes:

1. IEEE 802.1Q TSN amendment landscape — Qbv, Qbu, Qci, Qch, Qcr, Qcc, CB, AS, DG, Qdj — what each adds, when it matters for vehicle E/E, and what math an analyser needs. 802.1DG-2025 is the recommended anchor for spar's first iteration.
2. Network Calculus tooling survey — RTC Toolbox (dormant), DiscoDNC / NetCal-DNC (LGPL, slow but active oracle), NCBounds (dormant), WoPANets (closed), RTaW-Pegase (commercial benchmark target), Capital/Volcano (workflow ref). No Rust NC port exists; spar would be first.
3. AADL research extensions — Phan/Lee/Sokolsky 2010 (AADL→RTC), Lauer/Pagetti/Boniol on AFDX, FORA fog-platform property sets (closest prior art), and the Boyer/Maia ECRTS 2022 RTA↔NC formal link.
4. Math foundations — min-plus algebra primer, the four core bounds, TSN-specific service curves (CBS, TAS, Qbu, CQF, ATS), tightness ordering TFA ≤ SFA ≤ PMOO ≤ LUDB.
5. spar design space across 7 sub-axes:
   • 5.1 Spar_TSN::* and Spar_Network::* property sets with full AADL example.
   • 5.2 Switch modelling — recommends Option C: bus implementation with Spar_Network::Switch_Type discriminator. Spec-conformant, no grammar change.
   • 5.3 Recommends a new spar-network crate (mirrors spar-solver layering).
   • 5.4 wctt.rs algorithm sketch — graph extraction → arrival/service curves → TFA pass with petgraph toposort.
   • 5.5 Lean theorems — algebraic foundations (~450 lines) full in v0.8.0; headline bounds with sorry, full proofs in v0.9.0/v1.0.0.
   • 5.6 Backward-compat: bus_bandwidth.rs untouched; latency.rs consumes WCTT cache when Stream_ID is present, falls back otherwise.
   • 5.7 Performance budget — TFA on 100 ECUs / 200 streams / 10 switches ≈ 100 ms wall time.
6. Roadmap — 6 commits (~7 weeks elapsed) with explicit dependencies on PR feat(timing): Spar_Timing + Spar_Trace property sets (Track A foundation) (v0.7.0) #145 (timing properties) and PR docs: rivet <-> spar variant binding contract v1 (proposed) #144 (rivet binding).
7. Risks & open questions — modal-switching transients, FRER cycles, strict-vs-aggregate service curves, fixed-point arithmetic to keep Rust ↔ Lean in lockstep.

The final section refines #149's acceptance criteria based on the research.

Recommendations (TL;DR)

• Switch modelling: Option C — bus + Switch_Type discriminator
• Crate: new spar-network — clean separation of NC math from AADL analysis
• Analysis: TFA in v0.8.0, SFA in v0.9.0, PMOO/LP only if user demand
• Lean: ship algebraic foundations fully proved, headline bounds with sorry
• Effort: ~7 weeks elapsed for v0.8.0 (slightly larger than Track A)

Test plan

• Two reviewers (one on TSN standards, one on AADL/spar internals) sign off on Section 5 recommendations
• Decision logged on the five questions in Section 7.1 (TAS scope, CBS scope, FRER scope, accuracy target, Lean appetite) before implementation starts
• Section 6.1 commit decomposition adopted as the v0.8.0 plan or revised in writing
• Issue Track D: TSN/Ethernet WCTT analysis with first-class switch modeling #149 acceptance list updated to match Section 8

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!