【摘要】：隨著系統(tǒng)設(shè)計(jì)復(fù)雜度的提高,設(shè)計(jì)驗(yàn)證已成為系統(tǒng)設(shè)計(jì)的瓶頸;傳統(tǒng)驗(yàn)證技術(shù)已不能滿足需要,形式化驗(yàn)證技術(shù)是適應(yīng)這種需求而產(chǎn)生的新技術(shù)。形式化驗(yàn)證方法包括算法驗(yàn)證、屬性驗(yàn)證和等價(jià)性驗(yàn)證等方法。論文的研究領(lǐng)域?yàn)閷傩则?yàn)證。屬性驗(yàn)證又包括定理證明、語(yǔ)言包含、符號(hào)模型檢測(cè)等方法。常見(jiàn)的符號(hào)模型檢測(cè)器有CTL模型檢測(cè)器如SMV驗(yàn)證工具;LTL模型檢測(cè)器如SPIN驗(yàn)證工具。 SPIN這一軟件驗(yàn)證工具,是于1989年由貝爾實(shí)驗(yàn)室J.Holzmann等開(kāi)發(fā)的模型檢測(cè)器。主要面向分布式軟件和協(xié)議系統(tǒng)的驗(yàn)證。SPIN使用PROMELA作為驗(yàn)證的模型語(yǔ)言,并使用線性時(shí)態(tài)邏輯(LTL)公式描述屬性,應(yīng)用自動(dòng)機(jī)理論實(shí)現(xiàn)系統(tǒng)的模擬運(yùn)行和正確性驗(yàn)證。 SPIN對(duì)系統(tǒng)的驗(yàn)證過(guò)程是首先用PROMELA語(yǔ)言建立系統(tǒng)的狀態(tài)機(jī)模型,然后抽象出用LTL公式表示的系統(tǒng)需求屬性的形式化描述,系統(tǒng)的正確性需求屬性也可以在PROMELA中通過(guò)特殊標(biāo)記來(lái)描述。驗(yàn)證的目標(biāo)是判斷系統(tǒng)模型與其抽象屬性是否相符。 SystemC~(FL)是基于進(jìn)程代數(shù)ACP的SystemC語(yǔ)言的形式化語(yǔ)言。既表示了SystemC模型的語(yǔ)義,又是對(duì)SystemC模型中進(jìn)程的行為分析。SystemC~(FL)的目的是對(duì)SystemC設(shè)計(jì)的形式化描述以及SystemC進(jìn)程的形式化行為分析。SystemC~(FL)可對(duì)各種各樣的系統(tǒng)建模(有限狀態(tài)系統(tǒng)、實(shí)時(shí)系統(tǒng)等)。 為驗(yàn)證SystemC~(FL)建模的并行及硬件系統(tǒng),選擇SPIN模型檢測(cè)器作為驗(yàn)證工具。論文中通過(guò)將硬件系統(tǒng)的SystemC~(FL)模型轉(zhuǎn)換成PROMELA模型,然后用SPIN驗(yàn)證工具對(duì)模型進(jìn)行驗(yàn)證。通過(guò)論文中研究的驗(yàn)證方法,可以在一定程度上實(shí)現(xiàn)應(yīng)用SPIN模型檢測(cè)器對(duì)硬件系統(tǒng)設(shè)計(jì)的驗(yàn)證。
【圖文】：

太大我們則通常采用bit一hahsnig驗(yàn)證模式進(jìn)行屬性驗(yàn)證。然后對(duì)驗(yàn)證結(jié)果進(jìn)行分析，找出模型中的錯(cuò)誤，進(jìn)行修改后重新驗(yàn)證，，直到P中的每個(gè)屬性進(jìn)行一一驗(yàn)證后，系統(tǒng)的驗(yàn)證才結(jié)束。如圖2一9表示SPNI的驗(yàn)證過(guò)程圖示。圖2一9:SPNI的驗(yàn)證過(guò)程
【學(xué)位授予單位】：蘭州大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2006
【分類(lèi)號(hào)】：TP368.1

【相似文獻(xiàn)】

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

1 劉曉芹;黃考利;連光耀;呂曉明;;基于Rebeca模型的硬件設(shè)計(jì)形式化驗(yàn)證[J];計(jì)算機(jī)測(cè)量與控制;2009年05期

2 楊紅麗,王曙燕,韓俊剛;基于形式化的面向?qū)ο箝_(kāi)發(fā)方法(FMOO)[J];計(jì)算機(jī)應(yīng)用;2000年05期

3 周宏斌,黃連生,桑田;基于串空間的安全協(xié)議形式化驗(yàn)證模型及算法[J];計(jì)算機(jī)研究與發(fā)展;2003年02期

4 陳江;陳建國(guó);陸慧娟;王康健;;UML時(shí)間順序圖的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證[J];中國(guó)計(jì)量學(xué)院學(xué)報(bào);2010年01期

5 侯峻峰,張磊,黃連生;一種新的安全協(xié)議形式化驗(yàn)證方法[J];計(jì)算機(jī)研究與發(fā)展;2004年08期

6 郭建;時(shí)序電路的形式化證明[J];現(xiàn)代電子技術(shù);2005年20期

7 王金雙;楊華兵;張興元;王元元;張毓森;;電梯控制系統(tǒng)在Isabelle/HOL中的活動(dòng)性證明[J];計(jì)算機(jī)工程與應(yīng)用;2008年27期

