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

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

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