4. 需求建模与可验证性分析

在MBSE的验证与确认（V&V）工程中，需求不是一段静态文字，而是贯穿系统生命周期的“可验证契约”。如果需求在捕获阶段就模糊、在形式化阶段就不可判定、在追溯阶段就断裂，那么后续的仿真、测试和评审都会失去基准。本节围绕四个相互衔接的环节展开：基于模型的需求捕获、需求形式化、需求可验证性准则，以及需求追溯与验证矩阵构建。

一、基于模型的需求捕获

传统需求捕获以文档为中心，需求散落在Word或Excel中，与系统架构、接口、行为模型之间靠人工维护的“链接”关联。基于模型的需求捕获则把需求作为模型元素纳入统一仓库，使每条需求都拥有唯一标识、属性、所属包和与其他模型元素的关系。以SysML为例，需求通常用«requirement»构造型表示，其核心属性包括id、text，并可扩展source、rationale、verificationMethod、status等。

捕获时建议遵循“先结构、后行为、再约束”的顺序：先从利益相关者需要和系统边界导出顶层需求，再分解到功能、性能、接口、安全等类别，最后用«deriveReqt»、«satisfy»、«verify»、«refine»等关系把需求与用例、模块、活动、状态机连接起来。例如，一条顶层需求“无人机在GPS拒止环境下应能自主返航”可分解为“导航模块应支持惯性导航解算”“返航路径应避开禁飞区”“返航时间不超过90秒”等子需求，并分别挂接到导航子系统、路径规划活动和时序约束上。

二、需求形式化

自然语言需求容易产生歧义，形式化是把“可读”转化为“可判定”的关键步骤。形式化不等于全部写成数学公式，而是根据验证方式选择合适的形式：对逻辑条件可用时序逻辑或断言，对参数约束可用参数图与等式，对状态行为可用状态机或活动图，对接口数据可用类型与范围定义。

例如，需求“当高度低于120米时，系统应在2秒内触发返航”可形式化为：

when altitude < 120 m
then within 2 s
  system.mode == RETURN_HOME
  and navigation.source == INERTIAL

在模型中，这可以表达为状态机中的迁移条件、活动图中的约束节点，或参数图中的约束属性。形式化的目标是让每条需求都能对应到一个可观察、可测量、可判定的验证事件。

三、需求可验证性准则

一条需求是否可验证，通常用以下准则判断：

• 可观察性：验证结果能通过接口、日志、遥测或测试点直接观测。
• 可测量性：涉及性能、时间、精度等指标时，必须有明确数值和单位。
• 无歧义性：术语、条件、主体、动作唯一，不依赖读者主观解释。
• 可判定性：存在明确的通过/失败判据，而不是“尽量”“适当”等模糊表述。
• 可追溯性：能向上追溯到利益相关者需要，向下追溯到设计、实现和测试用例。
• 一致性：不与其它需求冲突，边界条件不重叠或遗漏。

实践中可用“需求质量检查表”逐条打分。例如，把“系统应快速响应”改为“在收到返航指令后，系统应在500毫秒内进入返航模式，并在2秒内输出返航航向”，就从不可验证变为可验证。

四、需求追溯与验证矩阵构建

需求追溯的核心是建立“需求—设计—实现—验证”的双向链路。验证矩阵（Verification Matrix）是这一链路的表格化表达，通常包含需求ID、需求描述、验证方法、验证层级、测试用例/仿真场景、预期结果、实际结果、状态和证据链接。验证方法一般分为检查、分析、演示和测试四类，在模型中可用«verify»关系把需求与测试用例、仿真配置或分析模型连接起来。

构建验证矩阵时，建议先按需求层级分组，再逐条填写验证方法。对于无法直接测试的需求，应通过分析或演示补充证据；对于存在多条需求共用同一测试用例的情况，应在矩阵中显式标注覆盖关系，避免漏测。矩阵不是一次性文档，而应随模型迭代自动更新，确保需求变更后验证状态同步刷新。

从工程实践看，需求建模与可验证性分析不是一次性活动，而是与架构设计、仿真验证、测试执行持续交互的闭环。模型中的需求元素、形式化约束、追溯关系和验证矩阵共同构成“可验证性证据链”，使V&V活动有据可依、有迹可循。