一种水下群机器人路径规划算法的形式化研究.

To enhance the correctness of the path planning of underwater swarm robots based genetic algorithm, this paper used theorem proving to formalize it, and gave the formal model of it in HOL4. According to the general steps of algorithm formalization, this paper analyzed the design procedure of the algorithm in detail firstly. It pointed out the key step of the algorithm and the difficulty in formal modeling, and constructed the overall frame of formal modeling. Then, it got three core modules of population initializing, selection and crossing by decomposing the algorithm. Finally, it formalized the three core modules separately after formalized the basic data types, which would be used in formal model, and got the formal model of the algorithm. By proving the 97 properties related to this model, this paper illustrates the rationality and effectiveness. Moreover, it carried out the formal verification of the algorithm, and also extended the application scope of HOL4. [ABSTRACT FROM AUTHOR]