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

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

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

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