Formal Verification For Path Planning Of Underwater Swarm Robots Using Genetic Algorithm

Swarm robots path planning algorithm as the foundation of swarm robots system,it is the research focus of people for a long time.Path planning of underwater swarm robots using genetic algorithm that can plan a path for every robot in underwater static environment.Only three test datas were used to illustrate the correctness of the algorithm,this couldn't guarantee the design correctness of it.To enhance the correctness of the algorithm design,making every robot find the shortest path to arrive at the object,one of the formal method(i.e.theorem proving)is used to verify it formally by HOL4.In this paper,the general steps of algorithm formalization was presented firstly,according this steps,the model of formalization for path planning of underwater swarm robots using genetic algorithm was given,and formally modeled the implementation of the algorithm.At the same time,specifications of the algorithm were given.Next the frame of formal verification for the algorithm was presented,Under the guidance of the frame,97 definitions and properties related to the model were firstly proven to illustrate the rationality and effectiveness of the model.Then the formal description of the whole implementation and specification of the algorithm was given,on this basis,the proof of "implementation(?)specification" was completed.Through the formal model and the frame of formal verification presented in this paper,formal modeling and verification for the path planning of underwater swarm robots using genetic algorithm was completed successfully.It is not only deepen the understanding of the algorithm,but also proven the correctness of the algorithm design,that is,the shortest path to arrive at the object can be planned for each robot.Compared with the traditional verification methods,this improves persuasiveness of correctness of the algorithm design greatly.In addition,during the process of formal research for the algorithm,the theory of ternary relation in HOL4 is supplemented and the application scope of HOL4 is expanded.