模块 5：需求与约束

SysML v2 的需求与约束建立在 KerML 的约束（Constraint）机制之上 — 这部分语言专门用来表达必须成立的布尔条件。本模块中的每个需求关键字，都是对 KerML 核心层与约束层某个 L1 构造的 SysML L2 特化。

KerML 起源：requirement def → ConstraintDefinition（核心层）

需求定义声明一个可复用的需求模板。它为需求命名，可以附加文档文本，也可以包含形式化的约束表达式。这正是前几个模块中「定义 / 使用」模式里的定义一侧。

带 doc 字符串的基本需求

最简单的写法是给一个具名需求定义附上 doc 字符串，用来承载系统工程中传统的「应当（shall）」式陈述：

1
requirement def MaxSpeedReq {
2
    doc /* The vehicle shall not exceed a maximum speed of 250 km/h
3
         under normal operating conditions. */
4
}

带属性的结构化需求

需求可以像零件定义一样携带带类型的属性。需求定义体内的 attribute 关键字声明的是参数，它们在需求被使用时才被绑定：

1
requirement def SpeedLimitReq {
2
    doc /* The vehicle shall not exceed the specified speed limit. */
3
    attribute maxSpeed : ISQ::SpeedValue;
4
    subject vehicle : Vehicle;
5
    require constraint { vehicle.currentSpeed <= maxSpeed }
6
}

需求标识符

需求可以带一个简短标识符以便追溯。SysML v2 为此提供了短名语法（尖括号写法）：

1
requirement def <'REQ-BRK-001'> BrakingDistanceReq {
2
    doc /* The vehicle shall achieve full stop within 40 metres
3
         from 100 km/h on a dry surface. */
4
    subject vehicle : Vehicle;
5
    attribute surfaceCondition : SurfaceType;
6
}

KerML 起源：requirement（使用）→ ConstraintUsage（由 ConstraintDefinition 定型的 Feature）

需求使用是需求定义在具体上下文中的实例化。与零件、动作的「定义 / 使用」划分一样：定义是可复用的模板，使用则把它绑定到具体的取值和设计元素上。

简单的需求使用

1
package VehicleRequirements {
2
    requirement maxSpeedReq : SpeedLimitReq {
3
        subject vehicle : SportsCar;
4
        attribute :>> maxSpeed = 250 [km/h];
5
    }
6
}

把需求嵌套成层次结构

需求可以嵌套，形成分解层次。父需求包含子需求，表示只有当全部子需求都成立时，父需求才被满足：

1
requirement def VehicleSafetyReq {
2
    doc /* The vehicle shall meet all safety requirements. */
3
    subject vehicle : Vehicle;
4

5
    requirement brakingReq : BrakingDistanceReq {
6
        doc /* Braking sub-requirement. */
7
    }
8

9
    requirement stabilityReq : StabilityControlReq {
10
        doc /* Stability control sub-requirement. */
11
    }
12

13
    requirement airbagReq : AirbagDeploymentReq {
14
        doc /* Airbag deployment sub-requirement. */
15
    }
16
}

在层次结构中传递 subject 绑定

当父需求声明了 subject，子需求会继承这个绑定，除非自己覆盖它。这保证所有子需求都作用在同一个设计元素上：

1
requirement def PowertrainReq {
2
    subject powertrain : Powertrain;
3

4
    requirement torqueReq {
5
        doc /* Peak torque shall exceed 400 Nm. */
6
        require constraint { powertrain.peakTorque >= 400 [N*m] }
7
    }
8

9
    requirement efficiencyReq {
10
        doc /* Overall efficiency shall be at least 92%. */
11
        require constraint { powertrain.efficiency >= 0.92 }
12
    }
13
}

KerML 起源：satisfy → SatisfyRequirementUsage（特化自 RequirementUsage 与 AssertConstraintUsage）

满足（satisfy）关系（写作 assert satisfy）断言某个设计元素达成了某条需求。它是需求域与设计域之间最主要的追溯链路。需求流转（由系统需求导出子系统需求）则通过特化（specializes）实现，SysML v2 没有单独的 derive 关键字。

satisfy：把需求连到设计上

1
part def BrakingSystem;
2

3
part vehicle : Vehicle {
4
    part brakes : BrakingSystem;
5

6
    // Assert that the braking system satisfies the braking requirement
7
    assert satisfy brakingReq by brakes;
8
}

多重满足

一个设计元素可以满足多条需求，一条需求也可以由多个元素协同满足：

