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

Web service modeling and composition based on bounded model checking

作　　者：李艳[1] 刘金江[2] 

机构地区：[1]山东理工大学计算机科学与技术学院,山东淄博255049 [2]南阳师范学院计算机与信息技术学院,河南南阳473061

出　　处：《计算机工程与设计》2011年第12期4079-4082,共4页Computer Engineering and Design

基　　金：河南省科技厅科技攻关基金项目(102102210483;102102210465);河南省重大科技攻关基金项目(092102110274)

摘　　要：针对面向服务架构(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.

关 键 词：有界模型检验 WEB服务组合 线性时态逻辑 服务社区 有限状态自动机 

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