正确性保证的组合服务综合问题复杂度研究  

Complexity of synthesis of composite service with correctness guarantee

作　　者：邓婷[1,2] 怀进鹏[1,3] 沃天宇[1,3] 

机构地区：[1]国家软件开发环境重点实验室,北京100191 [2]北京航空航天大学数学与系统科学学院,北京100191 [3]北京航空航天大学计算机学院,北京100191

出　　处：《中国科学：信息科学》2012年第7期789-802,共14页Scientia Sinica(Informationis)

基　　金：国家重点基础研究发展规划(批准号:2011CB302602)资助项目

摘　　要：Web服务应用中一个富有挑战性的关键问题是:如何自动组合已有的Web服务并保证组合的正确性(如以时态逻辑LTL,CTL,CTL*等公式规范的时态性质).现有研究工作大多延用传统软件开发中的设计、验证、分析和纠错的过程,这使得组合过程既复杂又低效.文中研究了基于CTL与CTL*的组合服务综合问题,即利用已有Web服务自动生成满足给定的CTL,CTL*逻辑公式的组合服务,从而可以无需另外的验证过程,避免反复进行组合.证明了以CTL与CTL*逻辑公式为组合需求时,组合服务综合问题分别为EXPTIME–完全和2EXPTIME–完全问题.同时讨论了当综合失败时,如何通过合理限制环境(即服务的交互对象,如用户或其他服务)的输出使得综合成功,并证明了该问题关于CTL与CTL*逻辑公式同样分别为EXPTIME–完全和2EXPTIME–完全问题.How to compose existing web services automatically and to guarantee the correctness of the design （e.g. temporal constraints specified by temporal logic LTL, CTL or CTL＊） is an important and challenging problem in web services. Most existing approaches use the process in conventional software development of design, verification, analysis and correction to guarantee the correctness of composite services, which makes the composition process both complex and time-consuming. In this paper, we focus on the synthesis problem of composite service; that is, for a given set of services and correctness constraint specified by CTL or CTL＊ formula, a composite service is automatically constructed which guarantees that the correctness is ensured. We prove that the synthesis problem for CTL and CTL＊ are complete for EXPTIME and 2EXPTIME, respectively. Moreover, for the case of synthesis failure, we discuss the problem of how to disable outputs of environment （i.e. users or services） reasonably to make synthesis successful, which are also proved complete for EXPTIME and 2EXPTIME for CTL and CTL＊, respectively.

关 键 词：业务协议 WEB服务 组合服务 综合 环境 时态逻辑 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]