Runtime Verification on Hierarchical Properties of ROS-Based Robot Swarms

Various robots are playing critical roles in many areas such as industrialmanufacturing, disaster rescuing, unmanned vehicle, and science exploration. Because of the uncertain environment, changed resource, or dynamic system structure at runtime, traditional methods such as testing, model checking, and static analysis used in the development stage are not enough to ensure that the executions of robot control software satisfy specified properties. In this paper, we propose a runtime verification approach calledRobotsMonitor on Multilayer (RMoM) based on robot operating system (ROS) for monitoring whether the running of a robot swarm violates given temporal properties. To monitor robot system in a comprehensive manner over multiple layers, RMoM unifies resource, communication, robot, and swarm properties into a systemic, hierarchical monitoring framework. A discrete-time Metric Temporal Logic (MTL3) RMoM is proposed for specifying properties with timed and parameterized characteristics in robot swarms. Then, the corresponding three-valued semantics is defined for MTL3-RMoM to generate impartial and anticipatory monitors. Moreover, a hierarchical monitoring specification language high-level specification language (HSL)-RMoM and a series of monitor construction algorithms are proposed to automatically generate monitors for MTL3-RMoM properties on ROS platform. The experiments show that the method can automatically generate the monitors for detecting properties of robot swarms.