Track D: TSN/Ethernet WCTT analysis with first-class switch modeling

[avrabe]

Problem

spar's latency.rs traces thread chains end-to-end but uses a single scalar Bus_Properties::Latency per network hop — a placeholder, not a real bound. Real embedded systems alternate WCET (compute stages) and WCTT (communication stages):

```
sensor → [WCTT₁] → ECU_A → [WCET_a] → ECU_A → [WCTT₂] → ECU_B → [WCET_b] → … → actuator
```

Without per-stream WCTT, every network hop is undercounted at the latency analysis layer. This produces optimistic end-to-end bounds that miss real deadline misses on contended networks.

WCTT is not a TSN-only advanced feature — it's foundational for honest end-to-end timing. Classical Ethernet, CAN, FlexRay all need it. TSN-specific features (TAS gate-control, CBS, frame preemption) are upgrades within the WCTT engine, not separate concerns.

Today:

• `bus_bandwidth.rs` — summed throughput per bus, no per-stream WCTT
• `latency.rs` — thread chains with scalar bus latency
• AADL spec has no first-class switch component
• IEEE 802.1Qbv (TAS), 802.1Qbu (preemption), 802.1Qcr — no AADL vocabulary

Customer driver: vehicle E/E architectures gateway → switches → Cortex-M0 ECUs. Sensor-to-actuator latency claims must compose WCTT and WCET correctly.

Acceptance — phased

Phase 1 (v0.8.0): WCTT engine for FIFO+priority networks

• New crate `spar-network` hosting Network Calculus primitives (arrival/service curves, residual service)
• Switch components first-class via `bus implementation` + `Spar_Network::Switch_Type` discriminator (Option C from design: Track D research — TSN/Ethernet WCTT design space (#149) #152 research, AADL-spec-conformant)
• New analysis pass `wctt.rs` — per-stream end-to-end traversal-time bound across the device/bus graph
• `latency.rs` extended to source per-hop network latency from `wctt.rs` instead of scalar `Bus_Properties::Latency`
• Backward-compat: models without `spar-network` annotations get classical scalar latency (existing behavior)
• Lean theorems for min-plus algebra monotonicity (commits to `proofs/Proofs/Network/`); `sorry`-acceptable for v0.8.0
• Integration tests: classical Ethernet + FlexRay multi-hop topologies
• Rivet traceability for new requirements

Phase 2 (v0.8.x or v0.9.0): TSN extensions

• New property set `Spar_TSN::{Stream_ID, Class_of_Service, Gate_Control_List, Max_Frame_Size, Frame_Preemption}`
• Service curve generators for TAS-shaped, CBS-shaped, preemption-aware service
• Integration tests: TSN-shaped Ethernet topologies (gateway → 802.1Qbv switch → ECU)

Research output

PR #152 — comprehensive research and design proposal (1264 lines, 50 citations). Recommended:

• Option C for switch modeling (`bus impl` + `Spar_Network::Switch_Type`)
• spar's positioning: complementary primary, competitive stretch goal (mirrors RocqStat decision)
• ~7-week scope across 6 commits

A follow-up RTaW-Pegase deep-dive + extended commercial-tool survey is in progress to refine acceptance criteria further.

Notes

• Network Calculus computations can be expensive on large graphs — performance budget needed (target: ≤30s for 100-ECU topologies)
• `Stream_ID` semantics across redundant paths (802.1CB FRER) deferred beyond Phase 2
• Lean foundations for min-plus algebra are bigger than RTA — full proofs target v1.0.0
• ~7-week scope for Phase 1, comparable to Track A