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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

8 潘國華;王惠芳;;密碼API安全性分析[J];計算機安全;2009年06期

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

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

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

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

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

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

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

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

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

7 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計算機科學(xué)學(xué)術(shù)年會論文集[C];2006年

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

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

10 陳博文;郭琦;沈海華;;浮點乘加部件的自動化形式驗證[A];第六屆中國測試學(xué)術(shù)會議論文集[C];2010年

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

本文編號：2708462