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

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

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

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