基于PVS的自穩(wěn)定算法形式化分析.pdf

1、隨著計(jì)算機(jī)和網(wǎng)絡(luò)的發(fā)展，分布式系統(tǒng)的應(yīng)用也越來越廣泛，同時(shí)對(duì)系統(tǒng)容錯(cuò)性和健壯性的要求也越來越高。分布式系統(tǒng)的容錯(cuò)性和健壯性也稱為自穩(wěn)定性。1974年Dijkstra 首次把自穩(wěn)定性的概念引入了計(jì)算機(jī)科學(xué)中，即系統(tǒng)從任何初始狀態(tài)出發(fā)，總能在有限步內(nèi)到達(dá)一個(gè)合法狀態(tài)。自穩(wěn)定系統(tǒng)是能夠保證自穩(wěn)定性的分布式系統(tǒng)，它的研究是計(jì)算機(jī)科學(xué)與理論中比較前沿的領(lǐng)域之一。 自穩(wěn)定算法是作用在分布式系統(tǒng)上的算法，它能夠保證系統(tǒng)的容錯(cuò)性和健壯性。對(duì)于不

2、同拓?fù)浣Y(jié)構(gòu)的分布式系統(tǒng)，要設(shè)計(jì)不同的自穩(wěn)定算法來保證系統(tǒng)的自穩(wěn)定性。性能好的自穩(wěn)定算法需要經(jīng)過復(fù)雜的正確性驗(yàn)證才能應(yīng)用到實(shí)際中。自穩(wěn)定算法的驗(yàn)證有多種方法，包括數(shù)學(xué)分析、定理證明、形式化分析等。 形式化方法是基于數(shù)學(xué)的方法來描述目標(biāo)軟件系統(tǒng)屬性的一種技術(shù)，它可以用來檢測(cè)軟件的可靠性和正確性。許多計(jì)算機(jī)科學(xué)家都認(rèn)為，采用形式化方法對(duì)系統(tǒng)進(jìn)行形式化驗(yàn)證和分析是構(gòu)造可靠安全軟件的一個(gè)重要途徑，而原型驗(yàn)證系統(tǒng)PVS 就是著名的模型檢測(cè)和

3、自動(dòng)化驗(yàn)證工具之一。 PVS為開發(fā)形式化規(guī)范和分析驗(yàn)證提供了一個(gè)集成化環(huán)境，它既有強(qiáng)有力的機(jī)器推理支持，規(guī)約語言，又有足夠豐富的表達(dá)手段，為算法的形式化驗(yàn)證提供了很好的驗(yàn)證工具和證明系統(tǒng)。本文主要使用PVS 自動(dòng)驗(yàn)證工具對(duì)自穩(wěn)定算法進(jìn)行形式化分析和驗(yàn)證，主要的研究成果和創(chuàng)新如下： 1. 在形式化分析和驗(yàn)證方面，本文使用PVS 自動(dòng)化驗(yàn)證工具對(duì)自穩(wěn)定算法進(jìn)行形式化建模和分析驗(yàn)證，完善地證明了自穩(wěn)定系統(tǒng)的基本性質(zhì)并提出了一個(gè)

4、比較系統(tǒng)的形式化驗(yàn)證方法。 2. 在算法的設(shè)計(jì)方面，本文的主要工作是在研究和總結(jié)前人工作的基礎(chǔ)上，提出了自穩(wěn)定算法設(shè)計(jì)的基本方法和原則。 3. 本文從實(shí)踐的角度出發(fā)，在試驗(yàn)的基礎(chǔ)上對(duì)原型驗(yàn)證系統(tǒng)PVS做了非常全面的說明和分析，并指明了PVS 存在的缺陷以及需要的改進(jìn)的地方。 4. 深入剖析和比較了形式化分析領(lǐng)域中各種自動(dòng)化驗(yàn)證工具的優(yōu)缺點(diǎn)，并提出了比較理想的自動(dòng)化驗(yàn)證工具的設(shè)計(jì)思想和實(shí)現(xiàn)。 5. 在研究了