A framework of model checking guided test vector generation for the 6DOF manipulator

In designing robot control systems, simulation is still the primary approach to verifying the functions of circuit descriptions written in hardware design language. The validity of the verification depends on the coverage metric. But not all state spaces can be specified in a simulation. Model checking can overcome the shortcomings of simulation, because all of the state spaces can be traversed. Robot control system is an important part of the robot, used in the control of the manipulator to perform specific tasks. Therefore, in this paper a verification framework is presented for design correctness of robotic manipulator, which combines simulation and model checking. The framework is also applied to other control system or control hardware. Model checking guides the generating of test vectors, and makes the functional coverage reach 100% quickly. In this paper, a manipulator designed with six degrees of freedom is verified. The results of the verification of the manipulator show that the verification framework is effective for checking the design correctness of robotic manipulator.