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

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

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