功能安全计算中的“可确定性”综述

# 功能安全计算中的“可确定性”综述（用于安全认证文档）

## 一、引言

在功能安全系统中，“可确定性”（Determinism）是实现高完整性等级（如 ISO 26262 ASIL-D，IEC 61508 SIL-3）系统的基本要求之一。它确保在同样的输入、环境与初始状态下，系统总能表现出一致、可预测的行为。本文将系统性地分类讨论功能安全计算中不同层次的“可确定性”类型，明确其定义、建模方式、分析工具和在安全认证中的角色。

---

## 二、主要的可确定性类型

| 可确定性类型        | 定义             | 表示符号/性质                             | 建模/验证方法              | 在认证中的作用        |
| ------------- | -------------- | ----------------------------------- | -------------------- | -------------- |
| **计算可确定性**    | 相同输入产生唯一输出     | \$f(i) \rightarrow o\$              | 状态转移系统、语义等价验证        | 避免歧义，实现一致性行为   |
| **时间可确定性**    | 响应时间在可预测区间内    | \$WCET\$, \$BCET\$                  | WCET 分析、调度验证、UPPAAL  | 确保满足任务时限要求     |
| **调度可确定性**    | 执行顺序可唯一推导      | \$\sigma(t) = \tau\_i\$             | ARINC 653、RMS/EDF 模型 | 防止资源竞争与干扰      |
| **资源访问可确定性**  | 多任务资源访问有界/无冲突  | \$\forall t\_i, A(t\_i) \subset R\$ | MPU 隔离、访问控制矩阵        | 防止非法访问、冲突等副作用  |
| **通信可确定性**    | 报文收发时序、顺序可预测   | \$delay \in \[d\_{min}, d\_{max}]\$ | TSN、CAN 等协议分析        | 消除延迟/丢包带来的安全隐患 |
| **路径可确定性**    | 控制流路径唯一或有限分支   | \$CFG\$ 稳定                          | 编译器分析、抽象解释           | 避免死路径/未定义行为    |
| **诊断行为可确定性**  | 故障检测与响应流程明确可复现 | \$E(f) \rightarrow A(f)\$           | EMV2 错误模型、契约定义       | 确保故障可检测与可控     |
| **启动/关机可确定性** | 初始/退出行为固定      | Boot → Init → Ready                 | 状态机建模、BIST 验证        | 保障生命周期完整性      |

---

## 三、数学定义与形式化表征

1. **计算可确定性**：

> 对任意输入 \$i\$ 和状态 \$s\$，程序行为 \$P(s, i)\$ 总是确定输出 \$(s', o)\$。
   >
   > $\exists!\ (s', o) \in \mathcal{S} \times \mathcal{O},\ P(s, i) = (s', o)$

2. **调度可确定性**：

> 调度函数 \$\sigma: \mathbb{T} \rightarrow \mathcal{T} \cup {\bot}\$ 唯一，满足：
   > $\forall t,\ \exists!\ \tau_i,\ \sigma(t) = \tau_i$

3. **时间可确定性**：

> 执行延迟满足固定区间：
   > $\forall \tau,\ Delay(\tau) \in [BCET, WCET]$

---

## 四、与不确定性的对照（违约场景）

| 不确定性来源 | 描述               | 风险        |
| ------ | ---------------- | --------- |
| 缓存未命中  | 执行时间波动           | 时间溢出、调度异常 |
| 多线程竞态  | 访问顺序不可控          | 状态污染、错误传播 |
| 异步事件   | 中断干扰控制流          | 死锁或重入问题   |
| 动态内存行为 | malloc/free 不可预测 | 崩溃或内存泄漏   |
| 网络延迟抖动 | 报文延迟不确定          | 通信丢失或重传失败 |

---

## 五、安全认证的需求

功能安全标准要求下，系统应提供以下证明材料以支持“可确定性”：

* **形式化模型**：AADL / TLA+ / Petri Net 等清晰建模系统结构与行为；
* **调度验证**：使用 AGREE 契约或调度表证明无空窗（完整覆盖）；
* **时间分析**：WCET 工具链（如 aiT, OTAWA）证明任务最坏执行时间；
* **隔离验证**：MPU / MMU 配置证明任务资源访问互不干扰；
* **错误模型**：EMV2 + Fault Tree 显式建模错误传播与恢复路径。

---

## 六、总结

“可确定性”是功能安全计算系统的基础保障属性之一。通过建立从**语义层、时间层、调度层、通信层到物理层**的多维度可确定性分析框架，可以实现系统运行行为的**可证明性、可追踪性与可复现性**。这不仅是系统设计的核心目标，也是认证流程中的关键评估要素。

---

> 本文可作为功能安全开发团队构建安全目标文档、架构说明书、形式化验证计划中的组成部分，适用于 ISO 26262、IEC 61508、ARINC 653 等安全标准框架。

同济大学计算机开放实验室/ComoFramework

内容风险标识

评论 (0)

同济大学计算机开放实验室/ComoFramework .gitee-modal { width: 500px !important; }

内容风险标识