發(fā)布時(shí)間：2024-05-19 23:47

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

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

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

【部分圖文】：

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

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

圖２－３形式化驗(yàn)證的主要方法??－

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

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

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

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

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

本文編號(hào)：3978633