Module 9: Verification & Validation

SysML v2 verification and validation modelling is built on KerML’s Case and Requirement infrastructure. A verification case def is a specialised CaseDefinition at the KerML level, inheriting the ability to have an objective, a subject, and a structured body of actions. The verify requirement relationship maps to a RequirementVerification dependency that tools can trace automatically.

A verification case definition is a reusable template for a test. It declares what is being tested (subject), what the test aims to prove (objective), and what steps the test performs (the action body). The verdict is the return value of the case.

Basic structure

Every verification case follows a three-part pattern: subject, objective, and body.

1
verification case def CheckTemperatureRange {
2
    subject sut : TemperatureSensor;
3

4
    objective {
5
        verify requirement SensorAccuracyReq;
6
    }
7

8
    action stimulate : ApplyTemperature {
9
        in  temperature = 85[degC];
10
    }
11

12
    action measure : ReadSensorOutput {
13
        in  sensor = sut;
14
        out reading : Real;
15
    }
16

17
    first stimulate then measure;
18

19
    return verdict : VerdictKind =
20
        if measure.reading >= 84.5 and measure.reading <= 85.5
21
            then VerdictKind::pass
22
            else VerdictKind::fail;
23
}

A verification case that stimulates a sensor, reads its output, and returns a pass/fail verdict.

Composing verification cases

Because verification cases are actions, you can compose them using the same sequencing and concurrency mechanisms from Module 4. A parent verification case can invoke child cases as sub-actions:

1
verification case def FullSensorSuite {
2
    subject sut : TemperatureSensor;
3

4
    action rangeCheck  : CheckTemperatureRange  { subject = sut; }
5
    action driftCheck  : CheckSensorDrift       { subject = sut; }
6
    action latencyTest : CheckResponseLatency   { subject = sut; }
7

8
    first rangeCheck then driftCheck then latencyTest;
9
}

The objective and subject are the two structural pillars of every verification case. Together they answer: what are we testing? (subject) and what must we prove? (objective).

The objective block

An objective is a requirement usage nested inside the verification case. It can contain one or more verify requirement references and additional constraints. The objective gives tools a machine-readable declaration of the test’s purpose:

1
verification case def BrakeResponseTest {
2
    subject sut : BrakingSubsystem;
3

4
    objective {
5
        verify requirement BrakeStoppingDistanceReq;
6
        verify requirement BrakeResponseTimeReq;
7
        require constraint {
8
            doc /* Both requirements must pass simultaneously */
9
        }
10
    }
11
}

Subject binding

The subject keyword declares the system under test (SUT). It is a directed feature — an in parameter that refers to the element being verified. When the verification case is instantiated, the subject is bound to a concrete part usage:

1
part vehicle : Vehicle {
2
    part brakes : BrakingSubsystem;
3
}
4

5
// Instantiate a verification case, binding subject to a real part
6
verification case brakeTest : BrakeResponseTest {
7
    subject = vehicle.brakes;
8
}

The verify requirement relationship is the backbone of V&V traceability in SysML v2. It creates a formal, tool-traversable link between a verification case and one or more requirements.

verify vs. satisfy

SysML v2 distinguishes two relationships between design elements and requirements:

• assert satisfy requirement — declares that a design element (a part, action, or constraint) meets a requirement by construction. This is a design-time assertion.
• verify requirement — declares that a verification case demonstrates whether the requirement is met through testing, analysis, or inspection. This is a V&V-time assertion.

1
requirement def StoppingDistance {
2
    doc /* The vehicle shall stop within 40m from 100 km/h */
3
    subject vehicle : Vehicle;
4
    require constraint {
5
        vehicle.stoppingDistance <= 40[m]
6
    }
7
}
8

9
// Design satisfies the requirement
10
part def BrakingSubsystem {
11
    assert satisfy requirement StoppingDistance;
12
}
13

14
// Verification case verifies the requirement
15
verification case def BrakeStopTest {
16
    subject sut : BrakingSubsystem;
17
    objective {
18
        verify requirement StoppingDistance;
19
    }
20
}

Traceability matrices

Because verify requirement is a first-class model element (not a comment or tag), tools can automatically generate requirements traceability matrices (RTMs). Every requirement is linked to zero or more verification cases, and every verification case declares which requirements it covers. Gaps in coverage — requirements with no verification case — are detectable by model queries.

Systems engineering traditionally recognises four verification methods: Test, Analysis, Inspection, and Demonstration (TAID). SysML v2 does not prescribe special keywords for each method, but the language provides natural patterns for modelling all four.

Test

A test involves exercising the SUT with controlled inputs and measuring outputs. This is the most common verification case pattern — the examples throughout this module are test cases:

