基于断言的监控器的边缘-云协同编排，用于机器人应用

《ACM Transactions on Embedded Computing Systems》：Edge-Cloud Orchestration of Assertion-Based Monitors for Robotic Applications

运行时验证多域软件应用时面临计算开销大、资源受限等问题，本文提出基于信号时序逻辑（STL）的监控器自动合成框架，结合边缘-云动态迁移和Docker容器化实现验证过程优化，通过合成符合ROS规范的监控节点与分布式架构降低延迟，并在工业案例中验证了有效性。

　　

摘要

实现现代机器人行为的多域软件应用程序的运行时验证是一项具有挑战性的任务。一方面，基于断言的验证（ABV）在运行时检查复杂系统的正确性方面展现出了巨大潜力；另一方面，运行时ABV引入的计算开销可能相当大、具有不确定性且变化无常。因此，将精确的ABV应用于资源受限计算架构的自主机器人时，可能会导致软件执行速度严重下降以及时间约束的失败，从而影响整个系统的正确性。为应对这一挑战，我们提出了一个运行时ABV平台，该平台能够从信号时态逻辑断言中合成监控器，并实现监控器在边缘设备和云之间的动态迁移。合成的监控器被封装成符合ROS标准的节点，并连接到待验证的系统中。整个ABV框架及其相关的迁移机制随后使用Docker进行容器化，以适应边缘计算和云计算环境。为了评估所提出的平台，我们通过一组合成基准测试和一个工业案例研究展示了其效果，该案例研究涉及Robotnik RB-Kairos移动机器人在智能制造生产线中的任务。给实践者的提示：本文的出发点是对机器人系统软件进行精确且运行时验证的需求。智能系统的验证和确认往往是不完整的，因为它们无法预测所有潜在场景，包括错误或意外事件。此外，基于断言的验证也可能消耗大量资源；因此，需要谨慎使用资源，以避免监控器过度占用机器人的计算资源。为此，我们采用了信号时态逻辑这一被广泛接受的解决方案来监控机器人和分布式应用程序。本研究的主要贡献是一个能够自动合成与机器人操作系统（ROS）交互的监控器的框架，同时还具备通过利用分布式计算架构（即边缘-云架构）来优化运行时验证端到端延迟的能力。在未来的工作中，我们不仅会继续致力于最小化端到端延迟，还会研究监控器的时间上限，以实现运行时的确定性验证。