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

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

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