使用 Timed Rebeca 对 ROS2 多机器人系统进行建模与模型检测

论文提出用 Timed Rebeca 对 ROS2 多机器人系统进行建模与模型检测，将节点图、周期性物理信号和运动基元等时间相关行为映射为离散模型。针对连续动力学与离散模型之间的鸿沟和大状态空间问题，作者给出面向不同数据类型的离散化策略、抽象阈值与验证加速优化技术，并保持抽象模型与 ROS2 实现之间的双向流转。Rebeca 与 ROS2 代码库已开源，可作为研究与验证自主机器人系统的参考。