隨著計算機系統(tǒng)規(guī)模的迅速增大,系統(tǒng)設計實現的正確性問題越來越嚴峻。形式化方法的出現,成為了解決該問題的一個重要手段。它運用數學方法的特點相比于傳統(tǒng)的模擬和測試具有更高的可靠性和良好的完備性。其中,定理證明的方法因其既能驗證系統(tǒng)規(guī)范又不受系統(tǒng)規(guī)模的限制而備受關注。遺傳算法被越來越多的應用在安全性要求較高的領域,然而定理證明器中還未有形式化的遺傳算法,這就限制了形式化方法在相關領域的應用。因此,將遺傳算法形式化在HOL4系統(tǒng)中對擴展定理證明方法的應用領域具有重要的研究意義和實用價值。眾所周知,遺傳算法的求解能力取決于最關鍵的操作——交叉算子。因此,本文對應用最多的單點交叉和多點交叉進行了形式化。首先,本文采用高階邏輯的方法對交叉算子進行了形式化分析,從而定義交叉算子生成子代的過程為交叉操作。通過對交叉操作的形式化抽象,提取了交叉操作的基本組成元素。這些基本元素組成了交叉操作的一般化模型,并使用高階邏輯表示基本組成元素�；谝话慊Y構模型,使用雙遞歸的方法提出了交叉操作的形式化模型,并用數學的方法描述了此模型。然后,使用形式化的交叉操作分別完成了單點交叉算子和多點交叉算子的形式化,并使用支持...

【文章頁數】：79 頁

【學位級別】：碩士

【部分圖文】：

圖２－１形式化??Ｆｉ．２－１?Ｆｏｒｍａｌｉｚａｔｉｏｎ??

所謂形式化，在邏輯學中首先要分析某一對象的組成部分及它們之間的聯結關??系，然后對研究對象進行抽象并提取它的形式結構，最后用一種符號語言來表示此形??式結構，如圖２－１所示。形式化從邏輯學理論發(fā)展到計算機應用，也就從符號語言描??述過渡到了使用特定工具表示的階段。因此，在計算機領....

圖２－３形式化驗證的主要方法??－

系統(tǒng)實現??正確／錯誤？??圖２－２系統(tǒng)規(guī)范和形式化驗證的關系??Ｆｉｇ．２－２?Ｔｈｅ?ｒｅｌａｔｉｏｎ?ｂｅｔｗｅｅｎ?ｓｙｓｔｅｍ?ｓｐｅｃｉｆｉｃａｔｉｏｎ?ａｎｄ?ｆｏｒｍａｌ?ｖｅｒｉｆｉｃａｔｉｏｎ??圖２－３為形式化驗證目前主要使用的三種方法。下面將對它們的基本原....

圖２－２系統(tǒng)規(guī)范和形式化驗證的關系??

圖２－２系統(tǒng)規(guī)范和形式化驗證的關系??Ｆｉｇ．２－２?Ｔｈｅ?ｒｅｌａｔｉｏｎ?ｂｅｔｗｅｅｎ?ｓｙｓｔｅｍ?ｓｐｅｃｉｆｉｃａｔｉｏｎ?ａｎｄ?ｆｏｒｍａｌ?ｖｅｒｉｆｉｃａｔｉｏｎ??圖２－３為形式化驗證目前主要使用的三種方法。下面將對它們的基本原理、優(yōu)勢??與不足和目前面臨....

圖２－５模型檢測的過程??Ｆｉｇ．２－５?Ｐｒｏｃｅｓｓ?ｏｆ?ｍｏｄｅｌ?ｃｈｅｃｋｉｎｇ??

?錯誤?＜給出反例３??圖２－４等價性檢驗的過程??Ｆｉｇ．２－４?Ｐｒｏｃｅｓｓ?ｏｆ?ｅｑｕｉｖａｌｅｎｃｅ?ｃｈｅｃｋｉｎｇ??設計錯誤不僅僅出現在系統(tǒng)轉換前后，還有一類需要關注的錯誤是出現在系統(tǒng)實??現上。模型檢測是驗證對象本身實現的正確性，它用有限狀態(tài)機表達系統(tǒng)，系統(tǒng)性....

本文編號：3978633