摘要
为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力,使用定理证明对其进行形式化研究,给出算法在定理证明器HOL4中的形式化模型。基于算法形式化的一般步骤,对算法的设计进行了详细的分析,指出算法设计的核心步骤和建模难点。在此基础上建立了总体形式化建模框架,然后对其进行化简,得到种群初始化、选择、交叉三个核心模块。给出了模型中要用到的基本数据类型的形式化描述,并分别对三个模块进行形式化描述,最终得到算法的形式化模型。通过证明与模型相关的97条性质,说明了模型的合理性及有效性,在此模型的基础上,可以完成对算法的形式化验证,同时还能拓展HOL4的应用范围。
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.
作者
张杰
刘耕阳
关永
Zhang Jie;Liu Gengyang;Guan Yong(College of Information Science & Technology,Beijing University of Chemical Technology,Beijing 100029,China;College of Information Engineering,Capital Normal University,Beijing 100048,China)
出处
《计算机应用研究》
CSCD
北大核心
2019年第2期490-494,共5页
Application Research of Computers
基金
国家自然科学基金资助项目(61572331)
