Soter：使用“运行保证” 编程安全机器人系统

编辑部编译

如今，得益于技术的不断进步和成熟，机器人系统的应用越来越普遍，但人们对于机器人系统的高要求无形中也增加了系统的复杂度。然而，形式验证和系统测试的进步速度与复杂度的增加速度并不成正比。那么，我们该如何确保机器人系统的安全性呢？最近，伯克利加州大学的Ankush Desai、Shromona Ghosh、Sanjit A. Seshia、Natarajan Shankar和Ashish Tiwari等研究人员针对这一问题进行研究，提出了运用“运行保证”技术来解决这一问题。

随着技术的成熟，机器人系统在社会中发挥着越来越多的安全性、关键性作用，比如，交付系统、监视系统，以及个人交通等。与此同时，这种对于自动化的追求趋势也导致了系统复杂程度的不断提高，包括高级数据驱动的机器学习组件的集成。然而，形式验证（formal verification）和系统测试的进步尚未能够跟上日益增加的复杂度。此外，机器人系统对第三方现成组件和机器学习技术的依赖性预计会增加，这将导致正在部署的系统的复杂性，与通过形式验证获得安全性和正确性认证的系统之间的差距越来越大。

弥合这一差距的一种方法是利用运行保证（run-time assurance，RTA）技术，其中，设计时的验证结果可用于构建一个系统，该系统在运行时监控自身及其环境，并切换到可证明安全性的运行模式，有可能性能较低，且会牺牲某些非关键性的目标。运行保证（RTA）框架的一个突出例子是单纯形架构（Simplex Architecture），已被用于构建具有一定正确性的安全关键航空电子设备、机器人和网络物理系统。Simplex架构将一个未经认证的高级控制器（AC）与一个经过认证的正确安全控制器（SC），以及决策模块（DM）相结合，其中DM的作用是在AC和SC之间切换，以使整个系统保持安全。然而，RTA之前的大多数应用，在设计用于这种系统的定时和通信行为时，不提供高级语言支持，用于以一种模块化方式构造可证明安全性的RTA系统。以往的技术要么将RTA应用于系统中的单个不可信组件，要么将大型单片系统包装到Simplex的单一实例中，而这使得相应的SC和DM的设计和验证变得困难或不可行。Schierman等人对如何在无人驾驶飞机系统的软件堆栈的不同级别上使用RTA框架进行了研究。在最近的一项研究中，Schierman等人提出了一种基于组件的单纯形架构（CBSA），它将假设保证合同（assume-guarantee contracts）与RTA相结合，以确保基于组件的网络物理系统运行时的安全性。然而，为了便于构建RTA系统，需要一种通用编程框架，用于构建具有运行保证的、可证明安全性的机器人软件系统，且该系统还考虑诸如定时和通信的实现方面。

在本文中，我们试图使用Soter来解决这一需求，Soter是一个使用运行保证构建安全机器人系统的编程框架。Soter程序是周期性过程的集合，称为节点，它使用一个“发布—订阅”的通信模型进行交互。Soter中的RTA模块由一个高级控制器节点、一个安全控制器节点和一个安全规范组成，如果模块格式良好，则框架提供一个系统满足安全规范的保证。Soter使得程序员能够以声明的方式构建一个具有指定时序行为的RTA模块，将可证明安全性的操作与安全时使用AC的特征相结合，以实现良好的性能。我们的评估表明，Soter能够有效地实现这种安全性和性能的融合。

Soter采用了用于将整个RTA系统的设计和验证分解为单个RTA模块的结构，同时保证了整个复合系统的安全性。Soter包括一个编译器，它能够生成实现切换逻辑的DM节点，并生成C代码，以便在诸如机器人操作系统（ROS）和MavLink等常见的机器人软件平台上执行。

我们通过构建一个安全的自主无人机监控系统对Soter框架的有效性进行评估。我们展示了Soter可用于构建一个由第三方不可信组件和复杂机器学习模块组成的复杂机器人软件堆栈，并且仍然能够提供系统范围内的正确性保证。生成的机器人软件代码已经在实际无人机平台（3DR无人机）和模拟（使用ROS/Gazeb和OpenAI Gym）上进行了测试。我们的测试结果表明，使用Soter构建的受RTA保护的软件堆栈，可以在使用不安全的第三方控制器的时候，以及在高级控制器中使用故障注入引入bug的时候，确保无人机的安全性。

总而言之，我们的论文做出了以下新颖的贡献：

1.一个基于Simplex的运行保证系统的编程框架，为安全机器人系统的模块化设计提供了语言原语；

2.一个基于可达集计算的理论形式，使得系统能够保持可靠安全性，同时保持安全和高级控制器之间的平滑切换行为；

3在模拟和实际无人机平台上的实验结果表明，在存在不可信或未经验证的组件的情况下，Soter是如何用于保证系统的正确性的。

