一句话：提出 RoboSimVer 工具，将平台无关的机器人仿真模型转换为时间自动机网络及其随机版本以进行严格验证。
本文介绍 RoboSimVer，一个用于建模与分析 RoboSim 模型的工具。RoboSim 是一种图形化记法，用于描述平台无关的机器人系统仿真模型。为支持模型分析，作者实现了一种基于模式与映射规则的模型转换方法，将 RoboSim 模型翻译为时间自动机网络（NTA）及其随机版本。该工具以 RoboSim 仿真模型为输入，提供多种严格验证技术，检查仿真模型是否满足性质约束。实验以群体机器人中的 alpha 算法为例，使用抽象机器人平台模型描述不确定环境中的群体，展示工具对随机与混合系统验证的支持。演示视频见 youtu.be/mNe4q64GkmQ。
We present RoboSimVer, a tool for modeling and analyzing RoboSim models. It uses a graphical notation called RoboSim to describe platform-independent simulation models of robotic systems. For model analysis, we have implemented a model-transformation approach to translate RoboSim models into NTA (Network of Timed Automata) and their stochastic version based on patterns and mapping rules. RoboSimVer takes a RoboSim simulation model as input and provides different rigorous verification techniques to check whether the simulation models satisfy property constraints. For experimental demonstrations, we adopt the alpha algorithm for swarm robotics as a case study. We use an abstract robotic-platform model to describe a swarm in an uncertain environment and illustrate how our tool supports the verification of stochastic and hybrid systems. The demonstration video is at youtu.be/mNe4q64GkmQ.