2. 嵌入式软件需求验证

需求验证不是“把需求读一遍确认没意见”，而是要在软件设计开始之前，用可检查的方式回答三个问题：这条需求能不能被验证？它是否被上层目标完整覆盖？它与其它需求之间是否存在矛盾或遗漏？在飞控这类安全关键软件中，需求缺陷一旦流入设计与编码，修复成本会随阶段呈数量级上升，因此需求验证是整条验证链中性价比最高的一环。

一、需求可验证性准则

一条需求可验证，意味着存在有限、客观、可重复执行的判定过程，能给出“通过/不通过”的确定结论。工程上通常用以下准则逐条筛查：

• 可观测：需求涉及的输出必须能被测量或采集，例如舵面偏度、总线报文、状态字，而不是“系统应工作良好”这类无法观测的表述。
• 可判定：判定条件必须量化。把“响应应及时”改写为“在传感器有效且模式为增稳时，从横滚角速率指令输入到舵机指令输出的延迟不超过 20 ms”。
• 无歧义：术语、单位、坐标系、边界条件唯一。例如必须明确“横滚角”是机体轴还是地面轴，正方向如何定义。
• 可追溯：每条需求有唯一标识，并能向上追溯到系统需求或适航目标，向下派生到设计单元与测试用例。
• 可实现且不冲突：在给定资源（周期、算力、总线带宽）下可满足，且不与其它需求在同一工况下给出相反约束。

实践中可用一个简单的“可验证性评分”快速分诊：对可观测、可判定、无歧义、可追溯四项各记 0/1 分，低于 3 分的需求必须返工，不得进入追踪矩阵。例如“飞控应保证飞行安全”得 0 分，属于典型不可验证需求；“当空速低于 30 m/s 时，应禁止起落架收起指令输出”得 4 分，可直接进入验证流程。

二、需求追踪矩阵的构建

需求追踪矩阵（RTM）是把“来源—需求—设计—实现—测试”串成闭环的表结构。构建时先给每条需求分配形如 FCS-REQ-012 的稳定标识，再逐列填充。一个可用的最小字段集如下：

矩阵的价值在于暴露“孤儿”和“悬空”：某条需求没有任何测试用例，说明验证遗漏；某个测试用例不追溯任何需求，说明存在无依据的测试。构建时应双向检查——从需求向下找测试，从测试向上找需求，两侧都闭合才算完整。对于派生需求，还要检查其父需求是否被所有子需求之和完整覆盖，避免“分解后丢失约束”。

三、基于形式化方法的矛盾与遗漏检测

自然语言需求难以自动推理，因此需要把关键需求转成形式化模型。常用做法是用线性时序逻辑（LTL）或信号时序逻辑（STL）描述时序约束，再用模型检验工具（如 NuSMV、SPIN）搜索反例。以两条飞控需求为例：

R1: 当 空速 < 30 m/s 时，禁止 起落架收起
R2: 当 起落架手柄置"收" 且 起落架未锁定 时，允许 起落架收起

形式化（简化）：
R1: G( (airspeed < 30) -> !gear_retract )
R2: G( (handle_up && !gear_locked) -> gear_retract )

把 R1、R2 同时送入模型检验器，若存在状态使 airspeed < 30 与 handle_up && !gear_locked 同时成立，则两条需求在该工况下矛盾——一个禁止、一个允许。工具会输出一条反例路径，工程师据此判定是需求冲突还是缺少优先级约束（例如“安全约束优先于操作指令”）。遗漏检测则通过覆盖性检查完成：把系统需求集合作为性质，验证设计模型是否满足所有性质，未被满足的性质即为遗漏或实现缺口。

四、典型飞控需求验证案例

以某型无人机横滚增稳功能为例。系统需求 SYS-REQ-009 要求“在增稳模式下，横滚角速率指令到副翼舵机指令的延迟不超过 20 ms”。验证过程如下：

1. 可验证性检查：输出为副翼舵机指令（可采集），判定条件为延迟≤20 ms（可量化），坐标系与单位明确，追溯至 SYS-REQ-009，评分 4 分，通过。
2. RTM 登记：FCS-REQ-013 对应设计单元 Roll_Ctrl.c，测试用例 TC-PERF-003，验证方法为“分析+测试”。
3. 形式化检查：将“增稳模式→延迟约束”与“故障模式→舵机回中”两条需求建模，模型检验未发现矛盾，但发现“模式切换瞬间”未被任何需求约束，判定为遗漏，补充需求 FCS-REQ-021。
4. 测试执行：在硬件在环台架上注入 1 Hz、幅值 10°/s 的横滚角速率阶跃指令，采集指令输入时刻与舵机指令输出时刻，示例测得延迟 14 ms、16 ms、15 ms，均小于 20 ms，判定通过。

该案例说明：需求验证不是单点动作，而是“可验证性筛查→追踪矩阵登记→形式化矛盾/遗漏检测→测试确认”的闭环。任何一步发现的问题都应回写到需求库，并同步更新 RTM 状态，确保需求、设计、测试三者始终一致。

把上述闭环固化到流程中，需求验证就从“人工评审”升级为“可追溯、可推理、可复现”的工程活动。下一阶段的设计与编码，只有在需求侧完成这一轮筛查后，才具备可靠的输入基线。