运行保证的体系结构

图1显示了由三个子组件组成的RTA架构（类似于Simplex）：（1）在正常操作条件下控制机器人的高级控制器（AC），并且旨在實现涉及特定度量（例如，成本和时间）的高性能。AC针对性能进行了优化，并且没有附带安全证书。（2）安全控制器（SC），可以进行预先认证，以使得机器人保持在工厂/机器人的安全操作区域内运行。（3）经过预先认证（或自动合成为正确）的决策模块（DM），以定期监视工厂的状态，并确定何时从AC切换到SC，以确保系统保持在安全区域内。

当AC控制系统时，DM每隔Δ周期对系统状态进行监视（采样），以检查系统是否能够在时间Δ内违反预期的安全规范（φ）。如果是，则DM切换控制到SC。我们将DM从AC切换到SC的条件作为切换条件。

案例研究：无人机监控系统

在本文中，我们考虑建立一个监视系统，其中，自主无人机必须安全地在城市中巡逻。图2a（顶部）显示了来自Gazebo模拟器的工作空间快照。图2a（底部）显示了工作空间的障碍物图，所有障碍物（房屋、汽车等）都是静态的。

图2b显示了无人机监控系统的软件堆栈。应用层实现监视协议，该协议确保应用特定属性（φapp），例如，必须经常性地访问所有监视点。软件堆栈的通用组件包括运动规划器和运动原语。该应用程序为无人机生成下一个目标位置。运动规划器对运动计划进行计算，该运动计划是从当前位置到目标位置的一系列路标点。图2a（底部）中的w1…w6，表示由运动规划器生成的运动计划，虚线表示无人机的参考轨迹。在接收下一个路标点上的运动原语模块生成所需的低级控制，以密切跟踪参考轨迹。图2a（底部）中的轨迹表示无人机的实际轨迹，由于潜在的动力学、干扰等因素，它偏离了参考轨迹。

用于安全运动规划器的RTA

我们使用的是OMPL，这是一个第三方运动规划库，它实现了许多最先进的基于采样的运动规划算法。我们使用来自OMPL的RRT算法为我们的监控应用程序实现了运动规划器。

总而言之，我们使用格式良好的RTA模块理论构建了三个RTA模块：运动原语、电池安全性和运动规划器。受RTA保护的软件堆栈（图2c）是三个模块的组合，在研究中，很多受RTA保护的软件堆栈中的软件进行了循环仿真。我们还将生成的代码在真正的无人机上进行了部署，以进行类似的实验。

相关研究

在这篇文章中，我们对此次的研究进行了详细的概述。可以说，单纯形架构除了广泛用于航空电子和机器人领域外，在其他领域也有着广泛的应用。D.Phan、J.Yang等人提出了基于组件的单纯形架构和A-G合同，用于自动确定开关逻辑并在需要时执行协调切换。在本文中，我们使用这些原理在Matlab中为QuickBot设计原型软件堆栈。从文中，我们可以获得一些灵感，并从以下两个问题的解决中为以后的研究奠定了基础：（1）我们提出了一个用于组合性构建系统的编程框架，以便整个系统的安全问题可以分解为由单一模块保证的RTA不变量。（2）我们使用该框架来构建安全的无人机任务。一个重要的区别是，我们使用φsafer来确保系统的高性能行为。在《用于网络物理系统的沙箱控制器》中，作者将Simplex方法应用于沙箱网络物理系统，并提出了一种基于自动可达性的方法来推断切换条件。

我们将一个通用运行保证架构进行了形式化，并在移动机器人系统的编程框架中实现它。安全关键系统的安全控制是一个非常活跃的研究领域。可达性（Reachability）分析经常用于研究控制系统的安全性。在正常条件下使用高级控制器（AC）的想法得到了研究人员的关注，在边界处，使用最佳安全控制（SC）来保持安全性已经用于在现实世界中操作四旋翼飞行器。我们可以使用这些方法来设计SC，并且在某些情况下，可以使用我们的框架来构建那些已经使用切换逻辑的系统。

运行验证已应用于机器人中，其中，监视器用于检查路径规划器和任务执行的状态。在本文中，我们实现了一个基于运行保证的编程框架，该框架支持复原以確保在现实世界中安全执行机器人系统。最近，ModelPlex将CPS模型的离线验证与系统执行的运行验证相结合，以便通过构造运行监视器来构建正确的模型，从而为运行时的CPS执行提供正确的保证。虽然ModelPlex的目标与我们的RTA框架相似，但它在两个方面有所不同：（1）它依赖于可用模型的完整知识（或在我们的情况下是Nac）；（2）虽然它将切换条件综合到Nsc，但它没有提供Nac可以接管控制的条件，即它们不构建φsafer。未来，对于这项研究，我们还会继续探索。