基于形式化規(guī)格說明的程序測試方法和工具的研究.pdf

1、軟件測試和形式化方法是保證軟件系統(tǒng)可靠性的兩種方法。由于形式化方法研究在工程應用領域并沒有取得突破性的研究成果，完全使用形式化方法不能解決現(xiàn)有的軟件問題。而軟件測試的方法和過程不是完全形式化的，必然包含一些規(guī)則、經(jīng)驗等非形式化的內(nèi)容。因此，將形式化方法引入軟件測試中，一方面實現(xiàn)了形式化方法在工程中的應用，另一個方面可以改善現(xiàn)有的測試方法，實現(xiàn)軟件測試的自動化。 本文在形式化方法SOFL的基礎上，提出了一個基于SOFL形式化規(guī)格說

2、明的測試模型，重點研究測試用例的生成，邏輯覆蓋準則和評估。這個模型描述為：首先確定程序中被測類與形式化規(guī)格說明的對應關系，從類的形式化規(guī)格說明導出類的狀態(tài)轉(zhuǎn)換圖。然后把狀態(tài)轉(zhuǎn)換圖看作有限自動機，就可以得到生成測試數(shù)據(jù)的方法，根據(jù)方法調(diào)用序列覆蓋標準，就可以驗證測試的完整性和一致性。最后根據(jù)邏輯覆蓋的評估準則，分析測試的效果。 在這個測試模型基礎上，實現(xiàn)了一個基于SOFL形式化規(guī)格說明的Java程序測試工具。這個工具首先確定SOF