模型檢查是一種非常重要的形式化驗(yàn)證技術(shù),它利用狀態(tài)空間搜索來探索所有可能的系統(tǒng)狀態(tài)。以這種方式,可以檢查給定的系統(tǒng)是否滿足某些屬性。近年來,模型檢查得到了快速的發(fā)展,已經(jīng)在很多高安全性領(lǐng)域中得到了廣泛應(yīng)用,如航空航天、軌道交通、汽車電子、工業(yè)控制等領(lǐng)域。下推系統(tǒng)因其特殊的結(jié)構(gòu),是模型檢查中一種常用的理論模型。下推系統(tǒng)的模型檢查已廣泛應(yīng)用于程序分析、惡意軟件檢測等實(shí)際問題。可是,在現(xiàn)實(shí)問題中,仍然有一些問題限制著模型檢查技術(shù)的發(fā)展。首先,隨著程序的復(fù)雜化,模型檢查遇到的一個(gè)真正的挑戰(zhàn),就是眾所周知的狀態(tài)爆炸問題。其次,現(xiàn)有模型檢查算法的效率往往取決于狀態(tài)空間的大小,在有限的處理器和內(nèi)存條件下,更加有效地進(jìn)行模型檢查也變得困難重重。到目前為止,已經(jīng)出現(xiàn)了一些技術(shù)來解決以上的問題,如:符號模型檢查、偏序規(guī)約、對稱規(guī)約等技術(shù)。除了這些傳統(tǒng)的技術(shù)外,并行計(jì)算,尤其是,在大規(guī)模計(jì)算任務(wù)方面表現(xiàn)出了獨(dú)特的優(yōu)勢,這引起了模型檢查研究者的廣泛關(guān)注。一些工作已經(jīng)使用對模型檢查進(jìn)行加速,并且取得了不錯的效果。本文基于自動機(jī)理論,為下推系統(tǒng)的模型檢查提出了通用并行解決方案,并基于實(shí)現(xiàn)了下推系統(tǒng)可達(dá)性分析和模型... 

【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：95 頁

【學(xué)位級別】：碩士

【部分圖文】：

圖一個(gè)示例程序

【參考文獻(xiàn)】：
期刊論文
[1]工業(yè)4.0和智能制造[J]. 張曙.  機(jī)械設(shè)計(jì)與制造工程. 2014(08)
[2]利用GPU進(jìn)行通用數(shù)值計(jì)算的研究[J]. 徐品,藍(lán)善禎,劉蘭蘭.  中國傳媒大學(xué)學(xué)報(bào)(自然科學(xué)版). 2009(02)
[3]基于圖形處理器（GPU）的通用計(jì)算[J]. 吳恩華,柳有權(quán).  計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào). 2004(05)
[4]基于形式化方法的需求分析[J]. 塔維娜,何積豐.  計(jì)算機(jī)工程. 2003(18)
[5]軟件可靠性研究與進(jìn)展[J]. 劉云,趙瑋.  微機(jī)發(fā)展. 2003(02)



本文編號：3319892