隨著計(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é)中[1],即系統(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ì)于不同拓?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è)和自動(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è)比較系統(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.在研究了自穩(wěn)定算法在分布式系統(tǒng)以及通信協(xié)議中的應(yīng)用的基礎(chǔ)上,指明了今后可能的研究方向和研究課題。
【學(xué)位單位】：上海交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位年份】：2009
【中圖分類】：TP338.8
【部分圖文】：

任務(wù)能夠由一個(gè)進(jìn)程或者一個(gè)線程實(shí)現(xiàn)。圖中的分布式應(yīng)用程序有三分組成，盡管程序 3 的任務(wù) A 和任務(wù) D 在相同的計(jì)算機(jī)上，但是它們；因?yàn)樗鼈冇蓛蓚�(gè)分離的處理器執(zhí)行。并行程序中的任務(wù)比分布式程序合得更緊密，通常與分布式程序關(guān)聯(lián)的處理器在不同的計(jì)算機(jī)上，但是關(guān)聯(lián)的處理器在相同的計(jì)算機(jī)上。

學(xué)位論文 第三章 自穩(wěn)定算法的，我們將給出具體的證明。同時(shí)我們可以證明，整個(gè)算法需定狀態(tài)，具體的證明可以參考[9]。ijkstra在 1974年的同一篇文章中提出了另外兩個(gè)自穩(wěn)定算法，算法和三狀態(tài)自穩(wěn)定算法，具體在這里就不介紹了，可以參 提出的這三個(gè)自穩(wěn)定算法雖然比較簡(jiǎn)單，但是作為自穩(wěn)定性這些算法得到廣大學(xué)者的一致性認(rèn)同，并被后來的很多學(xué)者。

SPIN模擬和檢驗(yàn)的基本過程
【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 鄭紅軍;張乃孝;;軟件開發(fā)中的形式化方法[J];計(jì)算機(jī)科學(xué);1997年06期

2 廖宇,楊大軍;定理證明輔助工具PVS剖析[J];計(jì)算機(jī)工程;2000年09期

本文編號(hào)：2843544