基于有界限模型检验的服务建模与自动组合

Web service modeling and composition based on bounded model checking

针对面向服务架构(SOA)体系的Web服务数量快速增长现状,为实现大规模服务场景下高效自动组合Web服务来满足用户复杂需求问题,提出一种基于有界模型检验的Web服务组合方法。其中,Web服务被建模为有限状态自动机,众多Web服务构成服务社区,Web服务组合需求由线性时态逻辑公式描述,通过有界模型检验器的系统化搜索,该方法能够从服务社区中自动地构建满足需求的Web服务组合。实验结果表明,该方法能够适应较大规模的Web服务组合场景。

Currently,the SOA in many fields of application is accepted,which result in the rapid growth of available web services.To meet user complicated needs effectively,a method of web service automated composition based on bounded model checking is proposed.Web services are modeled as a finite state machine and many web services constitute a service to the community.The user requirements are represented by the linear temporal logic formulas,the method can automatically construct solution from the community to satisfy the demand of user requests.Experiments show that this method can adapt to large-scale web service composition scenarios.