15-EFT.WP.Methods.Falsification v1.0 | Chapter 5: Test-Case Design & Coverage for Falsification

Home ／ Docs-Technical WhitePaper ／ 15-EFT.WP.Methods.Falsification v1.0

Chapter 5: Test-Case Design & Coverage for Falsification

I. Scope & Objectives

1. Present a falsification-oriented test design methodology centered on property assertions and metamorphic relations, spanning combinatorial coverage, boundary values, mutant generation, and kill-rate evaluation. All artifacts are reproducible and auditable under EnvLock and the shared time base ts = alpha + beta * tau_mono, yielding a verifiable TestPlan and a signed evidence bundle.
2. Pass criteria
   • Specification coverage: cov_spec ≥ tau_cov
   • Test-case coverage: cov_case ≥ tau_case
   • Mutant kill-rate: kill_rate ≥ tau_kill
   • All statistical tests pass with FDR or FWER control (see Chapter 3 S52-*).
   • Online gating linkage: GateDecision ∈ {pass, hold, block} is determined by a joint function of cov_spec, kill_rate, TS.error, and a risk-weighted score.

II. Terms & Symbols

• Properties & assertions: P(x) (property predicate), forall x in D: P(x) (universal assertion), Oracle(x, y_hat) (adjudicator), violation(x) ∈ {0,1}.
• Metamorphic relations: MR_k: X → X, invariant Inv_k(•), and x_prime = MR_k(x).
• Coverage & sets: C_total (set of spec units to cover), C_hit (hit set), cov_spec = ( |C_hit| / |C_total| ); test-case coverage cov_case = ( |T_executed| / |T_planned| ).
• Combinatorics & boundaries: factor set F = {f_1,...,f_m}, domains V_i; covering array CA(t, F) guarantees every t-wise value combination appears in at least one test; boundary set B = {B_j}, with Boundary(B_j) a decision or physical boundary.
• Mutation & killing: mut_i (mutant), mut_killed (killed set), kill_rate = ( |mut_killed| / |mut_all| ).

III. Postulates & Minimal Equations

• P51-6 (Monotonic evidence postulate)
  With TestPlan semantics and EnvLock fixed, adding valid tests never reduces coverage or kill-rate:
  cov_spec(t+1) ≥ cov_spec(t), kill_rate(t+1) ≥ kill_rate(t).
• P51-7 (Decidability & composability)
  For a composite assertion P = P_a ∧ P_b ∧ ..., falsification may be realized by the union of constituent violations:
  violation_P(x) = max( violation_{P_a}(x), violation_{P_b}(x), ... ).
• S52-8 (MR–property conservation & violation test)
  For any MR_k and invariant Inv_k, define
  Oracle_mr(x) = [ Inv_k(x) = Inv_k( MR_k(x) ) ];
  if Oracle_mr(x) = false, record a violation and include it in falsification statistics.
• S52-9 (t-wise covering array objective)
  Let CA(t, F) be a minimal test set such that every t-factor value combination appears at least once. For t=2 (pairwise), aim to minimize |CA(t,F)| while achieving cov_spec = 1 over the t-wise combination domain.
• S52-10 (Mutant sufficiency & confidence interval)
  kill_rate = ( |mut_killed| / |mut_all| ). Construct a (1 - delta) CI via bootstrap, or use the binomial approximation
  CI = kill_rate ± z_{1-delta/2} * sqrt( ( kill_rate * ( 1 - kill_rate ) ) / |mut_all| ).
• S52-11 (Test prioritization score)
  score(t) = w_risk * risk(t) + w_cost * ( 1 / cost(t) ) + w_cov * Δcov(t) + w_kill * E[ kill | t ],
  with weights satisfying w_risk + w_cost + w_cov + w_kill = 1. Execute tests in descending score(t).
• S52-12 (Boundary triplet minimization)
  For each Boundary(B_j), sample at least three points to straddle the boundary:
  x_left = argmin_{x ∈ B_j^-} dist(x, B_j), x_on ∈ B_j, x_right = argmin_{x ∈ B_j^+} dist(x, B_j), ensuring cross-boundary behavior is decidable.

IV. Data & Manifest Conventions

• TestPlan.card (minimum fields)
  id, version, purpose, scope, factors F and V_i, t_coverage, BoundarySet B, MR_set, MutatorSet, OracleSpec, risk_model, weights{w_risk,w_cost,w_cov,w_kill}, alpha/beta, FDR|FWER policy, ts_map{alpha,beta}, EnvLock, anchor.
• MR.card
  { id, Inv_k, transform, domain, constraints, examples[{x, x_prime}] } — all transform entries must pass check_dim(expr).
