中文摘要：

服务可替换性分析是服务无缝集成与协作领域的一个重要问题,通过形式化的分析方法验证替换前后服务组合效果是否一致,有助于实现服务的动态组合.现有研究针对服务内部的操作和操作序列是否一致对服务的可替换性进行分析,会缩小可替换服务的空间.基于服务执行时的触发条件和结果提出了服务可替换性的定量判定方法.该方法采用有色Petri网对服务行为进行建模,将服务执行时的触发条件和结果定义为服务的行为效果,给出了行为效果一致的概念,并结合Petri网变换理论实现对服务可替换度的计算.最后通过定理证明了方法的有效性,这种定量分析的判定方法对于服务替换的正确建立和替换后组合服务的可靠执行具有重要作用.

英文摘要：

Web service composition is a key issue in Web service research area.Service replacement refers to the problem of identifying a service that can replace another service in the context of a composition with a specified functionality,and the analysis of service replaceability is an important issue for supporting seamless service integration and collaboration.It is known that performing formal analyses to verify the consistency of the composition effect,before and after replacement,is helpful for service dynamic composition.Existing solutions to this problem rely on analyzing service replaceability of the service,according to both the consistency of operations and the operation sequence,but decrease the space of replaceable services.Consequently,the authors propose a determination method of service replaceability on service effect.They use colored Petri nets as formalism foundation modeling and specifying Web services and reasoning on behavioral features of Web services composition.The whole work is achieved by modelling the service behavior using colored Petri nets,defining the trigger condition and result as a behavior effect,introducing the concept of service behavior consistency,and listing the algorithms to implement the process.The theorem presented and proved illustrates that the analysis approach is very useful for correctly building and reliably executing the composing service after service replacement.