AADL CMU MBSE SEI 契约安全关键系统安全性形式化验证论证

基于模型的安全关键系统保障 — 契约与论证¶

概述¶

作者: Dionisio de Niz, CMU SEI
会议: MBSE in Practice Conference 2025, 2025年8月21日
资助: DoD Contract No. FA8702-15-D-0002（SEI作为FFRDC的运营合同）
核心创新: 提出基于模型的契约（Model-Based Contracts）和论证（Argumentations）方法，用于安全关键系统的形式化保障

核心问题：多重声明 — 多重分析¶

安全关键系统面临多种保障声明，每种声明需要不同分析，而不同分析的假设可能冲突：

控制稳定性（Control Stability）
可调度性（Schedulability）
功耗（Power）
温度/热失控（Thermal Runaway）
死锁/模型检查（Deadlock/Model Checking）

不同分析域（传感器采样、PID控制器、执行器、通信协议等）之间存在复杂的假设-保证关系，需要统一的框架来： - 组合多重分析 - 验证假设 - 解决假设冲突 - 整合到论证中以满足声明

核心方法论¶

分析契约（Analysis Contract）¶

每个分析被建模为包含四个组件的契约：

contract {
  inputs: E2ELatencies
  assumptions: areConnectionsDelayed(), areDeadlinesConstrained(), 
               areTasksSchedulable(), areAllThreadsPeriodic()
  analysis: meetEndToEndLatencies()
  guarantee: [E2EResponses[i] <= E2ELatencies[i] for i in range(len(Responses))]
}

假设（Assumptions）：分析有效所必须满足的约束条件
分析（Analysis）：评估保证是否可以履行
保证（Guarantee）：作为模型上真实事实呈现的断言
实现（Implementation）：基于SMT求解器（Z3）实现契约论证

保障契约论证（Assurance Contract Argumentation）¶

建立了契约之间的层级论证结构：

Claim 1 → Contract 1 → Guarantee（提供Assumption 1给下层）
Claim 2 → Contract 2 → Guarantee（依赖Assumption 2，又为上层提供Assumption 3）
Claim 3 → Contract 3 → Guarantee

论证链使用AADL数据作为证据，支持行为模型验证。关键机制： - 静态验证（Static Verification）使用AADL证据 - 行为模型提供假设验证 - 分析之间通过证明义务（Proof Obligation）连接

符号化契约论证框架¶

核心创新技术组件：

假设约束条件推理
SMT（Z3）实现契约论证：评估约束条件是否能从分析保证的事实中得到满足
假设验证：证明义务确保约束条件的缺失不会允许任何值满足假设（如RM优先级）
精化过程中的论证演进：未约束的符号变量被赋值以满足问题 → 视为证明义务（由于部分模型） → 最终验证完整模型的所有可能值

分析契约选择策略¶

基于精化的选择：基于模型数据可用性选择契约
基于设计的选择：基于模型数据类型（如RM优先级）选择契约

契约论证可扩展性¶

利用科学领域知识：

策略	说明
专门域算法	如实时理论中的贪心最坏情况响应时间，用命令式语言实现
分析正确性假设	验证契约论证时假定分析正确，可连接其他低级验证结果（如PROSA: Coq定理证明器验证实时理论）
实现正确性	利用运行时机制的已证明属性（调度器、hypervisor）；利用代码生成；推迟代码验证以适应假设

论证模块化（Argument Modularity）¶

支持将复杂安全声明分解为子声明，逐步构建备选方案：

可靠自动刹车（Reliable Autobrake）声明分解为多层子声明
子声明之间通过OR关系连接备选分析契约（如HarmonicBound vs NonHarmonicBound vs ResponseTime分析）
利用OR机制支持增量式分解和备选方案评估

多架构描述的分析论证¶

支持从不同架构描述中查询和组合分析：

AADL架构 → 提取线程、周期、WCET
SysML v2 / SysML v1架构 → 不同建模语言的一致性分析
使用模型查询语言提取分析所需数据：threads = root.allSubcomponents.filter {s -> s.isThread}
最终生成综合性的认证（Certificate）

案例研究：A330 CI202事故分析¶

2020年6月14日，空客A330-302在台北着陆时三台飞行控制主计算机（FCPC/PRIM）准同时故障，导致地面扰流板、反推和自动刹车全部失效。机组在跑道末端30英尺前安全停下飞机。

A330架构分析¶

完整性（Integrity）：COM+MON对（不同团队独立开发，需相同输入 → 输出交叉检查）
可用性（Availability）：PRIM1+PRIM2+PRIM3三重冗余（需独立故障假设 → FTA分析）
端到端时序：延迟通信、RM优先级、无自挂起

AADL通道建模¶

pedalToActuationCOMPRIM1: end to end flow 
  Sensor1.s1 -> Sensor1.f1 -> c2 -> COM.f5 -> c6 -> Actuator1.k1
pedalToActuationMONPRIM1: end to end flow 
  Sensor2.s3 -> Sensor2.f3 -> c4 -> MON.f6 -> c5 -> COM.f5 -> c6 -> Actuator1.k1

关键分析发现¶

零输入抖动无法实现——除非采用复杂（不现实）的同步方案
COM和MON可能同时故障——如果输出不一致
共享COM+MON传感器保留多样化计算——这是修正方案

验证计划¶

使用三个域（同步、可靠性、可调度性）和对应契约： - SamplingSynchronizationContract：验证采样抖动 ≤ 容忍度 - ReliabilityContract：验证可靠性 ≥ 目标（假设副本在独立处理器上） - EndToEndDelayedCommunicationContract：验证端到端响应 ≤ 延迟要求

结论与新架构¶

原始A330设计分析揭示的假设违规通过提出的新架构得到修复： - 满足所有声明 - 满足所有假设 - 编码为形式化的验证论证

工具网站：https://acps-sei.github.io/tools/sar