首页 | 本学科首页   官方微博 | 高级检索  
     


Complexity of synthesis of composite service with correctness guarantee
Authors:DENG Ting  HUAI JinPeng  & WO TianYu  State
Affiliation:Key Laboratory of Software Development Environment, Beihang University Beijing 100191, China; 2School of Mathematics and System Science, Beihang University, Beijing 100191, China; 3School of Computer Science and Engineering, Beihang University, Beijing 100191, China
Abstract: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.
Keywords:business protocol  composite service  synthesis  environment  branching temporal logic
本文献已被 CNKI 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号