軟件已經(jīng)成為當(dāng)今社會(huì)發(fā)展中不可或缺的元素,在航空航天、醫(yī)療、交通等關(guān)鍵領(lǐng)域已經(jīng)得到成功的運(yùn)用。隨著軟件的重要性日益凸顯,軟件的可靠性和安全性自然而然地受到重視。長(zhǎng)期以來(lái),研究人員一直著眼于如何發(fā)現(xiàn)軟件中隱藏的錯(cuò)誤,保障軟件的可靠性和安全性。模型檢測(cè)是應(yīng)用廣泛且十分有效的方法之一。它通過(guò)對(duì)程序建模,形式化地描述性質(zhì),然后自動(dòng)化地驗(yàn)證程序是否滿足期望的性質(zhì)。但是,狀態(tài)空間爆炸問(wèn)題是模型檢測(cè)面臨的一個(gè)關(guān)鍵問(wèn)題,嚴(yán)重影響了模型檢測(cè)方法的驗(yàn)證能力,降低了其對(duì)大規(guī)模程序的驗(yàn)證效果。因此,如何提高模型檢測(cè)方法的驗(yàn)證效率和驗(yàn)證規(guī)模,使得其能更好地應(yīng)用于大規(guī)模的程序驗(yàn)證,已經(jīng)成為程序驗(yàn)證領(lǐng)域的研究熱點(diǎn)。反例制導(dǎo)的抽象細(xì)化（Counterexample-guided Abstraction Refinement,CEGAR）技術(shù)能有效地縮減模型檢測(cè)的狀態(tài)空間,提高模型檢測(cè)的效率,對(duì)大規(guī)模程序也有很好的應(yīng)用性。本文重點(diǎn)圍繞基于CEGAR的抽象模型檢測(cè)方法,研究和討論如何緩解狀態(tài)空間爆炸問(wèn)題,以及如何自動(dòng)化地對(duì)程序的性質(zhì)進(jìn)行驗(yàn)證。本文的主要貢獻(xiàn)和研究?jī)?nèi)容如下:第一,基于CEGAR的模型檢測(cè)方法已經(jīng)成功地應(yīng)用于... 

【文章來(lái)源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁(yè)數(shù)】：145 頁(yè)

【學(xué)位級(jí)別】：博士

【部分圖文】：

示例程序simple.c和對(duì)應(yīng)的CFG

西安電子科技大學(xué)博士學(xué)位論文同時(shí)，由于 ( 0, ..., ) → ( [0])，因此，可以得到{ ( 0, · · · , )} ; · · · ; 1{ }即 ( 0, 0, ..., , , ..., )是可滿足的，得證。同樣，為了更清楚地理解E-interp插值的作用，下面介紹一下對(duì)圖2.1中的 . 程序，使用E-interp插值進(jìn)行驗(yàn)證的過(guò)程。完整的抽象可達(dá)樹(shù)如圖3.5所示，為了方便，在圖中用 表示錯(cuò)誤插值。首先介紹使用Craig插值計(jì)算E-interp插值的過(guò)程。 第

展開(kāi)控制流圖 ，探索是否存在一條真反例路徑，從而生成抽象可達(dá)樹(shù) 。圖3.6展示了驗(yàn)證程序安全性質(zhì)的框架流圖。對(duì)于一個(gè)抽象狀態(tài) : ( , , )，且 不是ERROR位置，則1.如果滿足下面三個(gè)條件之一，則遍歷其他路徑分支: = ； = ，且 ( 0, ..., ) → ( )； = ， 被抽象狀態(tài) ′覆蓋。這里， ′是已經(jīng)遍歷過(guò)狀態(tài)。2.如果 = ，且 ( 0, ..., ) → ( )

【參考文獻(xiàn)】：
期刊論文
[1]符號(hào)化模型檢測(cè)CTL[J]. 蘇開(kāi)樂(lè),駱翔宇,呂關(guān)鋒.  計(jì)算機(jī)學(xué)報(bào). 2005(11)



本文編號(hào)：2958799