Formal Verification of Node Communications in the Hybrid Robot Operating System RGMPROS
WANG Ya1，WANG Rui1，GUAN Yong1，WEI Hong-xing2，LI Xiao-juan1，ZHANG Jie3
1（Beijing Key Laboratory of Electronic System Reliability Technology，Capital Normal University，Beijing 100048，China）
2（School of Mechanical Engineering and Automation，Beijing University of Aeronautics ＆ Astronautics，Beijing 100191，China）
3（College of Information Science ＆ Technology，Beijing University of Chemical Technology，Beijing 100048，China）
Abstract：In the field of robot development，the software modularization problem of industry robot controllers can be solved by transplanting the robot operating system ROS to the Linux operating system.However，ROS running on the Linux operating system has no realtime performance，which cannot meet the needs of realtime control of robot motion.RGMPROS is a hybrid robot operating system applied on industry robot controllers and can solve the problem that ROS running on the Linux operating system has no realtime performance.So it is significant to verify the realtime performance of RGMPROS.This paper proposes to verify the node communications in the RGMPROS system using model checking.Firstly，timed automata of every part in communication process are modeled.Then properties of reachability of node communications and communication time are described as computational tree logic （CTL） formulas，and they are verified using the model checking tool Uppaal.The verification results show that the hybrid robot operating system RGMPROS has realtime performance and can meet realtime needs.
王亚,王瑞,关永,魏洪兴,李晓娟,张杰. RGMP-ROS混合机器人操作系统节点间通信的形式化验证[J]. 小型微型计算机系统, 2015, 36(10): 2379-2383.
WANG Ya,WANG Rui,GUAN Yong,WEI Hong-xing,LI Xiao-juan,ZHANG Jie. Formal Verification of Node Communications in the Hybrid Robot Operating System RGMPROS. Journal of Chinese Computer Systems, 2015, 36(10): 2379-2383.
2015, Vol. 36 
