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

【文章頁數(shù)】：79 頁

【學(xué)位級別】：碩士

【部分圖文】：

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

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

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

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

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

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

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

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

本文編號：3978633