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

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

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