Runtime Verification on Hierarchical Properties of ROS-Based Robot Swarms

Abstract

Various robots are playing critical roles in many areas such as industrial manufacturing, 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 called Robots Monitor 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 (MTL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">3</sub> ) RMoM is proposed for specifying properties with timed and parameterized characteristics in robot swarms. Then, the corresponding three-valued semantics is defined for MTL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">3</sub> -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 MTL <sub xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">3</sub> -RMoM properties on ROS platform. The experiments show that the method can automatically generate the monitors for detecting properties of robot swarms.