基于形式規(guī)格說明的協(xié)議測試研究.pdf

1、計算機通信協(xié)議的開發(fā)難度隨著復(fù)雜程度的增加而日益增大,潛在錯誤也越來越多,其中對協(xié)議規(guī)格說明理解的偏差是重要原因之一.因此需要對協(xié)議進行一致性測試,協(xié)議的一致性測試就是測試協(xié)議的實現(xiàn)是否與相關(guān)國際標(biāo)準(zhǔn)中的規(guī)格說明相一致.協(xié)議的規(guī)格說明主要是以自然語言描述的,對其進行形式化是為了精確描述協(xié)議,因而可有效的減少這類錯誤的出現(xiàn).在軟件測試過程中,測試用例的生成是軟件測試的關(guān)鍵和難點.目前,測試用例的生成主要靠手工完成,而且要求軟件測試人員具有

2、一定的經(jīng)驗和較高的專業(yè)水平,因而,測試過程往往帶有很大盲目性,致使測試效率低下,軟件成本居高不下,軟件質(zhì)量也很難保證.為此,迫切需要改進軟件測試的方法,開發(fā)一些測試用例的自動生成工具,提高軟件測試效率,降低軟件成本,保證軟件質(zhì)量,提高軟件測試的自動化程度.形式方法是基于數(shù)學(xué)方法來描述目標(biāo)軟件系統(tǒng)性質(zhì)的軟件開發(fā)方法,它為系統(tǒng)的說明、開發(fā)和驗證提供了一個框架.軟件規(guī)格說明是用形式規(guī)格說明語言精確描述軟件需求的文檔.Z語言是目前比較流行、使用

3、較為成功而有效的語言,它是基于模型的形式化規(guī)格語言,它以一階謂詞邏輯和集合論作為形式語言基礎(chǔ),將函數(shù)、映射、關(guān)系等數(shù)學(xué)方法用于規(guī)格說明之中,具有精確、簡潔、無二義性的特點,有利于保證程序的正確性,尤其適合于無法進行現(xiàn)場調(diào)試的高安全性系統(tǒng)的開發(fā).本文中我們使用Z對TCP協(xié)議進行形式化,為協(xié)議一致性測試打下基礎(chǔ).得到TCP協(xié)議的形式化描述后,可以將其轉(zhuǎn)換為xml格式的文件,構(gòu)造一個自動產(chǎn)生測試用例的工具,該工具導(dǎo)入存儲了TCP協(xié)議狀態(tài)轉(zhuǎn)換信