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

作者：陈圣标; 吴剑峰; 张广泉

来源：苏州大学学报(自然科学版), 2011, (01): 32-38.

• 限界模型检测
• Web服务
• 服务失配
• NuSMV Bounded Model Checking
• Web services
• service mismatch
• NuSMV

目前,Web服务组合已成为Web服务领域的研究热点,Web服务失配检测是保证服务正常组合的基础.当服务模型状态数较大时,现有的失配检测方法将面临状态空间爆炸问题,本文采用限界模型检测技术,提出一种基于NuSMV的Web服务失配检测方法.该方法能够有效地处理服务模型状态数较大时的情形,并且能够实现在异步通信模式下进行Web服务失配的自动化检测.最后通过实验说明了该方法的可行性.

• 单位
  中国科学院; 计算机科学国家重点实验室; 苏州大学