基于圖論的形式化驗(yàn)證方法的研究與實(shí)現(xiàn)

《基于圖論的形式化驗(yàn)證方法的研究與實(shí)現(xiàn)》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。

1、朵各糾成＊穿ＵＮＩＴＹＦＥＬＥＣＴＲＩＥＮＣＥＡＮＤＴＥ已ＨＮＯＬＯＧＹＯＦＣＨＩＮＡＩＶＥＲＳＯＯＮＩＣＳＣ專業(yè)學(xué)位碩±學(xué)位論文ＭＡＳＴＥＲＴＨＥＳＩＳＦＯＲＰＲＯＦＥＳＳＩＯＮＡＬＤＥＧＲＥＥｒ畫ｉ論支題目基于圖論的形式化驗(yàn)證方法的妍究與實(shí)現(xiàn)專業(yè)學(xué)位類別工程碩±學(xué)號２０１３２２２２０２２８作者娃名陳凌字指導(dǎo)教師詹謹(jǐn)瑜副繼■定獨(dú)創(chuàng)性聲明本人聲明所呈交的學(xué)位論文是本人在導(dǎo)師指導(dǎo)下進(jìn)行的研究工作及取得的研究成果。據(jù)我所知，除了文中特別加標(biāo)注和致謝的地

2、方外，論文中不包含其他人己經(jīng)發(fā)表或撰寫過的研究成果，也不包含為獲得電子科技大學(xué)或其它教育機(jī)構(gòu)的學(xué)位或證書而使用過的材料。與我一同工作的同志對本研究所做的任何貢獻(xiàn)均已在論文中作了明確的說明并表示謝意。作者簽名：常足寺曰期；巧／＾年＾月／２曰論文使用授權(quán)本學(xué)位論文作者完全了解電子科技大學(xué)有關(guān)保留、使用學(xué)位論文的規(guī)定，有權(quán)保留并向國家有關(guān)部口或機(jī)構(gòu)送交論文的復(fù)印件和磁盤，化許論文被查閱和借瞬。本人授權(quán)電子科技大學(xué)可臥將學(xué)位論文、的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索，可Ｗ采用影印縮印或掃描等復(fù)制手段保存、匯

3、編學(xué)位論文。）（保密的學(xué)位論文在解密后應(yīng)遵守此規(guī)定作者簽名：帶導(dǎo)師簽名：誨＞＾＾＾日期：年（月攻日，分類號密級注1UDC學(xué)位論文基于圖論的形式化驗(yàn)證方法的研究與實(shí)現(xiàn)陳凌宇指導(dǎo)教師詹瑾瑜副教授電子科技大學(xué)成都申請學(xué)位級別碩士專業(yè)學(xué)位類別工程碩士工程領(lǐng)域名稱軟件工程提交論文日期2016.03.18論文答辯日期2016.04.27學(xué)位授予單位和日期電子科技大學(xué)2016年6月答辯委員會(huì)主席評閱人RESEARCHANDIMPLEMENTATIONOFMODELCHECKINGALGORITHMBASEDONGRAHPTHEORYAM

4、asterThesisSubmittedtoUniversityofElectronicScienceandTechnologyofChinaMajor:MasterofEngineeringAuthor:ChenLingyuSupervisor:ZhanJinyuSchoolofInformationandSoftwareSchool:Engineering摘要摘要隨著硬件制作的工藝發(fā)展和軟件開發(fā)技術(shù)的日益成熟，軟硬件的制作產(chǎn)能越來越強(qiáng)，這也對軟硬件質(zhì)量的可靠性和效率性能有了越來越高的要求。為此在可靠性和性能的保證上的資源投入也越來越大。傳

5、統(tǒng)驗(yàn)證方法會(huì)耗費(fèi)太多的人力物力。為了降低制作和開發(fā)的成本，同時(shí)保證其產(chǎn)品的可靠性，基于嚴(yán)格的數(shù)據(jù)證明的驗(yàn)證方法形式化驗(yàn)證，也越來越受到人們的重視，在工業(yè)界有了廣泛的使用。在科學(xué)界，形式化驗(yàn)證的方法也有了很多分支和廣泛了研究。本文深入研究了現(xiàn)有的形式化驗(yàn)證方法，提出了一種新的形式化驗(yàn)證方法。該方法采用圖的鄰接矩陣建立待驗(yàn)證系統(tǒng)的數(shù)學(xué)模型，采用CTL表示式來描述待驗(yàn)證系統(tǒng)需要滿足的屬性，將待驗(yàn)證系統(tǒng)的屬性驗(yàn)證過程轉(zhuǎn)化成了對應(yīng)矩陣模型的計(jì)算。本文首先給出了一種基于鄰接矩陣的系統(tǒng)建模方法，根據(jù)待驗(yàn)證系統(tǒng)狀態(tài)圖中的各狀態(tài)編碼和狀態(tài)轉(zhuǎn)移關(guān)系，給出待驗(yàn)證系

6、統(tǒng)狀態(tài)圖的鄰接矩陣，由于該矩陣與待驗(yàn)證系統(tǒng)同構(gòu)，因此可以通過鄰接矩陣的相關(guān)運(yùn)算來反映待驗(yàn)證系統(tǒng)的各個(gè)屬性。本驗(yàn)證方法改進(jìn)了模型檢測算法中復(fù)雜的狀態(tài)標(biāo)記過程，為不同時(shí)態(tài)邏輯CTL運(yùn)算符分別給出了對應(yīng)的矩陣運(yùn)算表示，使得待驗(yàn)證系統(tǒng)的形式化驗(yàn)證過程變成了矩陣的公式計(jì)算，根據(jù)需驗(yàn)證的CTL屬性描述帶入相應(yīng)的矩陣計(jì)算公式即可方便地計(jì)算出其可滿足性。本文最后采用所提出的基于圖鄰接矩陣的形式化驗(yàn)證方法，設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)形式化驗(yàn)證工具，并通過對兩個(gè)實(shí)例（FIFO隊(duì)列和PCI總線仲裁器）的驗(yàn)證以及與NuSMV工具的驗(yàn)證結(jié)果對比，說明了本文方法及其工具的可用性和

7、有效性。關(guān)鍵詞：形式化驗(yàn)證，模型檢測，Kripke結(jié)構(gòu)，CTL表達(dá)式，鄰接矩陣IABSTRACTABSTRACTWiththedevelopmentofhardwareproductivityandsoftwaretechnology,thereliabilityandefficiencyofhardwareandsoftwarebecomemoreandmoreimportant.Thehigherrequirementcausemorecost.Thetraditionalverificationmethodsneedtoomuchman

8、powerandmaterialresources.Inordertoreducethecostofproductionanddevelopmentandensur