FPF Reference

C.3.A:B.5 LA lane — tests & monitoring that cover the right variants [A/I]

Preface node heading:c-3-a-b-5-la-lane-tests-monitoring-that-cover-the-right-variants-a-i:34340

Content

What LA contributes. Empirical assurance for claims with executable semantics or physical interfaces; especially when F ≤ F6 or when stochastic/real‑world effects matter.

LA‑patterns (informative):

  • Cover by subkind. Test at least one representative per subkind; add more where variability inside a subkind matters.
  • Boundary probing. Concentrate tests near KindSignature and Scope boundaries (e.g., temp limits, speed caps).
  • Hybrid checks (F6). When software controllers interact with physical systems, ensure both sides declare obligations; include their interaction cases in the matrix.
  • Monitoring windows. For live systems, define Γ_time policies (e.g., rolling 30 d) and tie alerts to kind‑aware metrics (“error rate per ServiceInstance”).

LA‑obligations (normative):

  • LA‑1. Each test campaign SHALL specify rows/columns in the evidence matrix and attach Scope/MemberOf predicates to each run.
  • LA‑2. Freshness windows SHALL be explicit and enforced in guards (no “latest”).
  • LA‑3. If a KindBridge merges subkinds, test plans SHALL be adjusted (more cells, stricter acceptance), and the kind‑bridge penalty (based on CL^k) applied to R.
  • LA‑4. Publishing SpanUnion coverage requires the independence note (which support lines differ).

Mini‑example (LA). Claim: “For all x ∈ Vehicle: brakeDistance ≤ 50 m on dry, ≤ 40 m on wet.” — Rows: {PassengerCar, LightTruck}. — Columns: {dry, ≤50}, {wet, ≤40} with rigs and versions. — Cells: PC/dry covered by track tests; LT/wet by simulation + surrogate tests (independent lines → SpanUnion allowed). — Bridge to jurisdiction Y collapses EV vs ICE ⇒ CL^k=2. Apply Ψ(2) to R; add extra wet tests to compensate.