3. MBSE建模语言与V&V
SysML 不是“画得好看”的建模语言，它的价值在于把系统需求、结构、行为、参数四类信息组织成可追溯、可检查、可执行的模型。V&V（验证与确认）关心的核心问题是：需求是否被正确分解、设计是否覆盖需求、行为是否满足约束、参数是否落在允许区间。SysML 的九种图中，与 V&V 关系最紧密的是需求图、块定义图、内部块图、活动图、状态机图和参数图。它们不是并列的“画图工具”，而是从不同侧面回答“验证什么、在哪里验证、用什么判据验证”。
下面先给出一张总览图，说明六类图在 V&V 信息链中的分工与衔接关系。
需求图：把“验证方法”写进需求本身
需求图在 V&V 中最容易被低估。很多团队只把它当作需求列表，实际上 SysML 需求可以携带 verifyMethod 属性，取值通常为 inspection（检查）、analysis（分析）、demonstration（演示）、test（测试）。这个属性直接决定后续验证活动的类型。例如一条需求“制动控制器在收到制动指令后 100 ms 内输出制动信号”，若 verifyMethod = test，则必须设计带时间戳采集的测试用例；若写成 inspection，则无法覆盖时序指标，属于可验证性设计缺陷。
需求图还通过 deriveReqt 表达派生关系，通过 satisfy 把设计元素与需求关联，通过 verify 把验证用例与需求关联。可验证性设计的第一条原则是：每条需求至少有一条 verify 关系指向具体验证用例，且该用例的判据可量化。若某需求只有 satisfy 没有 verify，说明设计声称满足但缺少验证证据。
块定义图与内部块图：确定验证边界与测试点
块定义图（BDD）定义系统、子系统、部件的类型、属性、端口和接口。对 V&V 而言，BDD 回答的是“验证对象的边界在哪里”。例如把“电池管理系统 BMS”定义为一个块，其值属性包括 nominalVoltage: 48 V、maxChargeCurrent: 20 A，端口包括 canBus: CANPort、hvOutput: PowerPort。这些属性就是后续参数图约束和测试用例的输入变量。
内部块图（IBD）则把 BDD 中的部件实例化并连接，显示连接器和流方向。IBD 对 V&V 的关键价值是测试点定位：连接器上的信号、能量或数据流，就是可以插入探针、采集日志或注入故障的位置。例如在 IBD 中，BMS.hvOutput 与 Inverter.hvInput 之间有一条 PowerPort 连接器，验证“过流保护响应”时，测试点就应选在该连接器上，而不是笼统地写在“系统级”。
活动图与状态机图：覆盖路径与状态
活动图描述控制流和对象流，适合表达用例场景、操作流程和判定分支。V&V 中常用它做路径覆盖分析：每个判定节点（decision node）的每条出边，都应至少有一条验证用例经过。例如充电流程中有“温度是否高于 45 ℃”的判定，则高温分支和正常分支都必须有对应用例，否则覆盖不完整。
状态机图描述状态、迁移、事件和守卫条件，适合表达模式切换、故障处理和生命周期行为。V&V 中常用它做状态覆盖与迁移覆盖：每个状态至少被进入一次，每条迁移至少被触发一次，尤其是异常迁移（如“充电中 → 故障”）。守卫条件如 [temperature > 45] 必须与参数图中的约束保持一致，否则会出现“模型说不会迁移、测试却触发迁移”的矛盾。
参数图：把性能判据变成可计算约束
参数图是 SysML 中最接近“可执行验证”的图。它通过约束属性（constraint property）和绑定连接器（binding connector），把块的值属性与方程或不等式关联起来。例如定义约束 P = U × I，把 BMS.nominalVoltage 绑定到 U，把 BMS.maxChargeCurrent 绑定到 I，则 P 可被自动计算。若需求规定“充电功率不得超过 960 W”，则参数图直接给出判据：U × I ≤ 960。测试时只需采集 U 和 I，代入即可判断，而不需要人工解释需求。
下面给出一份可直接参考的“SysML 图—V&V 可验证性检查表”，用于评审模型是否具备验证条件。
| 图类型 | V&V 关注点 | 可验证性检查项 | 常见缺陷 |
|---|---|---|---|
| 需求图 | 验证什么、用什么方法 | 每条需求有 verifyMethod；有 verify 关系指向用例；判据可量化 | 只有 satisfy 无 verify；判据写“正常工作”等模糊词 |
| 块定义图 | 验证对象边界与属性 | 关键性能属性有值类型和单位；端口类型明确 | 属性无单位；接口用泛化端口无法定位测试点 |
| 内部块图 | 测试点与流方向 | 每个待验证接口有连接器；流方向与采集方向一致 | 连接器缺失；测试点写在部件内部无法访问 |
| 活动图 | 路径覆盖 | 每个判定分支至少一条用例；异常分支有对应用例 | 只覆盖正常路径；判定条件与需求不一致 |
| 状态机图 | 状态与迁移覆盖 | 每个状态可进入；每条迁移可触发；守卫条件与参数一致 | 存在不可达状态；异常迁移无触发事件 |
| 参数图 | 数值判据可计算 | 约束方程完整；绑定连接器覆盖所有变量；单位一致 | 变量未绑定；单位混用（V 与 mV）导致判据错误 |
verifyMethod 和 verificationCriteria 两个属性。前者决定验证类型，后者写成可代入数值的表达式或区间。例如 verificationCriteria = "t_response ≤ 100 ms"。这样从需求阶段就避免了“无法验证”的模糊表述。
U × I ≤ 960，而状态机守卫写 [power < 1000]，则测试时会出现判据冲突。建议在模型评审时把这三类条件放在同一张追溯表中交叉核对。
综合来看，SysML 六类图在 V&V 中形成一条从“需求判据”到“结构边界”再到“行为路径”最后到“数值约束”的证据链。可验证性设计不是建模完成后的补充工作，而是在画每一张图时就要回答：这条需求由哪张图承载、在哪个连接器上采集、经过哪条路径或迁移、代入哪个方程判断。只有把这些问题在模型中显式表达，V&V 才能从人工核对转变为可追溯、可复现的工程活动。