4. 详细设计验证

详细设计验证的对象不再是需求文本，而是可执行语义更明确的设计模型——通常以 Simulink/Stateflow、SCADE、AADL 或 UML/SysML 模型为载体。与需求评审相比，详细设计验证的核心变化在于：验证证据从“人工阅读判断”转向“工具可计算的结构与行为属性”。本章围绕四类活动展开：设计模型静态分析、控制流与数据流验证、设计到需求的追溯性检查、基于模型的测试用例生成。它们并非线性步骤，而是共享同一份设计模型、互为输入输出的验证闭环。

一、设计模型静态分析：先看“结构是否合规”

静态分析不执行模型，只检查模型的语法、语义与建模规范。对航空航天嵌入式软件而言，静态分析通常覆盖三类规则：

• 建模规范类：命名一致性、端口方向、数据类型显式声明、禁止隐式类型转换、采样时间一致性、禁止代数环等。
• 安全模式类：禁止未初始化输出、禁止除零常量、禁止无默认分支的条件结构、禁止未连接的输入端口。
• 可追溯性类：每个功能模块是否绑定需求标识、是否缺少验证状态标记。

以某飞控大气数据模块为例，模型包含 ADC_Pressure、Temp_Compensate、Altitude_Calc 三个子系统。静态分析报告可能给出如下结果：

检查项：采样时间一致性
对象：Altitude_Calc / RateLimiter
结果：FAIL
说明：输入端口采样时间 0.01s，内部增益模块采样时间 0.02s
建议：统一为 0.01s 或显式声明速率转换

检查项：未初始化输出
对象：Temp_Compensate / Out1
结果：PASS

静态分析的价值在于“早发现、低成本”。一个采样时间不一致的问题若留到硬件在环阶段暴露，定位成本可能上升一个数量级。工程上通常将静态分析设为模型入库的门禁：未通过规则集不允许进入下一阶段。

二、控制流与数据流验证：看“行为是否可达、数据是否可信”

静态分析解决结构合规，控制流与数据流验证解决行为正确性。控制流验证关注状态机或条件分支的可达性、死逻辑、状态迁移完整性；数据流验证关注变量定义—使用链、数据依赖、范围传播与未定义使用。

以 Stateflow 实现的起落架收放控制为例，状态包括 GearUp、GearDown、Transitioning、Fault。控制流验证需要回答：Fault 状态是否在所有异常条件下可达？是否存在从 GearUp 直接跳到 GearDown 而绕过 Transitioning 的非法迁移？数据流验证则检查 gear_position_cmd 是否在每次使用前都被赋值，hydraulic_pressure 的取值范围是否在传感器量程内传播。

一个典型的数据流缺陷是“条件赋值遗漏”：在 if (mode == AUTO) 分支中给 cmd 赋值，但 else 分支未赋值，导致 cmd 保持上一周期值。数据流分析工具会标记该变量存在“可能未初始化使用”路径。修复方式不是简单补一个默认值，而是明确 else 分支的业务语义——是保持、清零还是进入安全值。

三、设计到需求的追溯性检查：看“每条需求是否被设计覆盖”

追溯性检查回答两个方向的问题：正向追溯——每条需求是否都有设计元素实现；反向追溯——每个设计元素是否都对应至少一条需求，是否存在“无需求来源”的冗余设计。

工程上通常用需求—设计追溯矩阵（RTM）承载。矩阵行是需求标识，列是模型元素路径，单元格标记实现关系。检查规则包括：

• 需求未覆盖：某条需求在矩阵中无任何设计元素对应，说明设计遗漏。
• 设计无来源：某模型元素无需求对应，可能是多余设计或需求遗漏。
• 追溯断裂：需求变更后，原设计链接失效，需重新确认。

追溯性检查不是一次性动作，而应嵌入变更流程。当需求 REQ-ALT-012 从“高度计算误差 ≤ 3m”改为“≤ 2m”时，追溯矩阵应自动标出受影响的设计元素 Altitude_Calc / CompensationTable，并触发回归验证。

四、基于模型的测试用例生成：从“人工设计”到“模型驱动”

前三类活动产出的是缺陷清单和追溯证据，第四类活动产出的是可执行的测试用例。基于模型的测试用例生成（MBT）利用设计模型的结构与行为信息，自动或半自动地推导测试输入序列与预期输出。

常见覆盖目标包括：

• 判定覆盖：每个条件分支的真假至少各执行一次。
• 状态覆盖：每个状态至少进入一次。
• 迁移覆盖：每条合法迁移至少触发一次。
• 迁移对覆盖：连续两条迁移的组合至少触发一次，用于发现状态序列相关缺陷。
• MC/DC：对安全关键条件，每个原子条件独立影响判定结果。

以高度计算模块为例，假设其输入为 pressure（范围 200～1100 hPa）和 temp（范围 -55～70℃），输出为 altitude。若采用边界值加判定覆盖，可生成如下测试用例骨架：

用例 TC-ALT-001
  输入：pressure=200, temp=-55
  预期：altitude 在 [ -1000, 0 ] m 区间
  覆盖：pressure 下边界、temp 下边界

用例 TC-ALT-002
  输入：pressure=1100, temp=70
  预期：altitude 在 [ 15000, 16000 ] m 区间
  覆盖：pressure 上边界、temp 上边界

用例 TC-ALT-003
  输入：pressure=650, temp=15
  预期：altitude 在 [ 3000, 4000 ] m 区间
  覆盖：典型巡航点

用例 TC-ALT-004
  输入：pressure=1013.25, temp=15
  预期：altitude 接近 0 m（标准大气海平面）
  覆盖：标准大气基准点

MBT 的关键不是“自动生成”本身，而是覆盖准则与安全目标的绑定。对 DAL A 级软件，仅做判定覆盖通常不足，需要 MC/DC 或等价类加边界组合。工具生成的用例仍需人工确认其物理合理性——例如 pressure=200, temp=70 在真实大气中是否可能出现，若不可能，应作为无效组合剔除或标记为鲁棒性测试。

五、四类活动的协同与工程落地

这四类活动在实际项目中共享同一份设计模型和同一套需求基线。静态分析发现的采样时间不一致，会直接影响控制流分析的周期假设；数据流分析发现的未初始化路径，会成为测试用例生成的重点覆盖目标；追溯性检查发现的需求未覆盖，会反向要求补充设计或调整测试范围。

工程落地时建议把握三个原则：第一，静态分析与追溯性检查设为模型入库门禁，不通过不进入下一阶段；第二，控制流与数据流验证结果必须关联到具体模型元素路径，便于修复闭环；第三，MBT 生成的用例需与需求标识绑定，确保每条安全需求都有对应的测试证据。只有四类活动形成证据链，详细设计验证才能真正支撑适航审定中的“设计正确且可验证”结论。