[發明專利]基于UIO序列法驗證有限狀態機所處狀態的方法

有效

• 申請號: 201410106244.8
• 申請日: 2014-03-20
• 公開（公告）號: CN103888314B
• 公開（公告）日: 2017-06-09
• 發明（設計）人: 張冰;方爽;張奭;周元海;吳效穎;崔璨;彭露
• 申請（專利權）人: 西安電子科技大學
• 主分類號: H04L12/26
• 分類號: H04L12/26;G06F11/36
• 代理公司: 陜西電子工業專利中心61205
• 代理人: 王品華,朱紅星

1.一種基于UIO序列法驗證有限狀態機所處狀態的方法，包括如下步驟：

(1)對要進行一致性測試的通信協議的有限狀態機，合并其等價狀態，使有限狀態機最簡；

(2)求出有限狀態機內各狀態的UIO序列，找出不存在UIO序列的狀態，并構成待驗證狀態集合M；

(3)從所述待驗證狀態集合M中，任意選取一個狀態作為待驗證狀態Si；

(4)選擇待驗證狀態Si的任一輸入/輸出I/O序列，找出除待驗證狀態Si以外的含有該輸入/輸出I/O序列的所有狀態，并構成校驗狀態集合N；

(5)將被測系統所處的狀態置為待驗證狀態Si；

(6)向被測系統輸入步驟(4)中選擇的I/O序列的輸入事件序列，并檢查被測系統的輸出事件序列：

6a)如果輸出事件序列與有限狀態機規定的在待驗證狀態Si下的輸出事件序列相符，則執行步驟(7)；

6b)如果輸出事件序列與有限狀態機規定的在待驗證狀態Si下的輸出事件序列不相符，則待驗證狀態不是預期狀態，結束本次狀態驗證過程；

(7)將被測系統所處的狀態置為待驗證狀態Si；

(8)從校驗狀態集合N中任選一個狀態作為校驗狀態Sj；

(9)選擇待驗證狀態Si與狀態Sj不相同的一個I/O序列，向被測系統輸入該I/O序列的輸入事件序列，并檢查被測系統的輸出事件序列：

9a)如果輸出事件序列與有限狀態機規定的在待驗證狀態Si下的輸出事件序列不相符，則待驗證狀態不是預期狀態，結束本次狀態驗證過程；

9b)如果輸出事件序列與有限狀態機規定的在待驗證狀態Si下的輸出事件序列相符，將狀態Sj從校驗狀態集合N中刪除，并判斷校驗狀態集合N是否為空：

9b1)如果校驗狀態集合N不為空，則執行步驟(7)；

9b2)如果校驗狀態集合N為空，則證明待驗證狀態為預期狀態，執行步驟(10)；

(10)將上述待驗證狀態Si從待驗證狀態集合M中刪除；

(11)重復步驟(3)到步驟(10)，直到待驗證狀態集合M中的所有狀態均被驗證為止。

2.根據權利要求1所述的方法，其中所述步驟(1)中的等價狀態，是指在有限狀態機中的兩個或多個狀態，它們對于相同的輸入，有相同的輸出，而且能轉換到相同的狀態。

3.根據權利要求1所述的方法，其中步驟(2)所述的求出有限狀態機內各狀態的UIO序列，按如下步驟進行：

(2a)從有限狀態機內所有狀態中任取一個狀態Sa；

(2b)設狀態集合P是從Sa經過1步就能到達的狀態的集合，檢查從Sa到狀態集合P中所有狀態的1步路徑中是否有I/O行為唯一的路徑：若有，則該I/O行為就是Sa的UIO序列，執行步驟(2d)；否則，執行步驟(2c)；

(2c)設狀態集合Q是從Sa經過n步就能到達的狀態的集合，n≥2，檢查從Sa到狀態集合Q中所有狀態的n步路徑中是否有I/O行為唯一的路徑：若有，則該I/O序列就是Sa的UIO序列，執行步驟(2d)；否則，n＝n+1，重新檢查從Sa到狀態集合Q中所有狀態的n步路徑中是否有I/O行為唯一的路徑；

(2d)從有限狀態機內任取仍未求出UIO序列的狀態，執行步驟(2b)，直到求出狀態集合N中所有狀態的UIO序列為止。