Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

在机器人领域，构建一台能够移动且具备思考能力的机器已经足够困难。而构建一支能够协同工作且互不碰撞的机器人团队，则是另一种完全不同的挑战。这些机器通常被称为自主移动机器人，它们旨在现实环境中导航，在尝试到达特定目的地时避开墙壁、人员以及彼此。运行它们的软件极其复杂，依赖于来自激光等传感器的持续数据流，以了解它们所处的位置及周围环境。由于这些机器人是在连续的物理世界中运行的，它们的运动是平滑且流动的，其变化以微秒和毫米为单位。然而，控制它们的计算机却是以离散的步骤进行思考的，即以不连续的时间块处理信息。这种物理世界的平滑性与代码逻辑的阶梯性之间的鸿ب，造成了一个危险的盲点。如果软件没有经过完美调试，机器人可能会移动得过快，导致传感器无法捕捉到障碍物，或者两台机器人可能在同一时刻到达同一个交叉路口，从而导致双方都无法移动的死锁状态。

为了解决这个问题，研究人员需要一种方法，在真实机器启动之前，测试机器人团队可能面临的所有可能场景。这就是“形式化验证”（formal verification）这一领域的用武之地。形式化验证并非仅仅运行几次模拟并寄希望于结果，而是利用数学逻辑来检查系统可能采取的每一条路径。它提出了一个简单而强大的问题：是否存在任何可能的事件序列，无论多么罕见，会导致系统失效？对于机器人团队而言，这意味着证明它们永远不会发生碰撞，永远不会陷入永久停滞，并且始终能够到达目标。挑战在于，真实的机器人是在连续世界中移动的，而这些数学证明则要求将世界分解为固定的步长网格。如果步长太大，证明过程会遗漏细小但关键的事故；如果步长太小，计算机则会被庞大的可能性数量所压垮，无法完成计算。

来自瑞典马拉德伦大学（Mälardalen University）和皇家理工学院（KTH Royal Institute of Technology）的研究小组开发了一种弥合这一差距的新方法。他们创建了一个系统，允许工程师使用一种名为 Timed Rebeca 的专门建模语言来设计多机器人团队，该语言将每台机器人视为一个对消息做出反应的独立参与者。随后，该模型由计算机进行严格检查以确保安全性。至关重要的是，该团队使用名为 ROS2 的标准系统编写了机器人的实际软件，从而确保数学模型与实际代码完全一致。他们不仅仅是在模拟机器人，而是构建了一个既足够抽象以供计算机检查，又足够详细以反映机器真实物理特性的模型版本。通过这种方式，他们能够预测标准模拟往往会忽略的罕见且危险的故障。

研究人员专注于一个涉及五台机器人在 50x50 网格（空间大小约等于一个大型仓库地面）上移动的情景。他们设置了一个复杂的环境，机器人必须在绕过障碍物的同时穿越彼此的路径以到达目标。在现实世界中，这些机器人使用激光扫描仪检测物体，每秒进行数百次测量。团队必须研究如何将这些连续的激光束和流畅的运动转化为计算机检查逻辑所需的离散步骤。他们发现，机器人的移动速度与其扫描周围环境的频率之间存在严格的关系。如果机器人移动过快，它可能会在传感器注意到障碍物之前就走完了两次扫描之间的整个距离。研究人员证明，为了使模型准确，必须限制机器人的速度，使其跨越一个网格单元的时间不能快于传感器更新的时间。这一源自信号处理基本原理的规则，确保了数字模型不会遗漏任何潜在的碰撞。

为了使计算机检查变得可行，团队必须在不丢失问题真相的前提下简化世界。他们不是将机器人表示为平滑的形状，而是表示为从一个方格单元移动到另一个单元、并以 45 度增量转弯的矩形。他们根据机器人的速度和单元格的大小计算了在这些单元格之间移动所需的时间。他们还预先计算了复杂的三角函数值（如正弦和余弦），并将它们存储在查找表中，这样计算机就不必每次都从头开始计算。这些优化使得模型检查器能够在几分钟内探索数百万种状态。当他们运行检查时，计算机可以绝对确定地告诉他们，一组特定的规则是否会导致碰撞或安全到达。

他们的实验结果非常显著。在机器人被设定为具有安全速度和变化等待时间的情况下，模型检查器确认所有五台机器人都会在不发生碰撞或死锁的情况下到达目的地。随后，研究人员在模拟中运行了实际的 ROS2 代码，机器人表现得与模型预测的完全一致，成功地在拥挤的空间中导航。然而，当他们改变参数以创造危险情况时——例如让所有机器人以完全相同的速度移动，或将扫描频率设置得过低以不匹配速度时——模型检查器立即发现了缺陷。它识别出了一个会导致碰撞的具体事件序列。当他们在这些相同的危险设置下运行实际代码时，模拟崩溃的方式与模型预测的完全相同。在一项测试中，模型在仅探索了几千个状态后就发现了碰撞，而实际模拟在五次运行中有三次失败，证实了这种危险是真实存在且可预测的。

该研究还强调了时机的重要性。在一种情景中，研究人员将机器人的移动速度设定为刚好略快于传感器更新频率。模型检查器发现，这种对安全规则的轻微违反使得碰撞几乎不可避免，无论机器人如何编程以避开彼此。计算机显示，机器人会在一个交叉点同时到达，由于它们无法及时看到对方，因此会发生碰撞。实际模拟证实了这一点，机器人在每一次运行中都未能成功避让。这表明该模型不仅是一个理论练习，更是一个能够捕捉到人类工程师可能忽视的微妙且危险错误的实用工具。

研究人员承认，他们的方法存在局限性。目前的方法要求工程师手动构建数学模型和实际代码，这是一个耗时的过程，可能会引入人为错误。他们还指出，虽然他们的系统可以处理在 50x50 网格上的五台机器人，但如果要扩展到一百台机器人或更大的地图，会迅速压垮计算机的内存。瓶颈在于机器人可能采取的路径总数；随着机器人数量和地图规模的增加，组合数量增长极快，导致计算机因空间不足而无法存储。尽管存在这些限制，这项工作证明了创建一个既足够简单以便检查，又足够精确以值得信赖的复杂机器人系统“数字孪生”是可能的。

这项研究为开发安全的自主系统提供了一条新路径。通过将机器人软件的设计视为首先构建并验证数学模型的过程，工程师可以在制造或部署单台机器人之前识别出致命缺陷。团队展示了通过在模型的详细程度与计算效率之间进行仔细平衡，验证多机器人系统在现实世界中能否安全运行是完全可行的。他们的工作表明，机器人技术的未来不仅在于制造更智能的机器，更在于建立更好的方法，以证明在关键时刻这些机器不会失效。