1
verification case def PedalForceTest {
2
    subject sut : BrakePedal;
3
    objective { verify requirement MaxPedalForceReq; }
4

5
    action applyForce : ApplyPedalForce { in force = 500[N]; }
6
    action readDisplacement : MeasureDisplacement { out travel : Real; }
7
    first applyForce then readDisplacement;
8

9
    return verdict : VerdictKind =
10
        if readDisplacement.travel >= 10[mm]
11
            then VerdictKind::pass else VerdictKind::fail;
12
}

Analysis

Analysis uses calculation or simulation rather than physical testing. In SysML v2 you can model this by embedding an analysis case (from Module 7) inside a verification case:

1
verification case def ThermalAnalysisVerification {
2
    subject sut : ElectronicEnclosure;
3
    objective { verify requirement MaxOperatingTempReq; }
4

5
    action runAnalysis : ThermalAnalysisCase {
6
        in  ambientTemp = 55[degC];
7
        out peakTemp : Real;
8
    }
9

10
    return verdict : VerdictKind =
11
        if runAnalysis.peakTemp <= 85[degC]
12
            then VerdictKind::pass else VerdictKind::fail;
13
}

Inspection

Inspection verifies a requirement by examining the design artefact itself — reviewing drawings, checking part numbers, or confirming labelling. In SysML v2, an inspection case typically has no stimulus action; it queries attributes directly:

1
verification case def LabelInspection {
2
    subject sut : ControlPanel;
3
    objective { verify requirement LabellingStandardReq; }
4

5
    return verdict : VerdictKind =
6
        if sut.hasLabel and sut.labelLanguage == "EN"
7
            then VerdictKind::pass else VerdictKind::fail;
8
}

Demonstration

Demonstration verifies by operating the system under realistic conditions and observing its behaviour. The verification case body sequences real-world scenario actions rather than isolated stimulus-response pairs:

1
verification case def EmergencyStopDemo {
2
    subject sut : Vehicle;
3
    objective { verify requirement EmergencyStopReq; }
4

5
    action driveAtSpeed  : DriveVehicle { in speed = 60[km/h]; }
6
    action triggerEStop  : ActivateEmergencyBrake;
7
    action observeResult : RecordStopBehaviour {
8
        out stoppedSafely : Boolean;
9
    }
10

11
    first driveAtSpeed then triggerEStop then observeResult;
12

13
    return verdict : VerdictKind =
14
        if observeResult.stoppedSafely
15
            then VerdictKind::pass else VerdictKind::fail;
16
}

The V-model is the standard systems engineering lifecycle shape. The left side decomposes stakeholder needs into requirements and design; the right side integrates and verifies back upwards. SysML v2’s verification constructs map directly onto the right side of the V.

Left side: requirements to design

Modules 1–7 of this series covered the left side of the V:

• Stakeholder needs → requirement def with require constraint (Module 5)
• System requirements → decomposed requirements with subject bindings
• Architecture → part def, port def, connection def (Module 3)
• Detailed design → action def, state def, analysis case def (Modules 4, 7)

Each level is linked to the one above through assert satisfy requirement relationships and specialisation hierarchies.

Right side: verification to validation

The right side mirrors the left. For every level of decomposition, there is a corresponding verification level:

• Unit verification → verification cases targeting individual part attributes or actions
• Integration verification → verification cases targeting assembled subsystems with connected ports
• System verification → verification cases targeting top-level system requirements
• Validation → verification cases with stakeholder-facing objectives (does the system solve the original problem?)

1
package VModelTraceability {
2
    // Left side: requirements hierarchy
3
    requirement def StakeholderNeed {
4
        doc /* Vehicle shall be safe to operate */
5
    }
6
    requirement def SystemReq :> StakeholderNeed {
7
        doc /* Braking system shall stop within 40m from 100 km/h */
8
        subject vehicle : Vehicle;
9
    }
10
    requirement def SubsystemReq :> SystemReq {
11
        doc /* Brake caliper shall apply >= 15kN clamping force */
12
        subject caliper : BrakeCaliper;
13
    }
14

15
    // Right side: verification hierarchy
16
    verification case def UnitTest_Caliper {
17
        subject sut : BrakeCaliper;
18
        objective { verify requirement SubsystemReq; }
19
    }
20
    verification case def SystemTest_Braking {
21
        subject sut : Vehicle;
22
        objective { verify requirement SystemReq; }
23
    }
24
    verification case def Validation_Safety {
25
        subject sut : Vehicle;
26
        objective { verify requirement StakeholderNeed; }
27
    }
28
}

A requirements hierarchy (left V) mirrored by a verification hierarchy (right V), with traceability at each level.

This example models a complete verification campaign for an automotive braking system. It references requirements from Module 5, structural parts from Module 3, and behavioural actions from Module 4. The package demonstrates all core V&V patterns: verification case definitions, subject binding, objective declaration, verdict evaluation, multiple verification methods, and V-model traceability.

