一种Web服务特征交互自动检测方法

模型检测技术可有效验证Web服务组合的异常情况,如特征交互问题等,但是目前验证过程的自动化程度比较低。为了提高验证的自动化程度,需要将BPEL转化为模型检测工具的输入语言。在分析BPEL语言控制流程的基础上,提出BPEI、活动执行的形式化模型,给出活动执行语义,进而分别提出将BPEL流程自动转换为七元组集合以及将这些七元组转化为MCTK(一种我们开发的符号化模型检测工具)输入语言的算法,这些七元组包含了智能体执行过程中有关状态变化的有效信息。实验表明,提出的算法可以有效验证Web服务中的特征交互问题,而且支持认知逻辑规范的验证。     

一种基于认知模型检测的Web服务组合验证方法

近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法,将Web服务组合建模为多主体系统,在分析BPEL语言控制流程基础上,提出BPEL活动的形式化模型,给出活动执行...     

基于时态认知逻辑的Web服务模型检测

传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题.而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述.Web服务是一个典型的分布式系统.把Web服务组合建模为多智能体系统,并成功采用我们实现的时态认知逻辑符号模型检测工具MCTK验证了SAS股票分析服务实例.同时采用WSAT,WS-Engineer和SPIN 3个模型检测工具在相同实验环境下验证了该实例,实验结果表明我们的Web服务模型检测方法不仅比这3个模型检测工具更高效,而且支持认知逻辑规范的验证,这是这3个模型检测工具所不具备的.     

Web服务的形式化验证

将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模,并验证该实例。实验结果表明,基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。     

基于Verics的组合Web服务有界模型检测

传统的模型检测技术无法描述系统的认知逻辑特性,而在分布式系统领域,系统和协议的规范适合用多智能体时态认知逻辑来描述.组合Web服务是典型的分布式系统.为了保证组合Web服务运行的正确性,把组合Web服务看成多智能体系统,将其建模成一组相互通信的时间自动机.采用时态认知逻辑模型检测工具Verics对该组合Web服务的可用性、可靠性和时效性的时态认知逻辑特性进行检测.本文以旅游预订系统组合Web服务为例,阐述了上述过程.     

着色Petri网模型检测工具的扩展及其在Web服务组合中的应用

Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模型检测工具--CPN Tools--中使用ML(meta language)语言实现了这些算法,然后将扩展后的CPN模型检测工具应用在Web服务组合的验证问题中.该方法不仅可以验证Web服务组合是否存在逻辑错误,还能告诉用户发生错误的原因,为Web服务组合的验证提供了技术上的保障.实验表明对着色Petri网的模型检测工具的扩展是正确、有效的.     

基于Pi-演算的BPEL4WS Web服务组合形式化模型

Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型来可以用来检查、验证Web服务组合以保证组合的正确性。Pi-演算是一种适合于Web服务组合建模的进程代数。本文介绍了P-演算的基本语法,针对目前最主要的一种描述和执行基于工作流模式的Web服务组合的规范-Web服务商业流程执行语言（Business Process Execution Language for Web Services,BPEL4WS）,定义了Pi-演算和BPEL4WS之间的概念映射,并给出了BPEL4WS的基于P-演算的形式化模型,最后通过一个案例给出了模型验证的方法。     

基于动作时序逻辑的Web服务组合

为了更有效地实现Web服务组合,提出一种使用动作时序逻辑TLA(Temporal Logic of Actions)进行Web服务组合的方法.Web服务组合与工作流有着共同特征,首先根据工作流的基本控制模式,将服务之间的关系用TLA进行描述,然后提出了基于图的宽度优先搜索的Web服务自动组合算法,并采用TLA模型检验器TLC验证组合逻辑的正确性以及是否存在死锁问题,最后给出了现有的Web服务组合平台BPEL4WS向TLA转化的方法.     

面向服务的多参与者协调事务建模方法

为了保证Web服务组合执行获得正确一致的结果,用形式化方法研究Web服务事务处理的协调过程是很重要的。基于Web服务事务规范(Web services transaction,WS-TX),提出了一种由业务流程执行语言(business process execution language,BPEL)自动生成Web服务多参与者协调事务模型的方法。介绍了Web服务协调的Pi-演算建模方法,阐述了如何由BPEL描述的业务流程建立服务协调事务模型,进一步给出了自动生成该协调模型的算法描述,并通过具体实例说明了该方法的正确性及可行性。     

Web服务组合事务处理研究与实现

通过重用已有的服务进行服务组合来实现应用集成;而保证服务组合的事务特性是实现服务组合的关键。文中提出一个Web服务组合事务处理模型,将BPEL (Business Process Execution Language,业务流程执行语言)的流程设计与WS-C/T (Web Services Coordination/Transaction,Web服务协调/事务)规范结合。该模型主要由客户端、BPEL执行引擎、事务协调器和参与者四个部分组成。客户端发起请求,BPEL执行引擎响应请求并开启事务,事务协调器和参与者根据事务协调算法完成事务协调。     

Verifikation von Webservicekompositionen:

Web service compositions coordinate Web services of different enterprises. They are expected to constitute the foundation of service-oriented architectures, to improve business processes as well as to foster intra- and inter-organizational integration. Especially in inter-organizational contexts, quality of service referring to non-functional requirements and conformance to functional requirements are becoming vital properties. With Web service compositions being asynchronous and distributed systems, the latter property – which is also called correctness – can be shown best by verification. This paper examines from a system-theoretic perspective how correctness can be operationalized for Web service compositions. It also proposes a requirements framework for service-oriented modeling techniques so that correctness can be shown by verification and Web service compositions can be modeled intuitively. In order to show the framework’s principle applicability, an example approach is analyzed with respect to the corresponding requirements.     

