基于NuSMV的Web服务失配限界模型检测  

Detect mismatching of Web Services using Bounded Model Checking based on NuSMV

作　　者：陈圣标[1] 吴剑峰[1] 张广泉[1,2] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]中国科学院计算机科学国家重点实验室,北京100190

出　　处：《苏州大学学报（自然科学版）》2011年第1期32-38,共7页Journal of Soochow University(Natural Science Edition)

基　　金：中国科学院计算机科学国家重点实验室开放课题(SYSKF0908);江苏省高校自然科学研究项目(08KJB520010);苏州大学"莙政学者"研究项目

摘　　要：目前,Web服务组合已成为Web服务领域的研究热点,Web服务失配检测是保证服务正常组合的基础.当服务模型状态数较大时,现有的失配检测方法将面临状态空间爆炸问题,本文采用限界模型检测技术,提出一种基于NuSMV的Web服务失配检测方法.该方法能够有效地处理服务模型状态数较大时的情形,并且能够实现在异步通信模式下进行Web服务失配的自动化检测.最后通过实验说明了该方法的可行性.At present,Web services composition has become a hot point in Web services area,and the detection of Web service mismatching is the base of combining services correctly.If the states of service model are numerous,the existing method will meet with state space explosion problem.Using bounded model checking,this paper proposes a method based on NuSMV for detecting mismatching of Web Services.This method can handle large state space effectively,and detect services mismatching automatically under the asynchronous communication mode.In the end,our experiment illustrates the feasibility of the proposed method.

关 键 词：限界模型检测 WEB服务 服务失配 NUSMV 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]