1
part vehicle : Vehicle {
2
    part brakes   : BrakingSystem;
3
    part esc      : ElectronicStabilityControl;
4
    part airbags  : AirbagSystem;
5

6
    assert satisfy brakingReq   by brakes;
7
    assert satisfy stabilityReq by esc;
8
    assert satisfy airbagReq    by airbags;
9
}

用特化实现需求流转

需求流转（由系统需求导出子系统需求）使用 specializes 实现。子需求继承父需求的全部约束，并可以追加新约束或收紧已有约束：

1
requirement def SystemSafetyReq {
2
    doc /* The system shall prevent unintended acceleration. */
3
}
4

5
requirement def ThrottleSafetyReq specializes SystemSafetyReq {
6
    doc /* The throttle controller shall return to idle
7
         within 200 ms of brake pedal activation. */
8
}

KerML 起源：constraint def → ConstraintDefinition； constraint → ConstraintUsage

约束是一个求值为真或假的布尔表达式。约束是需求的形式化骨架：doc 字符串承载人可读的意图，约束则承载机器可校验的条件。每个 requirement def 本身就是一个特化的 constraint def。

定义约束

1
constraint def TemperatureRange {
2
    attribute temp : ISQ::TemperatureValue;
3
    attribute minTemp : ISQ::TemperatureValue;
4
    attribute maxTemp : ISQ::TemperatureValue;
5
    temp >= minTemp and temp <= maxTemp
6
}

在零件上使用约束

约束可以施加在结构元素上，用来断言在系统整个生命周期内都必须成立的不变式：

1
part def Engine {
2
    attribute operatingTemp : ISQ::TemperatureValue;
3
    attribute coolantTemp   : ISQ::TemperatureValue;
4

5
    constraint tempLimit : TemperatureRange {
6
        attribute :>> temp    = operatingTemp;
7
        attribute :>> minTemp = 343.15 [K];  // 70 °C
8
        attribute :>> maxTemp = 393.15 [K];  // 120 °C
9
    }
10
}

带运算符的约束表达式

SysML v2 为约束提供了丰富的表达式语言，包含算术、比较和逻辑运算符：

1
constraint def PowerBudget {
2
    attribute totalPower     : ISQ::PowerValue;
3
    attribute maxPower       : ISQ::PowerValue;
4
    attribute safetyMargin   : Real;
5
    totalPower <= maxPower * (1.0 - safetyMargin)
6
}
7

8
constraint def MassBalance {
9
    attribute dryMass    : ISQ::MassValue;
10
    attribute fuelMass   : ISQ::MassValue;
11
    attribute payloadMass: ISQ::MassValue;
12
    attribute maxTakeoff : ISQ::MassValue;
13
    dryMass + fuelMass + payloadMass <= maxTakeoff
14
}

KerML 起源：assume constraint → isAssumption = true 的 ConstraintUsage； require constraint → isRequired = true 的 ConstraintUsage

SysML v2 把需求内部的约束分成两类：假设（被视为理所当然成立的条件）与要求约束（必须被保证的条件）。这种区分对应契约式编程的思路：只要假设成立，要求约束就必须被满足。

assume 与 require 的区别

1
requirement def BrakingPerformanceReq {
2
    doc /* The vehicle shall stop within 40 m from 100 km/h. */
3
    subject vehicle : Vehicle;
4

5
    assume constraint dryRoad {
6
        doc /* Surface friction coefficient is at least 0.7. */
7
        vehicle.surface.frictionCoeff >= 0.7
8
    }
9

10
    assume constraint normalLoad {
11
        doc /* Vehicle mass does not exceed gross vehicle weight. */
12
        vehicle.totalMass <= vehicle.grossVehicleWeight
13
    }
14

15
    require constraint stopDistance {
16
        doc /* Stopping distance from 100 km/h shall not exceed 40 m. */
17
        vehicle.stoppingDistance(100 [km/h]) <= 40 [m]
18
    }
19
}

动作的前置条件与后置条件

assume 和 require constraint 是需求体内的条目 — 它们不能直接写在 action def 里。要为动作表达前置条件与后置条件，应当写一个以该动作为 subject 的需求：

1
requirement def EmergencyBrakeContract {

2
    subject brake : EmergencyBrake;

3


4
    // Precondition: vehicle must be moving

5
    assume constraint {

6
        brake.vehicle.speed > 0 [km/h]

7
    }

8


9
    // Postcondition: vehicle must be stopped

10
    require constraint {

11
        brake.vehicle.speed == 0 [km/h]

12
    }

13
}

