We present RoboSimVer, a tool for modeling and analyzing RoboSim Models. It uses a graphical modeling approach to model platform-independent simulation models of Robotics called RoboSim. For model analysis, we implemented a model-transformation approach to translate RoboSim models into NTA (Network of Timed Automata) and its stochastic version SHA (Stochastic Hybrid Automata) based on some patterns and mapping rules. RoboSimVer is able to get a simulation model. It also provides different rigorous verification techniques to check whether the simulation models satisfy property constraints. For experimental demonstrations, we adopt the case study Alpha algorithm for robotics. We use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our tool supports the verification of stochastic and hybrid systems. The demonstration video of the tool is available at https://youtu.be/mNe4q64GkmQ

Dehui Du

East China Normal University

Ana Cavalcanti

University of York

United Kingdom

JihuiNie

East China Normal University