1
package BrakingVerification {
2
    private import ISQ::*;
3
    private import SI::*;
4
    private import ScalarValues::*;
5
    private import VerificationCases::*;
6

7
    // ── Requirements (from Module 5) ────────────────────────
8
    requirement def StoppingDistanceReq {
9
        doc /* The vehicle shall stop within 40 m from 100 km/h
10
              on dry pavement (friction coefficient >= 0.7). */
11
        subject vehicle : Vehicle;
12
        require constraint {
13
            vehicle.stoppingDistance <= 40[m]
14
        }
15
    }
16

17
    requirement def BrakeResponseTimeReq {
18
        doc /* Brake actuation shall begin within 150 ms
19
              of pedal input exceeding 50 N. */
20
        subject brakes : BrakingSubsystem;
21
        require constraint {
22
            brakes.responseTime <= 150[ms]
23
        }
24
    }
25

26
    requirement def PedalForceReq {
27
        doc /* Maximum pedal force shall not exceed 500 N. */
28
        subject pedal : BrakePedal;
29
        require constraint {
30
            pedal.maxForce <= 500[N]
31
        }
32
    }
33

34
    requirement def ABSActivationReq {
35
        doc /* ABS shall activate when wheel slip exceeds 15%. */
36
        subject abs : ABSController;
37
        require constraint {
38
            abs.activationThreshold == 0.15
39
        }
40
    }
41

42
    // ── Verification case 1: Stopping distance (Test) ───────
43
    verification case def StoppingDistanceTest {
44
        subject sut : Vehicle;
45

46
        objective {
47
            verify requirement StoppingDistanceReq;
48
        }
49

50
        action accelerate : AccelerateToSpeed {
51
            in targetSpeed = 100[km/h];
52
        }
53
        action applyBrakes : FullBrakeApplication;
54
        action measureDist : MeasureStoppingDistance {
55
            out distance : LengthValue;
56
        }
57

58
        first accelerate then applyBrakes then measureDist;
59

60
        return verdict : VerdictKind =
61
            if measureDist.distance <= 40[m]
62
                then VerdictKind::pass else VerdictKind::fail;
63
    }
64

65
    // ── Verification case 2: Response time (Analysis) ───────
66
    verification case def ResponseTimeAnalysis {
67
        subject sut : BrakingSubsystem;
68

69
        objective {
70
            verify requirement BrakeResponseTimeReq;
71
        }
72

73
        action simulate : HydraulicResponseSimulation {
74
            in  pedalForce = 80[N];
75
            out latency : TimeValue;
76
        }
77

78
        return verdict : VerdictKind =
79
            if simulate.latency <= 150[ms]
80
                then VerdictKind::pass else VerdictKind::fail;
81
    }
82

83
    // ── Verification case 3: Pedal force (Inspection) ───────
84
    verification case def PedalForceInspection {
85
        subject sut : BrakePedal;
86

87
        objective {
88
            verify requirement PedalForceReq;
89
        }
90

91
        return verdict : VerdictKind =
92
            if sut.ratedMaxForce <= 500[N]
93
                then VerdictKind::pass else VerdictKind::fail;
94
    }
95

96
    // ── Verification case 4: ABS activation (Demonstration) ─
97
    verification case def ABSActivationDemo {
98
        subject sut : Vehicle;
99

100
        objective {
101
            verify requirement ABSActivationReq;
102
        }
103

104
        action driveOnWetSurface : DriveVehicle {
105
            in speed = 80[km/h];
106
            in surfaceFriction = 0.4;
107
        }
108
        action hardBrake : FullBrakeApplication;
109
        action checkABS : ObserveABSBehaviour {
110
            out absActivated : Boolean;
111
        }
112

113
        first driveOnWetSurface then hardBrake then checkABS;
114

115
        return verdict : VerdictKind =
116
            if checkABS.absActivated
117
                then VerdictKind::pass else VerdictKind::fail;
118
    }
119

120
    // ── Composite test campaign ──────────────────────────────
121
    verification case def BrakingSystemCampaign {
122
        subject sut : Vehicle;
123

124
        objective {
125
            verify requirement StoppingDistanceReq;
126
            verify requirement BrakeResponseTimeReq;
127
            verify requirement PedalForceReq;
128
            verify requirement ABSActivationReq;
129
        }
130

131
        action test1 : StoppingDistanceTest  { subject = sut; }
132
        action test2 : ResponseTimeAnalysis   { subject = sut.brakes; }
133
        action test3 : PedalForceInspection   { subject = sut.brakes.pedal; }
134
        action test4 : ABSActivationDemo      { subject = sut; }
135

136
        // Run inspection first, then analysis, then physical tests
137
        first test3 then test2 then test1 then test4;
138
    }
139
}

This model demonstrates: verification case def with subject and objective, verify requirement traceability, all four TAID verification methods (test, analysis, inspection, demonstration), verdict evaluation with pass/fail logic, and a composite test campaign that sequences individual verification cases.