模块 9：验证与确认

SysML v2 的验证与确认建模建立在 KerML 的用例（Case）与需求（Requirement）机制之上。在 KerML 层面，verification def 是特化的 CaseDefinition，因而继承了拥有目标、主题以及结构化动作主体的能力。verify requirement 关系映射到 RequirementVerification 依赖，工具可以自动对其进行追溯。

验证用例定义是一个可复用的测试模板。它声明被测的是什么（subject）、测试要证明什么（objective），以及测试执行哪些步骤（动作主体）。判定结论（verdict）就是该用例的返回值。

基本结构

每个验证用例都遵循三段式：主题、目标与主体。

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

4
    objective {
5
        verify requirement : SensorAccuracyReq;
6
    }
7

8
    action stimulate : ApplyTemperature {
9
        in  temperature = 358.15[K];  // 85 °C
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
            ? VerdictKind::pass
22
            else VerdictKind::fail;
23
}

一个验证用例：给传感器施加激励、读取其输出，并返回通过 / 失败的判定结论。

组合验证用例

由于验证用例本身就是动作，你可以用模块 4 中相同的顺序与并发机制来组合它们。父验证用例可以把子用例作为子动作调用：

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

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

8
    first rangeCheck; then driftCheck; then latencyTest;
9
}

objective 与 subject 是每个验证用例的两根结构支柱。二者共同回答：我们在测什么？（主题）以及我们必须证明什么？（目标）。

objective 块

objective 是嵌套在验证用例内部的一个需求使用。它可以包含一条或多条 verify requirement 引用以及额外的约束。目标为工具提供了对测试意图的机器可读声明：

1
verification 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 关键字声明被测系统（SUT）。它是一个带方向的特征 — 一个指向被验证元素的 in 参数。当验证用例被实例化时，主题就被绑定到某个具体的零件使用上：

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

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

verify requirement 关系是 SysML v2 中 V&V 可追溯性的主干。它在验证用例与一条或多条需求之间建立形式化、可被工具遍历的链接。

verify 与 satisfy 的区别

SysML v2 区分设计元素与需求之间的两种关系：

• assert satisfy requirement — 声明某个设计元素（零件、动作或约束）在构造上即满足某条需求。这是设计期的断言。
• verify requirement — 声明某个验证用例通过测试、分析或检查来证实该需求是否被满足。这是 V&V 期的断言。

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 def BrakeStopTest {
16
    subject sut : BrakingSubsystem;
17
    objective {
18
        verify requirement : StoppingDistance;
19
    }
20
}

可追溯性矩阵

由于 verify requirement 是一等模型元素（而非注释或标签），工具可以自动生成需求可追溯性矩阵（RTM）。每条需求都关联到零个或多个验证用例，每个验证用例也都声明自己覆盖了哪些需求。覆盖缺口 — 即没有任何验证用例的需求 — 可以通过模型查询检测出来。

系统工程传统上认可四种验证方法：测试、分析、检查与演示（TAID）。SysML v2 并未为每种方法规定专门的关键字，但语言本身为这四种方法都提供了自然的建模模式。

测试

测试是用受控输入驱动被测系统并测量其输出。这是最常见的验证用例模式 — 本模块中的示例大多属于测试用例：

1
verification 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
            ? VerdictKind::pass else VerdictKind::fail;
12
}

分析

分析依靠计算或仿真而非物理试验。在 SysML v2 中，可以把（模块 7 中的）analysis 嵌入验证用例来建模：

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

5
    action runAnalysis : ThermalAnalysisCase {
6
        in  ambientTemp = 328.15[K];  // 55 °C
7
        out peakTemp : Real;
8
    }
9

10
    return verdict : VerdictKind =
11
        if runAnalysis.peakTemp <= 358.15[K]  // 85 °C
12
            ? VerdictKind::pass else VerdictKind::fail;
13
}

检查

检查是通过审视设计制品本身来验证需求 — 例如查阅图纸、核对零件编号或确认标识。在 SysML v2 中，检查类用例通常没有激励动作，而是直接查询属性：

1
verification 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
            ? VerdictKind::pass else VerdictKind::fail;
8
}

演示

演示是在真实条件下操作系统并观察其行为来完成验证。此类验证用例的主体串联的是贴近实际的场景动作，而非孤立的激励—响应对：

1
verification 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
            ? VerdictKind::pass else VerdictKind::fail;
16
}

V 模型是系统工程生命周期的标准形态。左侧把利益相关方需要逐级分解为需求与设计，右侧则自下而上地集成并验证。SysML v2 的验证构造正好对应 V 的右半边。

左侧：从需求到设计

本系列的模块 1–7 覆盖了 V 的左侧：

• 利益相关方需要 → 带 require constraint 的 requirement def（模块 5）
• 系统需求 → 带 subject 绑定的分解后需求
• 架构 → part def、port def、connection def（模块 3）
• 详细设计 → action def、state def、analysis def（模块 4、7）

每一层都通过 assert satisfy requirement 关系与特化层次连接到它的上一层。

右侧：从验证到确认

右侧与左侧互为镜像。每一个分解层级，都有一个与之对应的验证层级：

• 单元验证 → 针对单个零件属性或动作的验证用例
• 集成验证 → 针对端口已连接、装配完成的子系统的验证用例
• 系统验证 → 针对顶层系统需求的验证用例
• 确认 → 目标面向利益相关方的验证用例（系统是否解决了最初的问题？）

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 def UnitTest_Caliper {
17
        subject sut : BrakeCaliper;
18
        objective { verify requirement : SubsystemReq; }
19
    }
20
    verification def SystemTest_Braking {
21
        subject sut : Vehicle;
22
        objective { verify requirement : SystemReq; }
23
    }
24
    verification def Validation_Safety {
25
        subject sut : Vehicle;
26
        objective { verify requirement : StakeholderNeed; }
27
    }
28
}

需求层次（V 的左侧）与验证层次（V 的右侧）互相映照，且每一层都保持可追溯。

本例为一套汽车制动系统建模了完整的验证活动。它引用了模块 5 的需求、模块 3 的结构零件与模块 4 的行为动作，演示了全部核心 V&V 模式：验证用例定义、主题绑定、目标声明、判定结论求值、多种验证方法，以及 V 模型下的可追溯性。

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 <= 0.15[s]
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 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
                ? VerdictKind::pass else VerdictKind::fail;
63
    }
64

65
    // ── Verification case 2: Response time (Analysis) ───────
66
    verification 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 <= 0.15[s]
80
                ? VerdictKind::pass else VerdictKind::fail;
81
    }
82

83
    // ── Verification case 3: Pedal force (Inspection) ───────
84
    verification 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
                ? VerdictKind::pass else VerdictKind::fail;
94
    }
95

96
    // ── Verification case 4: ABS activation (Demonstration) ─
97
    verification 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
                ? VerdictKind::pass else VerdictKind::fail;
118
    }
119

120
    // ── Composite test campaign ──────────────────────────────
121
    verification 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
        verification test1 : StoppingDistanceTest  { subject = sut; }
132
        verification test2 : ResponseTimeAnalysis   { subject = sut.brakes; }
133
        verification test3 : PedalForceInspection   { subject = sut.brakes.pedal; }
134
        verification 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
}

该模型演示了：带主题与目标的 verification def、verify requirement 可追溯性、全部四种 TAID 验证方法（测试、分析、检查、演示）、带通过 / 失败逻辑的判定结论求值，以及把各个验证用例串联起来的组合测试活动。