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

有效

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

技術領域

本發明屬于Web服務組合規則的形式化驗證領域，具體涉及到一種基于模型檢測的服務規則路由的正確性驗證方法。

背景技術

隨著企業信息化的發展，傳統的軟件架構已經不能滿足多個應用集成的需求。面向服務架構（Service?Oriented?Architecture，SOA）思想的提出在一定程度上解決了這個問題。企業服務總線（Enterprise?Service?Bus，ESB）作為SOA架構主要的基礎設施，已經成功應用在電信、金融等多個領域。當使用ESB集成應用系統時，各個應用將自己的業務功能封裝為服務部署在總線上，不同應用之間的交互通過服務的組合和交互完成，具體的傳輸協議和消息格式的轉換則由總線實現。ESB減少了應用集成代價，但消息的路由規則分散在代碼中，當業務規則改變時，需要修改源代碼以應對由此引起的消息路由規則的改變，從而使得系統的維護成本增加。

將業務規則從業務流程中提取出來，即在傳統的ESB中引入規則引擎，使得不同服務之間的消息基于獨立的規則進行路由，當規則變更時，直接修改相應的規則配置信息即可，可大大降低系統的維護成本。實現基于規則的消息路由，一個核心問題是如何檢測消息路由的正確性，例如：組合服務的實際運行結果是否與用戶期望的目標結果相一致，是否出現引起死鎖的循環調用，等等。

發明內容

本發明針對現有技術的不足，提供了一種基于NuSMV的服務組合規則路由的正確性驗證方法。

本發明方法的具體步驟是：?

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

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

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

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

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

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

本發明中NuSMV是一種經典的模型檢測工具，本發明所提供的基于NuSMV的服務組合規則路由的正確性驗證方法由一組功能模塊組成，它們包括：原子服務六元組模型生成模塊、組合服務六元組模型生成模塊、NuSMV驗證程序生成模塊和正確性驗證模塊。

原子服務六元組模型生成模塊根據表示服務信息和路由規則信息的服務模型生成每個原子服務的六元組模型。

組合服務六元組模型生成模塊合并每個原子服務的六元組模型，生成表示整個業務流程的組合服務六元組模型。

NuSMV驗證程序生成模塊根據組合服務六元組模型，生成完整的NuSMV驗證程序，包括定義狀態變量和消息變量以及它們的初始值，使用?next語句定義狀態變量的轉換關系。

正確性驗證模塊輸入使用分支時序邏輯CTL或者線性時序邏輯LTL描述的待驗證的性質，運行NuSMV驗證程序，對性質進行驗證，對于不滿足的性質給出反例。