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

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

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