期刊
IEEE TRANSACTIONS ON RELIABILITY
卷 69, 期 2, 页码 674-689出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TR.2019.2923681
关键词
Formal specification; monitor generation; robot operating system (ROS); robot swarm; runtime verification (RV)
类别
资金
- National Natural Science Foundation of China [61690203, 61532007]
- National Key Research and Development Program of China [2017YFB1001802]
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据