[發(fā)明專利]一種協(xié)議一致性測試中的狀態(tài)驗證方法

有效

• 申請?zhí)枺?/td>: 201010167584.3
• 申請日: 2010-05-10
• 公開（公告）號: CN102244590A
• 公開（公告）日: 2011-11-16
• 發(fā)明（設(shè)計）人: 楊美紅;張新常
• 申請（專利權(quán)）人: 山東省計算中心
• 主分類號: H04L12/26
• 分類號: H04L12/26;H04L29/06
• 代理公司: 濟(jì)南泉城專利商標(biāo)事務(wù)所 37218
• 代理人: 李桂存

1.一種協(xié)議一致性測試中的狀態(tài)驗證方法，該方法基于FSM/EFSM模型并且采用以下步驟：

1)驗證準(zhǔn)備：給定一個被測實現(xiàn)、該被測實現(xiàn)對應(yīng)的規(guī)范FSM/EFSM模型、該被測實現(xiàn)中的一個被測狀態(tài)u及擬驗證的狀態(tài)s；

2)若所述被測實現(xiàn)符合輸入正確條件或為提供診斷信息而假定輸入正確條件成立，則將規(guī)范FSM/EFSM模型以預(yù)定的數(shù)據(jù)結(jié)構(gòu)加以存儲；否則，結(jié)束本方法；

3)基于規(guī)范FSM/EFSM模型獲取擬驗證狀態(tài)s所對應(yīng)的診斷輸入序列及候選狀態(tài)集合，并將獲得的診斷輸入序列及候選狀態(tài)集合加以存儲以備驗證所述被測實現(xiàn)中的其它被測狀態(tài)；

4)若步驟3)中所述候選狀態(tài)集合中的元素數(shù)量超過候選閾值，則放棄繼續(xù)進(jìn)行本方法；否則，進(jìn)入下一步；

5)根據(jù)步驟3)中找到的擬驗證的狀態(tài)s所對應(yīng)的診斷輸入序列對被測狀態(tài)u進(jìn)行測試，觀察對應(yīng)的測試結(jié)果，得到狀態(tài)驗證結(jié)論，即：被測實現(xiàn)中被測狀態(tài)u是否為擬驗證的狀態(tài)s，或該被測狀態(tài)是否為擬驗證的狀態(tài)s所對應(yīng)的候選狀態(tài)集合中的一個狀態(tài)。

2.根據(jù)權(quán)利要求1所述的方法，其特征在于：所述輸入正確條件優(yōu)選在相關(guān)聯(lián)的單元測試中通過對被測實現(xiàn)的狀態(tài)進(jìn)行輸入符號測試得以滿足。

3.根據(jù)權(quán)利要求1所述的方法，其特征在于：規(guī)范FSM/EFSM模型以矩陣結(jié)構(gòu)或者鏈接表結(jié)構(gòu)存儲，且若采用矩陣結(jié)構(gòu)存儲，須區(qū)分各狀態(tài)遷移標(biāo)簽元素；若采用鄰接表結(jié)構(gòu)存儲，則節(jié)點元素與狀態(tài)遷移標(biāo)簽的元素相對應(yīng)。

4.根據(jù)權(quán)利要求3所述的方法，其特征在于：矩陣結(jié)構(gòu)的存儲元素類型為字符串形式，加以區(qū)分的狀態(tài)遷移標(biāo)簽元素包括輸入符號、輸出符合和變量賦值操作，并采用轉(zhuǎn)義符號表示法對狀態(tài)遷移標(biāo)簽元素加以區(qū)分；該轉(zhuǎn)義符號表示法采用“/”表示分隔符號，若標(biāo)簽元素包含“/”符號，則用“//”符號替換；在對上述表示方法進(jìn)行語義解釋時，單個出現(xiàn)的“/”符號為分隔符，順序出現(xiàn)的連續(xù)兩個“/”符號用一個“/”符號替換回來。

5.根據(jù)權(quán)利要求1所述的方法，其特征在于：所述步驟3)中首先獲取起始于對應(yīng)擬驗證的狀態(tài)s所對應(yīng)的基于規(guī)范FSM/EFSM模型的可執(zhí)行輸入序列，進(jìn)而選取能夠把相應(yīng)狀態(tài)與模型中的其它狀態(tài)最大可能區(qū)分開來的可執(zhí)行輸入序列作為診斷輸入序列；并取診斷輸入序列不能區(qū)分的狀態(tài)組成的集合作為擬驗證的狀態(tài)s所對應(yīng)的候選狀態(tài)集合。

6.根據(jù)權(quán)利要求1或5所述的方法，其特征在于：診斷輸入序列通過對錯誤轉(zhuǎn)換空間的遍歷獲得。

7.根據(jù)權(quán)利要求1所述的方法，其特征在于：所述候選閾值設(shè)為2或3。

8.根據(jù)權(quán)利要求1所述的方法，其特征在于：當(dāng)擬驗證的狀態(tài)s所對應(yīng)的候選狀態(tài)集合的大小為1時，若擬驗證的狀態(tài)s所對應(yīng)的診斷輸入序列施加在被測狀態(tài)u上能夠無中斷地執(zhí)行，則被測狀態(tài)u為擬驗證的狀態(tài)s，否則被測狀態(tài)u不是擬驗證的狀態(tài)s；當(dāng)狀態(tài)s的候選狀態(tài)集合的大小大于1時，若擬驗證的狀態(tài)s所對應(yīng)的診斷輸入序列施加在被測狀態(tài)u上能夠無中斷地執(zhí)行，則被測狀態(tài)u是擬驗證的狀態(tài)s所對應(yīng)的候選狀態(tài)集合中的一個狀態(tài)，否則，被測狀態(tài)u不在擬驗證的狀態(tài)s所對應(yīng)的候選狀態(tài)集合中。