From Offline Towards Real-Time Verification for Robot Systems
National Natural Science Foundation of China 61303014 61572331 61472468 61373034 National Key Technology Research and Development Program 2015BAF13B01 National Key R D Plan 2017YFC0806700 2017YFB1301100 Beijing Municipal Science and Technology Commission LJ201607
Ieee Transactions On Industrial Informatics
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.
Locate the Document
Wang, R., Wei, Y., Song, H., Jiang, Y., Guan, Y., Song, X., & Li, X. (2018). From Off-line Towards Real-time Verification for Robot Systems. IEEE Transactions on Industrial Informatics.