14.3 中断驱动软件与验证

集成硬件会在软件是否准备好都不确定的情况下产生事件。中断驱动固件必须在下个事件前完成紧急工作、保持共享状态一致，并把长时间处理留给前台代码。随后，验证要提供证据，证明这些性质在正常与故障条件下都成立。

保持处理程序有界并维护共享缓冲区一致性

综合项目使用环形缓冲区（ring buffer）：一个固定数组，带有称为 head 的写索引与称为 tail 的读索引。DMA 或 ISR 在样本到达后推进 head；前台代码消费样本后推进 tail。索引到达数组末尾时会回绕到零。

当 head==tail 时缓冲区为空。一种安全约定是在推进 head 后将等于 tail 时宣布缓冲区已满，有意留出一个不用的单元。不变量（invariant）是在每个可达状态都必须成立的规则，例如“索引始终位于数组内部”和“生产者绝不覆盖未读数据”。

ISR 的最坏执行时间比平均时间更重要。若样本每 1000 个周期到达，但处理程序最多消耗 1200 个周期，即使单次测试看起来正确，积压仍会增长。优先级不会创造 CPU 容量。更高优先级的 UART ISR 也可能推迟采样 ISR，因此最坏响应时间（worst-case response time）包括阻塞和高优先级干扰。

如果中断发生在前台读取多字节字段的中间，共享字段可能不一致。软件可以在很短的临界区暂时屏蔽中断、使用处理器支持的原子指令，或采用更新天然原子的生产者/消费者协议。调度实验会直接显示过载、优先级干扰、缓冲区填充与事件丢失。

用轨迹、边界与故障注入验证需求

测试展示选定情形中的行为。验证（verification）把每项需求连接到证据，并包含最容易隐藏缺陷的边界条件。可追溯矩阵（traceability matrix）把需求 ID 映射到测试与结果，使看似完整的测试套件无法悄悄遗漏需求。

有用的测试类型包括：

• 标称测试：普通采样、命令与风扇更新。

• 边界测试：缓冲区空/满、末地址、最大 ADC 编码、同时事件和恰好截止时刻。

• 故障注入测试：READY 卡住、奇偶错误、遗漏 EOI、DMA 通道被屏蔽、译码重叠与传感器削顶。

• 长时间测试：计数器回绕、重复自动初始化与缓慢累积的积压。

最终输出正确并不是充分证据。如果缓冲区曾短暂溢出后恢复，最后风扇电压可能正确，但数据已经丢失。验证要观察中间状态：请求时刻、ISR 进入、总线所有权、head/tail 变化、错误标志与输出更新时间。

验证控制台允许选择需求、情景和注入故障，然后显示哪些断言能够检出问题，以及哪些覆盖仍然缺失。若一个故意注入的故障没有任何测试发现，在产品真正失效之前，验证就已经失败。

第 14.3 节把时序与状态声明转换成证据。第 14.4 节将把同样耐久的思想映射到现代 x86、ARM 与片上系统；集成密度虽然更高，但所有权与可见性依然关键。