Formal verification of a collision-free algorithm of dual-arm robot in HOL4

Possessing two manipulators heightens the ability of dual-arm robots (DAR) to conduct complex tasks, while raising hazard that the two manipulators might collide with each other or with other objects. DARs are usually equipped with a collision-free motion planning algorithms (CFMPA) to prevent the two manipulators from colliding. The CFMPA searches the motion paths of robot manipulators, which are expected to be as short and smooth as possible under the premise of ensuring safety. It is important to ensure that the algorithm is correct and efficient. It is not enough to apply traditional test methods to determine whether DARs can work in safety-critical applications. In this paper, theorem proving technology is employed to analyze the correctness and efficiency of a classical CFMPA. The CFMPA is outlined, and then formalized in high order logic with the theorem prover HOL4. An inconsistency in the range of motions of the robot manipulators in the algorithm is discovered. An improved algorithm is therefore proposed. Formal verification with HOL4 proves the correctness and efficiency of the proposed algorithm that has already run on a real DAR as well, in conformity with our expectation.