【摘要】： 計算機(jī)軟硬件系統(tǒng)日益復(fù)雜,在很多系統(tǒng)中,測試、模擬等傳統(tǒng)的驗證方法已不能保證其正確性和可靠性。模型檢測技術(shù)產(chǎn)生于上世紀(jì)80年代,由美國的Clarke和Emerson,法國的Quielle和Sifakis分別獨(dú)立提出。在該形式化驗證方法中,系統(tǒng)性質(zhì)用命題時態(tài)邏輯公式表示,有限狀態(tài)反應(yīng)系統(tǒng)(硬件電路、通訊協(xié)議)用狀態(tài)轉(zhuǎn)換系統(tǒng)描述,有效的查詢過程檢測模型,判斷模型是否滿足系統(tǒng)性質(zhì)。然而,隨著系統(tǒng)規(guī)模的增大,狀態(tài)數(shù)呈指數(shù)上升的狀況和顯式模型檢測有限的處理能力之間存在難以克服的矛盾,即狀態(tài)爆炸。1986年,Bryant將傳統(tǒng)的二值判定圖BDD技術(shù)加以改進(jìn),使之成為布爾函數(shù)的規(guī)范表示方法。之后McMillan將這種技術(shù)應(yīng)用于模型檢測中,基于BDD的模型檢測稱為符號模型檢測。符號模型檢測的主要特點(diǎn)是用BDD隱式地表示有限狀態(tài)反應(yīng)系統(tǒng)的狀態(tài)集合和狀態(tài)轉(zhuǎn)換集合,空間爆炸問題被有效緩解。 本研究實現(xiàn)了一個基本的符號模型檢測器CTLMC。該模型檢測器直接采用布爾函數(shù)作為系統(tǒng)模型的描述語言,用來描述模型的初始狀態(tài)集合和系統(tǒng)狀態(tài)轉(zhuǎn)換關(guān)系;采用CTL時態(tài)邏輯作為系統(tǒng)性質(zhì)的描述語言,用來描述系統(tǒng)應(yīng)該滿足的需求(性質(zhì));采用CTL符號模型檢測算法計算模型是否滿足性質(zhì)。 此外,在實現(xiàn)CTLMC過程中發(fā)現(xiàn)一種基于BDD的SMC中PRE(?)操作的改進(jìn)算法,該算法處理PRE(?)步驟3(嵌套布爾存在量化)的方法是,一次遍歷“刪除”所有被量化變量的節(jié)點(diǎn),產(chǎn)生表示布爾函數(shù)與嵌套存在量化結(jié)果等價的不確定排序二值判定圖,然后把不確定排序二值判定圖轉(zhuǎn)換成OBDD。實驗表明該算法能有效縮短計算時間,減少中間節(jié)點(diǎn)所需空間。
【學(xué)位授予單位】：西安理工大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2008
【分類號】：TP306
【圖文】：

黝黝黝翼翼瀕瀕 MMM滿足 sssssM不滿足 sss圖1一 2CTLMC結(jié)構(gòu)概圖Fig.l一 2CTLMCframework.6論文的組織結(jié)構(gòu)論文的后續(xù)章節(jié)分別為:第二章系統(tǒng)模型，主要介紹系統(tǒng)模型的表示，如何用臉ipke狀態(tài)轉(zhuǎn)換圖和布爾函數(shù)表示，以及布爾函數(shù)詞法語法解析器的實現(xiàn)，最后介紹二值判定圖和布爾函數(shù)對應(yīng)的二值判定圖的生成算法。第三章系統(tǒng)性質(zhì)，主要介紹計算樹時態(tài)邏輯CTL和CTL詞法語法解析器的實現(xiàn)。第四章模型檢測，主要介紹Labeling檢測算法和cTLMc所采用的符號模型檢測算法。

芍芍勺勺【【)已 已已}積 積 芍芍口口 lll刁，，，，，， 芍芍口口【【〕日日 圖1一 3CTLMC界面Fig.1一 3CnJMCuserinterface

【引證文獻(xiàn)】

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

1 韓樹森;戴航;;模型檢驗下蠕蟲病毒檢測器的設(shè)計與實現(xiàn)[J];現(xiàn)代電子技術(shù);2012年03期

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

1 于帥帥;基于RPR的核電數(shù)字化保護(hù)系統(tǒng)安全通信網(wǎng)絡(luò)的研究[D];上海交通大學(xué);2011年

2 聞曉;一種基于Mealy機(jī)的BPEL程序驗證模型研究[D];西南大學(xué);2009年

3 高超;安全級軟件驗證與確認(rèn)中測試技術(shù)研究[D];上海交通大學(xué);2010年

4 張澤恩;基于GSTE中的符號仿真設(shè)計與實現(xiàn)[D];電子科技大學(xué);2012年

本文編號：2715956