8 潘國(guó)華;王惠芳;;密碼API安全性分析[J];計(jì)算機(jī)安全;2009年06期

9 郭建,韓俊剛;SOC的形式化驗(yàn)證方法[J];西安郵電學(xué)院學(xué)報(bào);2005年03期

10 張海賓;段振華;;混合投影時(shí)序邏輯與混合系統(tǒng)的形式化驗(yàn)證[J];計(jì)算機(jī)科學(xué);2007年11期

相關(guān)會(huì)議論文 前10條

1 苗潔君;王克;;密碼模塊的形式化設(shè)計(jì)和驗(yàn)證研究[A];第二十一次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2006年

2 吳鈴鈴;周干民;何偉;高明倫;;IP軟核的形式化驗(yàn)證[A];全國(guó)第十五屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用學(xué)術(shù)會(huì)議論文集[C];2003年

3 劉力軻;游定山;楊佳;元國(guó)軍;沈華;;集合通信芯片物理設(shè)計(jì)階段的驗(yàn)證方法[A];第十五屆計(jì)算機(jī)工程與工藝年會(huì)暨第一屆微處理器技術(shù)論壇論文集（A輯）[C];2011年

4 郭建;韓俊剛;;基于PSL的FIFO的驗(yàn)證[A];第五屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2008年

5 余興超;馬爭(zhēng)先;王玉斌;董榮勝;;基于UPPAAL的簡(jiǎn)單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計(jì)算機(jī)學(xué)會(huì)2010年學(xué)術(shù)年會(huì)論文集[C];2010年

6 李彩虹;章超;李廉;孫守卿;;分布式同步仲裁器電路的SPIN建模和驗(yàn)證[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

7 何青;駱翔宇;蘇開(kāi)樂(lè);;對(duì)弈必勝策略的符號(hào)化模型檢測(cè)[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

8 薛慧琦;吳恒;;由程序規(guī)約推導(dǎo)程序[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

9 郭華;莊雷;;電子商務(wù)協(xié)議的形式化驗(yàn)證方法及FR驗(yàn)證實(shí)例[A];2005年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2005年

10 陳博文;郭琦;沈海華;;浮點(diǎn)乘加部件的自動(dòng)化形式驗(yàn)證[A];第六屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2010年

相關(guān)博士學(xué)位論文 前10條

1 張海賓;混合系統(tǒng)的形式化驗(yàn)證[D];西安電子科技大學(xué);2007年

2 許可;網(wǎng)格服務(wù)流的狀態(tài)π演算形式化驗(yàn)證技術(shù)研究與應(yīng)用[D];清華大學(xué);2007年

3 沈勝宇;模型檢驗(yàn)的反例解釋[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

4 張鵬飛;Agent通信的全信息形式語(yǔ)用方法[D];北京郵電大學(xué);2007年

5 李夢(mèng)君;安全協(xié)議形式化驗(yàn)證技術(shù)的研究與實(shí)現(xiàn)[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

6 范年柏;程序正確性驗(yàn)證的幾個(gè)問(wèn)題[D];湖南大學(xué);2005年

7 張秀國(guó);基于過(guò)程網(wǎng)絡(luò)的服務(wù)協(xié)同計(jì)算模型研究[D];大連海事大學(xué);2006年

8 岳華偉;對(duì)一種SOC總線系統(tǒng)的驗(yàn)證[D];中國(guó)科學(xué)技術(shù)大學(xué);2007年

9 程亮;基于模型檢測(cè)的安全操作系統(tǒng)驗(yàn)證方法研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2009年

10 王小兵;面向?qū)ο驧SVL語(yǔ)言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D];西安電子科技大學(xué);2009年

相關(guān)碩士學(xué)位論文 前10條

1 李彩虹;硬件系統(tǒng)SystemC～（FL）設(shè)計(jì)模型的SPIN驗(yàn)證[D];蘭州大學(xué);2006年

2 吳孝軍;基于SPIN的ATM交換機(jī)行為的驗(yàn)證[D];蘭州大學(xué);2006年

3 林立;基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗(yàn)證[D];西安電子科技大學(xué);2005年

4 閆碩;基于多項(xiàng)式符號(hào)代數(shù)的電路形式驗(yàn)證[D];北京交通大學(xué);2011年

5 王莉;供熱混合系統(tǒng)的抽象及其形式化驗(yàn)證[D];華中科技大學(xué);2004年

6 馬小龍;形式化驗(yàn)證在Office安全中的應(yīng)用研究[D];中國(guó)人民解放軍信息工程大學(xué);2005年

7 楊漢明;基于CPS的實(shí)時(shí)系統(tǒng)的面向方面的形式化驗(yàn)證方法[D];廣東工業(yè)大學(xué);2011年

8 鄭強(qiáng);基于SPIN的802.1X協(xié)議形式化驗(yàn)證和改進(jìn)[D];華東理工大學(xué);2012年

9 廖軍和;深亞微米EoPDH專(zhuān)用集成電路的設(shè)計(jì)與實(shí)現(xiàn)[D];合肥工業(yè)大學(xué);2009年

10 姜玉蓉;LINUX內(nèi)核進(jìn)程間通信的模型檢測(cè)研究[D];湖南大學(xué);2009年

本文編號(hào)：2708462