Chapter 30 — Verification laboratory I
Lesson map
Lesson 30 published. Map, example, EX059.
flowchart TD
N0["Learning outcomes and connection"]
N1["30.1 Verification as a campaign"]
N2["30.2 Kinds of test"]
N3["30.3 Reproducibility"]
N4["30.4 Failed tests"]
N5["30.6 Practical activity: Lab 11"]
N6["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6
N6 --> EX["Worked example"]
EX --> Q["Exercise EX059"]
Logical drawing
flowchart LR
N0["Learning outcomes and connection"]
N1["30.1 Verification as a campaign"]
N2["30.2 Kinds of test"]
N3["30.3 Reproducibility"]
N4["30.4 Failed tests"]
N5["30.6 Practical activity: Lab 11"]
N6["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> Q["EX059"]
[Learning outcomes and connection]
|
v
[30.1 Verification as a campaign]
|
v
[30.2 Kinds of test]
|
v
[30.3 Reproducibility]
|
v
[30.4 Failed tests]
|
v
[30.6 Practical activity: Lab 11]
|
v
[Chapter synthesis]
|
v
[Worked example] --> [Exercise EX059]
Learning outcomes and connection
After this chapter you can (1) plan and run a verification campaign for security controls with defined pass/fail criteria; (2) use example-based, boundary, negative and property-based testing; (3) record results so another engineer can reproduce them; and (4) handle failed tests honestly, including re-test after fixes. It verifies Chapter 28's implementation and prepares Chapter 38 (validation) and Chapter 40 (Verification laboratory II).
30.1 Verification as a campaign
Verification answers: does the implementation meet its specification? A campaign plan lists, for each requirement, the test cases, environment, inputs, procedure, expected result, pass criterion and who runs it. Tests are written before execution and are not changed to make results pass. Results include environment details (software versions, seeds, configuration) so the test can be repeated.
TMRP's campaign plan lists T1 to T7 against R1 to R8, with pass criteria fixed before any test runs; R9 has no test assigned yet, which the evidence map later exposes. Each test names its environment and who runs it.
30.2 Kinds of test
- Example tests check typical behaviour.
- Boundary tests check edges: exactly at limits, just inside, just outside.
- Negative tests check that invalid input is rejected: malformed, forged, replayed, out of range.
- Property-based tests state a property that must hold for all inputs ("no unsafe setpoint is ever accepted") and check it on many generated inputs, including special values. They find cases no one thought to write.
- Fault-injection tests (Chapter 40) perturb the environment: drop, delay or corrupt messages; restart components.
Example tests show the presence of correct behaviour in chosen cases; property-based and fault-injection tests search for the absence of incorrect behaviour more broadly. None proves correctness for all inputs except in small finite domains (Chapter 2).
30.3 Reproducibility
Seed every random generator and print the seed; record tool and library versions; keep the test inputs; store results with the source revision. A failed test that cannot be reproduced cannot be fixed or re-verified.
TMRP's T3 record follows this rule: it gives the seed, the number of generated cases and the Python version, so anyone can rerun the property-based test and see the same thirty-one NaN acceptances on v1 and none on v2. Without the seed, a reviewer could only take the result on trust. The same record stores the source revision of each validator version.
30.4 Failed tests
A failed test is information. Record it as failed with evidence; analyse root cause; fix; re-run the failed test and the regression suite; record the re-test. Never re-label a failure as "not applicable" because the deadline is close (Chapter 10). If a failure is accepted temporarily, it needs a compensating control, an owner and a date.
T3 is the model: failed on v1, fixed in v2, re-tested and recorded. The v1 failure was never relabelled, and the PS4 compensating control had an owner and a date.
30.5 Worked example: T3 setpoint bounds (synthetic)
Test T3 verifies R3. Example tests on v1 (in range, above, below, large step) pass. The property-based test generates 2,000 cases with seed 30, one in ten drawn from special values (NaN, ±∞, exact boundaries). v1 accepts 31 unsafe values — all NaN. v2 accepts none. T3 is recorded as failed on v1, root cause "negative comparisons are false for NaN", fixed in v2, re-tested and passed on v2, with the seed and Python version recorded.
Both results stay in the record. The re-test result is later entered in the traceability matrix.
30.6 Practical activity: Lab 11
# Lab 11 - property-based testing of a setpoint validator finds what example tests missed (offline)
import random, math
def validate_v1(new, old, lo=0.5, hi=5.5, max_step=0.5):
if new < lo: return False
if new > hi: return False
if abs(new - old) > max_step: return False
return True
def validate_v2(new, old, lo=0.5, hi=5.5, max_step=0.5):
if not (isinstance(new, float) and math.isfinite(new)): return False
return lo <= new <= hi and abs(new - old) <= max_step
examples = [(3.0, 3.2), (6.0, 5.8), (0.2, 0.6), (4.0, 3.0)]
print("example tests v1:", [validate_v1(n, o) for n, o in examples])
rng = random.Random(30)
specials = [float("nan"), float("inf"), -float("inf"), 5.5, 0.5]
def prop(f, trials=2000):
fails = []
for i in range(trials):
old = rng.uniform(0.5, 5.5)
new = rng.choice(specials) if i % 10 == 0 else rng.uniform(-1, 7)
ok = f(new, old)
safe = math.isfinite(new) and 0.5 <= new <= 5.5 and abs(new - old) <= 0.5
if ok and not safe: fails.append(new)
return fails
f1 = prop(validate_v1); f2 = prop(validate_v2)
print("v1 unsafe acceptances:", len(f1), "first:", f1[:1])
print("v2 unsafe acceptances:", len(f2))
Expected output:
example tests v1: [True, False, False, False]
v1 unsafe acceptances: 31 first: [nan]
v2 unsafe acceptances: 0
The example tests give the same answers for both validators, so they cannot tell v1 from v2. The property-based run is what separates them: v1 accepts thirty-one unsafe values, all NaN, while v2 accepts none. The seed of thirty makes the run repeatable. Notice that the generator draws special values only one time in ten; without that, NaN would almost never appear and the bug would stay hidden however many random cases were tried. Record the seed with the result.
30.7 Common errors and limits
- Tests written after seeing results.
- Example tests only.
- Unseeded random tests; results without versions.
- Failures re-labelled instead of fixed.
- Claiming property-based tests prove correctness.
TMRP's T3 record avoids each of these. Its property was written before the run, its generator is seeded, the failure on v1 stayed recorded as failed, and the report claims only that no unsafe value was found among the generated cases, not that v2 is correct for every input. The seed and version are stored with the result.
Exercises — chapter 30
EX059 — Count the failures. Objective: reason about generated tests. Inputs: Lab 11. Steps: (1) explain why all 31 unsafe acceptances are NaN; (2) estimate how many NaN cases the generator produced (one in ten cases are special values, chosen uniformly from five) and compare with 31; (3) explain why not every NaN case is an unsafe acceptance in v1 — or show that every NaN is accepted. Expected evidence: reasoning and numbers. Rubric: 3 = ≈ 200 special cases × 1/5 ≈ 40 expected NaN, 31 observed consistent with random variation, and every NaN is accepted by v1 so 31 is the NaN count; 2 = partial; 1 = no numbers; 0 = none.
EX060 — Verification plan for R2. Objective: plan tests for replay rejection. Inputs: R2 and Lab 8. Steps: write a test plan with at least six cases (including restart of each side, counter wrap or maximum, out-of-order delivery), expected results and pass criteria. Expected evidence: table. Rubric: 3 = cases cover restart and ordering, expected results consistent with the design in §19.5, criteria unambiguous; 2 = restart missed; 1 = happy path only; 0 = none.
Chapter synthesis
Verification is a planned campaign with criteria fixed in advance. Combine example, boundary, negative, property-based and fault-injection tests; make every run reproducible; and treat failures as information to be fixed and re-verified, never relabelled.
Continue studying — chapter 30 of 50
← Chapter 29 · Course chapter index · Chapter 31 →
Continue to the next authored lesson.