RoboSimVer: A Tool for RoboSim Modeling and Analysis

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.