基于遺傳算法的水下群機(jī)器人路徑規(guī)劃算法的形式化驗(yàn)證.pdf

1、群機(jī)器人路徑規(guī)劃算法作為群機(jī)器人系統(tǒng)的基礎(chǔ)，一直是人們的研究熱點(diǎn)。基于遺傳算法的水下群機(jī)器人路徑規(guī)劃算法能夠?yàn)樗蚂o態(tài)環(huán)境中的多個(gè)機(jī)器人規(guī)劃路徑，該算法在說(shuō)明其設(shè)計(jì)正確性時(shí)只使用了三組測(cè)試數(shù)據(jù)，這并不能保證算法設(shè)計(jì)的絕對(duì)正確性。為了提高算法設(shè)計(jì)正確性的說(shuō)服力，確保所設(shè)計(jì)的算法能夠正確的為每一個(gè)機(jī)器人規(guī)劃出到達(dá)目標(biāo)的最短路徑，本文使用形式化方法中的定理證明在HOL4中對(duì)其進(jìn)行形式化驗(yàn)證。首先給出算法形式化的一般步驟，基于該步驟提出了基于遺

2、傳算法的水下群機(jī)器人路徑規(guī)劃算法的形式化模型，對(duì)算法實(shí)現(xiàn)進(jìn)行形式化建模，并給出算法規(guī)范。然后提出了算法的形式化驗(yàn)證框架，在該框架的指導(dǎo)下首先證明了與模型相關(guān)的97條定義及性質(zhì)以說(shuō)明所建模型的合理性和有效性，接著給出了基于遺傳算法的水下群機(jī)器人路徑規(guī)劃算法的完整實(shí)現(xiàn)與規(guī)范的形式化描述，在此基礎(chǔ)上完成了“實(shí)現(xiàn)==＞規(guī)范”的證明。通過(guò)本文所提出的形式化模型和形式化驗(yàn)證框架，成功完成了對(duì)基于遺傳算法的水下群機(jī)器人路徑規(guī)劃算法的形式化建模及形式化