14


15
action def EmergencyBrake {

16
    in part vehicle : Vehicle;

17
}

下面的模型综合了前五节的全部内容：一个车辆制动系统，包含需求定义、层次分解、满足关系、形式化约束，以及假设与保证的分离。

1
package VehicleBrakingRequirements {
2
    private import ISQ::*;
3
    private import SI::*;
4
    private import ScalarValues::*;
5

6
    // ── Structure (from earlier modules) ────────────────────
7
    part def Vehicle {
8
        attribute totalMass : ISQ::MassValue;
9
        attribute speed     : ISQ::SpeedValue;
10
    }
11

12
    part def BrakingSystem {
13
        attribute brakingForce    : ISQ::ForceValue;
14
        attribute responseTime    : ISQ::TimeValue;
15
        attribute thermalCapacity : ISQ::EnergyValue;
16
    }
17

18
    part def ABSController;
19
    part def BrakeActuator;
20

21
    // ── Constraints (reusable boolean expressions) ──────────
22
    constraint def MaxStoppingDistance {
23
        attribute distance : ISQ::LengthValue;
24
        attribute limit    : ISQ::LengthValue;
25
        distance <= limit
26
    }
27

28
    constraint def ResponseTimeLimit {
29
        attribute actual : ISQ::TimeValue;
30
        attribute limit  : ISQ::TimeValue;
31
        actual <= limit
32
    }
33

34
    // ── Requirement definitions ─────────────────────────────
35
    requirement def <'REQ-BRK-000'> BrakingSafetyReq {
36
        doc /* The braking system shall ensure safe deceleration
37
             under all normal operating conditions. */
38
        subject vehicle : Vehicle;
39

40
        // ── Child: stopping distance ──
41
        requirement <'REQ-BRK-001'> stopDistReq {
42
            doc /* Full stop within 40 m from 100 km/h. */
43

44
            assume constraint drySurface {
45
                vehicle.surface.frictionCoeff >= 0.7
46
            }
47

48
            require constraint : MaxStoppingDistance {
49
                attribute :>> distance = vehicle.stoppingDistance;
50
                attribute :>> limit    = 40 [m];
51
            }
52
        }
53

54
        // ── Child: response time ──
55
        requirement <'REQ-BRK-002'> responseTimeReq {
56
            doc /* Brake actuation shall begin within 150 ms
57
                 of pedal input. */
58

59
            require constraint : ResponseTimeLimit {
60
                attribute :>> actual = vehicle.brakes.responseTime;
61
                attribute :>> limit  = 0.15 [s];
62
            }
63
        }
64

65
        // ── Child: thermal endurance ──
66
        requirement <'REQ-BRK-003'> thermalReq {
67
            doc /* Brakes shall sustain 10 consecutive emergency stops
68
                 without fade below 80% effectiveness. */
69

70
            assume constraint normalAmbient {
71
                vehicle.ambientTemp >= 253.15 [K] and  // -20 °C
72
                vehicle.ambientTemp <= 318.15 [K]  // 45 °C
73
            }
74

75
            require constraint {
76
                vehicle.brakes.fadeAfterRepeatedStops(10) >= 0.80
77
            }
78
        }
79
    }
80

81
    // ── Specialised requirement: ABS-specific ──────────────
82
    requirement def <'REQ-ABS-001'> ABSActivationReq specializes BrakingSafetyReq {
83
        doc /* ABS shall modulate brake pressure at 15 Hz minimum
84
             when wheel slip exceeds 10%. */
85
        subject abs : ABSController;
86
        // flow-down via specializes (declared above)
87

88
        require constraint {
89
            abs.modulationFrequency >= 15 [Hz]
90
        }
91
    }
92

93
    // ── Satisfaction: linking design to requirements ────────
94
    part testVehicle : Vehicle {
95
        part brakes     : BrakingSystem;
96
        part absCtrl    : ABSController;
97
        part actuators  : BrakeActuator;
98

99
        assert satisfy requirement : BrakingSafetyReq by brakes;
100
        assert satisfy requirement : ABSActivationReq by absCtrl;
101
    }
102
}

该模型演示了：带 doc 字符串与标识符的 requirement def、需求的层次分解（父需求 BrakingSafetyReq 下含三条子需求）、assume 与 require constraint 的分离、可复用的约束定义（MaxStoppingDistance、ResponseTimeLimit）、用 specializes 实现需求流转（ABSActivationReq 特化 BrakingSafetyReq），以及把需求连到设计元素的 assert satisfy 链接。