Model Checking for the Goal-Feedback-Result Pattern in ROS
Wei Wei, Xiaojuan Li, Yong Guan, Rui Wang, Qian Lu, Jie Zhang · 2019
Goal-Feedback-Result (GFR) pattern is widely used for the communication of multiple tasks processing and distributed control systems based on Robotics Operation System(ROS). With the more sensor devices and applications are deployed in service robots, it is getting more important to guarantee the correctness and reliability of structured GFR communication in ROS. Formal analysis and verification of GFR communication and scheduler of tasks in ROS are completed by model checking in this paper. The timed automaton of client process, server process and scheduler are designed for modelling the communication process and scheduling policy. The deadlock-free, schedulability and responsive properties, which are formally described in CTL(Computation Tree Logic) formulas, are verified automatically by model checker. The formal modelling analysis and verification of GFR pattern provide a refined design model and are helpful for avoiding subtle error or bug in early design stage of GFR based robotic system applications.