From Offline Towards Real-Time Verification for Robot Systems

Robot systems have been widely used in industry and also play an important role in human social life. Safety critical applications usually demand rigorously formal verification to ensure correctness. But for the increasing complexity of dynamic environments and applications, it is not easy to build a comprehensive model for the traditional offline verification. In this paper, we propose RobotRV, the first data-centered real-time verification approach for the robot system. Within this approach, a domain-specific language named RoboticSpec is designed to specify the complex application scenario of the robot system, the data packets transmitted in the robot system, and the safety critical temporal properties. Then, we develop an engine to automatically translate the RoboticSpec model into a real-time verifier. The generated verifier serves as an independent plug-in component for the runtime verification of concerned temporal properties. We applied the proposed approach to a real robot system. As presented in experiment results, our method detected potential failures, and improved the safety of robot system.