• Mutator.card
  { id, operator, granularity, seed, limits, compatibility }, plus an explicit compatibility matrix for model/data channels.

V. Algorithms & Implementation Bindings

1. Interface extensions (building on I50-*)
   • I50-20 design_test_plan(spec:dict) -> TestPlan (synthesizes CA(t,F), boundary points, and MR compositions)
   • I50-21 prioritize_tests(plan:TestPlan, telemetry:any) -> OrderedSuite
   • I50-22 evaluate_kill_rate(suite:any, mutants:any) -> {kill_rate:float, ci:list}
   • I50-23 generate_pairwise(F:list, V:list, t:int) -> Cases
   • I50-24 generate_boundary_cases(B:list) -> Cases
   • I50-25 weave_mr_cases(D:any, MR_set:list) -> Cases
   • I50-26 measure_spec_coverage(logs:any, C_total:set) -> {cov_spec:float, C_hit:set}
2. Pseudocode (test-generation skeleton)
   • plan ← design_test_plan(spec)
   • cases_pair ← generate_pairwise(F, V, t)
   • cases_boundary ← generate_boundary_cases(B)
   • cases_mr ← weave_mr_cases(D_seed, MR_set)
   • suite ← merge_dedup( cases_pair ∪ cases_boundary ∪ cases_mr )
   • suite_ordered ← prioritize_tests(plan, telemetry)
   • Execute & log: logs ← run(suite_ordered, OracleSpec)
   • cov ← measure_spec_coverage(logs, C_total); kill ← evaluate_kill_rate(suite_ordered, mutants)

VI. Metrology Flows & Run Diagram

• Mx-59 Test design & review
  Auto-synthesize CA(t,F) and boundary points from TestPlan.card; human-review MR.card for physical feasibility and dimensional consistency; audit OracleSpec for ambiguity.
• Mx-5A Execution & online observability
  Execute the suite in batch/streaming; collect TS.latency/TS.error, incremental Δcov(t), and online violation streams; trigger degradation or blocking on anomaly.
• Mx-5B Kill-rate & power evaluation
  Compute kill_rate, its CI, and estimated power from mutants and execution logs; if power < 1 - beta, backfill tests in high-value regions.
• Mx-5C Gating & rollback
  Decide GateDecision via score_release = g( cov_spec, kill_rate, TS.error ) against pre-registered thresholds; on failure, roll back to the prior anchor and open a regression task.

VII. Verification & Test Matrix

1. Minimum required set
   • t=2 combinational coverage: cov_spec(t=2) = 1.
   • Boundary triplets: cover {left, on, right} for all B_j.
   • MR sampling: each MR_k in MR_set is hit at least N_mr_min times.
2. Killing & power
   • kill_rate ≥ tau_kill with CI lower bound ≥ tau_kill_min.
   • Using target effect_size, compute sample size to ensure power ≥ 1 - beta.
3. Multiple testing & error control
   All assertion tests enter a unified gatekeeping program controlling FDR ≤ q_star or FWER ≤ alpha_family.
4. Consistency & replay
   Replay 3×: relative differences in cov_spec and kill_rate ≤ tau_cv; offline/online delta satisfies delta_offon ≤ tau_offon.

VIII. Cross-References & Dependencies

• Depends on: Core.DataSpec (fields & dimensions), Core.Metrology (coverage, confidence, windowing), Core.Errors (exceptions & alerting), Core.Threads (orchestration & resources).
• Cross-links: EFT.WP.Methods.Falsification Chapters 3 (postulates & tests), 4 (sample families & adversarial conventions), 9 (online gating); EFT.WP.Methods.Inference Chapter 7 (uncertainty & calibration).

IX. Risks, Limitations & Open Questions

• Risks & limitations
  Oracle ambiguity yields false positives/negatives; non-physical MR_k induce spurious violations; coverage metrics may decouple from real risk; mutant equivalence inflates kill_rate; resource ceilings can elevate TS.latency.
• Open questions
  Adaptive covering arrays driven by online feedback (CA(t,F) updates); verifiability of generative MR_k; multi-domain sharing and quotas for C_total.

X. Deliverables & Versioning

• Deliverables
  TestPlan.card, MR.card, Mutator.card, CA_matrix.csv, Boundary.cases.csv, Suite.index.json, Coverage.report, KillRate.report, GateDecision.log, anchor.sig.
• Versioning policy
  Changing F/V/t, MR_set, MutatorSet, OracleSpec, or threshold weights increments minor; changing the risk model or gating policy increments major. All changes require re-signature and updates to fingerprint and anchor.