基于形式化描述的協(xié)議一致性測試方法的研究.pdf

1、該文針對協(xié)議數(shù)據(jù)流的測試進行了研究,選擇了構(gòu)造類別代數(shù)來對協(xié)議的數(shù)據(jù)流部分進行形式化描述,提出了相應(yīng)的測試方法.在此基礎(chǔ)上,將其與有限狀態(tài)機模型結(jié)合起來,對協(xié)議的控制流和數(shù)據(jù)流進行完整的測試.該文的主要內(nèi)容包含以下幾個部分:1.提出了基于構(gòu)造類別代數(shù)的變異分析方法構(gòu)造類別代數(shù)是一種特別適合于描述協(xié)議數(shù)據(jù)流的形式化方法.該文對構(gòu)造類別代數(shù)的基本定義進行了擴展:使用前/后條件來定義公理,以擴充構(gòu)造類別代數(shù)的描述能力;使用公理選擇優(yōu)先級來簡化

2、公理前條件的定義.在協(xié)議一致性測試中,有兩種基本的測試策略:一是定義錯誤模型,然后根據(jù)該錯誤模型設(shè)計測試用例,以檢測出所有可能出現(xiàn)的錯誤;二是根據(jù)協(xié)議行為的描述,針對所有可能出現(xiàn)的行為情況進行檢查,以確定協(xié)議實體的行為是否正確.2.提出了基于構(gòu)造類別代數(shù)的滿足分支覆蓋標準的測試方法采用上述第二種策略,并考慮到公理是使用前/后條件來定義的這一特點,該文提出了滿足分支覆蓋標準的測試用例集合生成方法.首先,介紹了判定覆蓋、條件覆蓋、條件/判定

3、覆蓋、多重條件覆蓋和改進的條件/判定覆蓋五種標準的定義;然后,選擇改進的條件/判定覆蓋標準為例,給出了針對單條公理的滿足該覆蓋標準的測試集合;最后,提出了將單條公理的測試集合結(jié)合得到完整測試集合的算法.3.提出了結(jié)合構(gòu)造類別代數(shù)與有限狀態(tài)機的描述和測試方法在協(xié)議一致性測試中,有限狀態(tài)機是描述協(xié)議控制流的最常用的形式化模型.該文提出使用狀態(tài)-公理關(guān)聯(lián)函數(shù)來將構(gòu)造類別代數(shù)與有限狀態(tài)機模型結(jié)合起來,使得協(xié)議控制流和數(shù)據(jù)流部分的描述相對獨立,便