技术摘要：ACCESS —— 安全关键系统的保证案例中心化工程

1. 问题陈述

安全关键系统需要对其在定义语境下的运行安全性进行明确的证明。传统上，保证案例（由证据支持的论证）是手动创建的文档，通过冗长且易出错的过程进行评估。随着系统变得更加复杂且相互连接，管理开发生命周期（包括验证、确认以及跨异构工程工件的变更影响分析的协调）变得日益困难。

此外，机器人与自主系统 (RAS) 的出现引入了传统保证方法无法解决的挑战。RAS 通常是开放且具有适应性的，要求其保证案例能够在系统运行生命周期内以极少的人为干预进行演进。现有方法论缺乏足够的基于模型的理论基础来实现以下目标：

1. 将保证案例系统地追溯到多样化的工程工件（例如：架构模型、安全分析、行为模型）。
2. 自动评估保证案例及其引用的工件。
3. 将安全保证活动从开发阶段转移到运行时，以应对动态环境。
4. 将形式化方法的结果直接集成到保证论证中。

现有的符号体系（如 GSN 和 CAE）本身并不原生支持实现自动化、连贯的保证所需的对外部工件的追溯性。

2. 方法论：ACCESS

本文提出了 ACCESS（保证案例中心化的安全关键系统工程），这是一种围绕演进式的、基于模型的保证案例来开发安全关键系统的工程方法。ACCESS 采用了基于模型的系统工程 (MBSE) 原则，将模型视为一等公民工件。

该方法论由七个迭代步骤组成，协调了系统开发与系统保证活动：

• 第 1 步：规划保证案例： 定义系统功能、硬件平台和环境假设。进行高层安全分析（如 HARA）以导出初步的安全目标。
• 第 2 步：创建保证案例： 对系统架构进行建模并指定模块化的保证案例模块。为分配的需求生成公开主张（Public Claims），并为同级子系统定义假设。
• 第 3 步：细化保证案例： 进行子系统安全分析（如 FMEDA）并将需求分配至子系统。开发每个子系统的安全论证，并保持与需求的追溯性。
• 第 4 步：验证与确认工程工件： 创建具有形式语义的行为模型（如状态机）。进行模型分析与验证，以确保满足需求并维持模型完整性（例如：无死锁）。
• 第 5 步：评估保证案例： 实现系统并进行系统级的验证与确认。对保证案例进行整体评估，未得到支持的主张将触发对前序步骤的重新评估。
• 第 6 步：转换为动态保证案例： 对于 RAS，将特定部分的保证案例转换为“动态”形式。这涉及定义将运行数据驱动程序（Runtime Data Drivers）与工程模型相连，使保证案例能够反映系统的当前状态。
• 第 7 步：自动化运行时评估： 利用运行时数据对动态保证案例进行非侵入式的、自动化的周期性评估。如果有效性丧失，系统可以过渡到安全状态。

3. 工具支持：ACME

为了支持 ACCESS，作者开发了 保证案例管理环境 (ACME)。ACME 是一个基于 Eclipse 建模框架 (EMF) 和结构化保证案例元模型 (SACM) 构建的模型驱动框架。

ACME 的核心能力包括：

• 追溯性： 实现从保证案例元素（目标、解决方案、语境）到异构工程工件（EMF 模型、Excel 表格、Isabelle 理论文件）的细粒度追溯。
• 自动化验证： 执行模型查询（使用 Epsilon 对象语言 - EOL）以验证工程工件是否符合保证案例的约束。
• 形式化集成： 连接至 Isabelle/HOL 服务器，以验证形式化理论（例如：死锁自由证明），并生成用于逻辑完整性检查的 Isabelle/SACM 形式化保证案例表示。
• 动态保证： 支持 运行时数据驱动程序 和 动态安全管理系统 (DSMS)，用于将运行时数据与保证模型同步，并执行持续评估。

4. 案例研究与结果

该方法论及工具被应用于一个涉及 自主水下航行器 (AUV) 的案例研究。该 AUV 的安全控制器（最后响应引擎 - LRE）是使用 RoboChart（一种具有形式 CSP 语义的图形化语言）进行建模的。

案例研究的关键发现：

• 追溯性： 团队成功地将安全论证追溯到了 Excel 表格中的 FMEDA 结果、RoboChart 行为模型以及 Isabelle 形式化证明。
• 自动化： ACME 自动执行了针对 Excel FMEDA 数据的验证规则，并调用 Isabelle 服务器来检查形式化证明。模型中的错误（例如：缺失的转换或失败的证明）会在保证案例编辑器中被立即标记。
• 运行时适应性： LRE 保证案例被转换为动态形式。运行时传感器数据（障碍物探测）被同步到模型中，并通过验证规则检查传感器读数是否保持在安全范围内。
• 效率评估： 研究人员针对一个电源单元（系统 A）和一个导航单元（系统 B）进行了对比实验，使用了三种方法：
  1. 手动（基于文本）。
  2. 不使用 ACME 的基于模型的方法。
  3. 使用 ACME 支持的基于模型的方法。
  • 结果： 手动方法耗时显著较长（例如：系统 A 约为 505 分钟），且无法支持运行时保证。不使用 ACME 的基于模型方法减少了时间（约 262 分钟）。使用 ACME 支持的方法效率最高（系统 A 约为 87 分钟），证明了开发工作量的实质性减少。
• 可扩展性： ACME 成功处理了包含约 5,689 个元素的模型。然而，可扩展性测试表明，当模型元素数量达到百万级时会出现内存溢出问题，这是由于需要在查询时将整个 EMF 模型加载到内存中所致。

5. 重要性与贡献

本文声称的主要贡献如下：

1. ACCESS 方法论： 一种以演进式保证案例模型为中心的关键系统工程方法，弥合了开发阶段与运行时保证之间的鸿沟。
2. 自动化评估： 一个可在开发阶段和运行时评估保证案例及其引用工程工件的框架，并由原型动态管理系统提供支持。
3. 形式化集成： 提供了将多样化的形式化验证结果（如来自 Isabelle）集成到保证案例中，并自动生成用于定理证明的（Isabelle/SACM）形式化保证案例的功能。
4. 变更影响分析： 自动分析工程工件的变化如何影响保证案例。
5. 实际应用： 通过 AUV 案例研究成功应用了上述内容，证明了基于模型且以保证为中心的工程的可行性。

作者强调，ACCESS 使安全保证能够从静态的、基于文档的保证转向动态的、模型驱动的保证，这对于在不确定环境中运行的自适应 RAS 的安全性至关重要。他们指出，尽管该方法提高了效率和覆盖范围，但未来仍需解决可扩展性限制问题，并降低定义验证规则的技术门槛（例如：通过支持受限自然语言）。