一种基于广义随机Petri网的Web服务组合性能预测模型

Web服务交互消息受到不可预知的网络环境的影响,因特网环境中的个体Web服务的性能表现与访问者的地域位置有关。于是,服务组合的性能则更加容易受到网络环境因素的影响。同时,服务组合的性能还会受到服务组合流程中不同的分支执行概率的影响。在这种情况下,服务组合建模只考虑组合本身,而不考虑网络环境因素和分支执行概率,这将会对模型的预测结果造成较大的偏差。为了能够真实地评估服务交互行为、网络环境与分支执行概率之间的关系,提出了一种基于广义随机Petri网的Web服务组合性能预测模型,该模型不仅引入了伙伴服务性能方面的因素,而且充分考虑了网络环境因素和分支执行概率,从而能够对被建模系统进行定性和定量分析,进而指导服务组合性能优化。     

Declarative Web services composition using proofs

Over the last decade, Web services composition has become a thriving area of research and development endeavors for application integration and interoperability. Although Web services composition has been heavily investigated, several issues still need to be addressed. In this paper, we mainly discuss two major bottlenecks in the current process of modeling compositions. The first bottleneck is related to the level of expertise required to achieve a composition process. Typical procedural style of modeling, inspired by workflow/business process paradigm, do not provide the required abstractions. Therefore, they fail to support dynamic and self-managed compositions able to adapt to unpredictable changes. The second bottleneck in current service compositions concerns their life cycle and their management, also called their governance. In this context, we propose a declarative proof-based approach to Web service composition. Based on the three stages of pre-composition, abstraction, and composition, our solution provides an easy way to specify functional and non-functional requirements of composite services in a precise and declarative manner. It guides the user through the composition process while allowing detection and recovery of violations at both design and run-time using proofs and planning. Experiment results clearly show the added value of the proof-based solution as a viable strategy to improve the composition process.     

The design with object (DwO) approach to Web services composition

Web services are being adopted, more and more, as a viable means of accessing Web-based applications. With a Web-native XML based solution, Web services can, thus, tackle the problem of heterogeneous sources and make them inter-operable. At present, there is a trend towards deploying business processes as composite Web services, known as Web services compositions. Web services compositions are synthesized by researchers from elementary web services, offering the opportunity for service providers and application developers to create value-added services, through Web services composition. However, a problem exists in the current distribution process of Web services compositions: the general analysis and selection of services can be overly complex and un-systemic. There is a need to manage composite Web services, based on these emerging technologies, but the research related to ranking candidate services and selection of optimization strategies is sparse. Nothing has yet been published that considers the constraints of non-functional service properties. In this paper, a design with object (DwO) approach is proposed. This has the advantage of being an object-orientated concept, which characterizes (i) changing the design object without directly changing the Web services themselves, and (ii) information hiding. A systemic but complete composition process is also proposed for Web services composition, which shows great promise in the emerging demand for composite Web services.     

Web服务的Pi演算描述

如何从已有的 Web 服务构造新的增值性的正确的 Web 服务,已成为研究 Web 服务的群体关注的一个焦点。因此,为了得到可靠的、高质量的服务,必须找到一种建模方法和工具,在 Web 服务投入使用之前,对其进行分析和验证。本文主要从过程代数的角度出发,用 Pi 演算来描述 Web 服务以及 Web 服务的组合。     

基于本体和QoS的Web服务组合

服务组合是一种重要的服务应用形式,为服务重用与自动化集成提供了支撑。传统服务组合方法依赖基于关键字的查找,缺乏服务语义的分析,且现有服务组合算法往往未考虑QoS的因素。文章将语义本体和QoS结合起来,共同作为Web服务选择和组合的条件,以提高服务组合的质量和组合结果的执行效率。仿真实验结果显示出该方法较传统组合方法能够获得更好的组合结果,使应用的服务性能得到改善。     

Constrained evolutionary computing approach to Web service compositions

Web services are being adopted as a viable means of accessing Web-based applications. Web services are not only used to exchange information between enterprises but also to help software developers provide value-added services for various demands. Web service compositions are synthesised by researchers from elementary Web services, offering the opportunity for service providers and application developers to create value-added services. However, a problem exists in the current distribution process of Web service compositions: the general analysis and selection of services can be overly complex and are completed manually. Therefore, there is a need to manage composite Web services automatically. But the research related to ranking candidate services and selection of optimisation strategies is sparse. Yet, few have been published that consider the constraints of non-functional properties. In this article, a systemic but autonomous composition process has been proposed. This study proposes an evolutionary approach that applies the characteristics of the object-oriented concept of Web services and the genetic algorithm to effectively manage and optimise the Web service composition. It is capable of escaping not only from local optima due to a population-based approach, but also from unbiased nature, which enables it to perform well in a situation with little domain knowledge. In this article, the related literature is reviewed. Then, the Web service composition model incorporated with a genetic algorithm is proposed. Finally, a practical implementation is illustrated and shows a good result in terms of solution quality.     

一种基于CPN的运行时监控服务交互行为的方法

BPEL对Web服务组合的描述特性使得它很难表达和分析服务组合中的交互行为属性.这些行为属性需要遵循一定的交互协议.然而良定义的交互协议还是容易受到侵犯,这将导致服务组合进程产生状态不一致的问题.为了解决这类实际交互行为与其服务组合描述之间的不一致性问题,提出了一种由BPEL描述自动构造运行时监控器的方法.首先提出了一种基于有色Petri网(CPN)的形式化表示模型以及服务组合规约到模型的映射方法,用于精确表达从BPEL流程描述中提取的服务交互行为规约.然后,描述了由CPN形式化表示模型生成运行时监控器的方法.该运行时监控器能够捕获所有进出服务组合进程的交互消息,并且检测是否存在违背交互协议的行为.