基于模型檢查的程序驗(yàn)證和測試用例生成.pdf

1、隨著計(jì)算機(jī)軟硬件系統(tǒng)規(guī)模的日益復(fù)雜化，如何保證計(jì)算機(jī)系統(tǒng)的正確性和可靠性，逐漸成為當(dāng)前理論界和產(chǎn)業(yè)界共同關(guān)心的重要問題。而當(dāng)前限制計(jì)算機(jī)實(shí)際廣泛應(yīng)用的因素已經(jīng)不再是機(jī)器硬件“緩慢”的速度和“低下”的計(jì)算能力，而更多的是我們在設(shè)計(jì)和實(shí)現(xiàn)復(fù)雜系統(tǒng)時，設(shè)計(jì)與驗(yàn)證的能力還比較有限，無法保證所設(shè)計(jì)系統(tǒng)的正確性和可靠性。而基于狀態(tài)搜索的模型檢查技術(shù)為系統(tǒng)驗(yàn)證提供了有效的保證手段。 模型檢查是一種針對有限狀態(tài)并發(fā)系統(tǒng)的形式化驗(yàn)證技術(shù)，其基本思

2、想是構(gòu)造系統(tǒng)的有限狀態(tài)模型，在系統(tǒng)模型的狀態(tài)空間內(nèi)運(yùn)算，檢查建立的系統(tǒng)模型是否滿足期望的性質(zhì)。本文考察模型檢查技術(shù)的基本原理，研究模型檢查在軟件驗(yàn)證上的應(yīng)用，并開發(fā)實(shí)現(xiàn)了一個針對C語言編寫的程序進(jìn)行驗(yàn)證的系統(tǒng)原型。并且按照存在量詞公式的證據(jù)是全稱量詞公式的反例的特性，用模型檢查的反例生成機(jī)制對測試用例生成技術(shù)進(jìn)行研究，然后把模型檢查的算法引入到軟件測試領(lǐng)域，尋找滿足規(guī)格說明的路徑，生成測試用例，據(jù)此對系統(tǒng)進(jìn)行測試。 本文的主要工