[發明專利]一種協議一致性測試中的狀態驗證方法

有效

• 申請號: 201010167584.3
• 申請日: 2010-05-10
• 公開（公告）號: CN102244590A
• 公開（公告）日: 2011-11-16
• 發明（設計）人: 楊美紅;張新常
• 申請（專利權）人: 山東省計算中心
• 主分類號: H04L12/26
• 分類號: H04L12/26;H04L29/06
• 代理公司: 濟南泉城專利商標事務所 37218
• 代理人: 李桂存

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

1)驗證準備：給定一個被測實現、該被測實現對應的規范FSM/EFSM模型、該被測實現中的一個被測狀態u及擬驗證的狀態s；

2)若所述被測實現符合輸入正確條件或為提供診斷信息而假定輸入正確條件成立，則將規范FSM/EFSM模型以預定的數據結構加以存儲；否則，結束本方法；

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

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

5)根據步驟3)中找到的擬驗證的狀態s所對應的診斷輸入序列對被測狀態u進行測試，觀察對應的測試結果，得到狀態驗證結論，即：被測實現中被測狀態u是否為擬驗證的狀態s，或該被測狀態是否為擬驗證的狀態s所對應的候選狀態集合中的一個狀態。

2.根據權利要求1所述的方法，其特征在于：所述輸入正確條件優選在相關聯的單元測試中通過對被測實現的狀態進行輸入符號測試得以滿足。

3.根據權利要求1所述的方法，其特征在于：規范FSM/EFSM模型以矩陣結構或者鏈接表結構存儲，且若采用矩陣結構存儲，須區分各狀態遷移標簽元素；若采用鄰接表結構存儲，則節點元素與狀態遷移標簽的元素相對應。

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

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

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

7.根據權利要求1所述的方法，其特征在于：所述候選閾值設為2或3。

8.根據權利要求1所述的方法，其特征在于：當擬驗證的狀態s所對應的候選狀態集合的大小為1時，若擬驗證的狀態s所對應的診斷輸入序列施加在被測狀態u上能夠無中斷地執行，則被測狀態u為擬驗證的狀態s，否則被測狀態u不是擬驗證的狀態s；當狀態s的候選狀態集合的大小大于1時，若擬驗證的狀態s所對應的診斷輸入序列施加在被測狀態u上能夠無中斷地執行，則被測狀態u是擬驗證的狀態s所對應的候選狀態集合中的一個狀態，否則，被測狀態u不在擬驗證的狀態s所對應的候選狀態集合中。