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

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

目前,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.