[發明專利]一種基于NuSMV的服務組合規則路由的正確性驗證方法

有效

• 申請號: 201210134962.7
• 申請日: 2012-05-04
• 公開（公告）號: CN102710434A
• 公開（公告）日: 2012-10-03
• 發明（設計）人: 俞東進;殷昱煜;閆大強;劉志清
• 申請（專利權）人: 杭州電子科技大學
• 主分類號: H04L12/24
• 分類號: H04L12/24;H04L12/56
• 代理公司: 杭州求是專利事務所有限公司 33200
• 代理人: 杜軍

1.?一種基于NuSMV的服務組合規則路由的正確性驗證方法，其特征在于該方法的具體步驟是：

步驟(1)?對于每一個原子服務，建立表示其規則路由的六元組模型???????????????????????????????????????????????，其中表示一個原子服務所有狀態的集合，表示原子服務的初始狀態，表示原子服務的終結狀態集合，表示消息集合，表示消息標識集合，表示當前狀態接收消息后達到下一狀態，表示發送消息后到下一狀態，表示服務所有狀態之間的轉移關系的集合；

步驟(2)?將通過步驟(1)得到的所有六元組模型合并為表示整個業務流程的組合服務模型六元組；

步驟(3)?為組合服務模型服務六元組定義一個NuSMV驗證程序的狀態變量，取值范圍為組合服務模型六元組的狀態集合的所有狀態元素，初始值為狀態變量的初始賦值；

步驟(4)?根據組合服務模型六元組的消息集合創建NuSMV驗證程序的消息變量，初始值設置為具有實際意義的取值范圍之外的任意一個值；

步驟(5)?由組合服務模型六元組的狀態轉移關系集合中的初始狀態所在的轉移關系得到轉移后的狀態，由此定義對應該狀態變量的NuSMV驗證程序的next語句的一個條件及賦值；從該狀態及其所在的轉移關系得到狀態變量的next語句的下一個條件及賦值；依次交替進行，得到狀態變量的所有條件分支及賦值，其中狀態變量轉換關系的next語句的條件包括狀態變量的當前值和消息標識對應的消息變量的取值，最終生成NuSMV驗證程序；

步驟(6)?輸入使用分支時序邏輯CTL或者線性時序邏輯LTL描述的待驗證的性質，運行通過步驟(5)生成的NuSMV驗證程序，對性質進行驗證，對于不滿足的性質給出反例。