一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

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

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

基于Pi演算的OWl-s的Web服务的自动组合

Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型可以用来检查、验证Web服务组合以保证组合的正确性。针对目前最主要的一种语义Web服务组合的规范WEB本体论语言(Ontology Web Langage-Semantic,简称OWL-S),给出基于Pi演算的形式化描述,定义了Pi演算和OWl-S之间的概念映射,并给出了OWl-S的基于Pi演算的形式化模型,最后通过一个案例给出了模型验证的方法。     

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

基于Pi-演算的Web服务组合的描述和验证

形式化方法对于建模和验证软件系统是一种有效的方法,所以对Web服务的形式化描述和验证是一个重要的研究方向．对于Web服务及其组合来说,保证其组合正确性以实现其服务增值是十分必要的．Pi-演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模．该文基于Pi-演算对Web服务及其组合进行形式化描述和建模．文中说明了Pi-演算与以前形式化方法的不同之处,分析了Pi-演算应用于Web服务组合需要解决的问题．讨论了Pi-演算与Web服务协议栈的对应关系,说明了利用Pi-演算建立Web服务组合模型的规则,指出了如何寻找代理和通道．最后建立了一个实际的模型,并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证．     

基于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服务组合进行介绍;然后对Web服务组合给出形式化的定义,并对语义Web和OWL-S进行了分析;接着给出了一个基于语义Web的动态服务组合模型;最后讨论了存在的问题。     

一种基于Petri网的Web服务组合安全性动态检测技术

Web服务组合安全性检测对提高Web服务组合在复杂网络环境下的安全性具有重要意义。针对Web服务组合安全检测存在的问题,提出了一种Web服务组合安全性动态检测框架,并对其中的服务组合流程建模技术、安全模型以及安全检测算法等关键技术进行了详细分析,最后通过实例进一步说明该框架能够实现安全性检测的基本功能。     

基于MAS模型检测与抽象的Web服务验证

Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统( MAS)模型检测工具( MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。     

数据和时间感知的Web服务组合模型检测

为了验证Web服务组合中的数据属性和时间属性,提出了一种基于数据和时间感知的服务模型DTSM的Web服务组合模型检测方法。首先将I3PEL描述的Web服务组合转换为含有数据流信息和时间信息的形式化模型,然后将该模型映射至UPPAAL规约,最后应用模型检测工具UPPAAL实现了Web服务组合的正确性验证。     

一种验证Web服务流程的新方法*

在实际的服务组合中,Web服务流程（process）的验证(verification)对于Web服务的组合实现和应用具有重要意义——通过验证可以证明一个组合服务的控制流满足某个重要或者期望的属性,如不包含死锁或不包含无限循环,诸如此类;而服务提供者可对Web服务流程进行验证,以确保所提供的Web服务是完全正确的。然而,针对这两种语言的验证方法较少被人们注意。提出一种验证Web服务流程的方法,该方法使用时序行为逻辑（TLA）建模服务流程,然后,利用模型检验（model checking）技术验证模型的某些属     

基于WS-BPEL 的Web 服务组合技术

随着Web服务技术的不断发展,越来越多的Web服务已经发布在互联网上。然而独立的Web服务功能通常有限,不能满足用户或企业实际应用的需求。因此,Web服务的组合显得越来越重要。介绍了Web服务组合和WS-BPEL的相关知识,使用最新的业务流程执行语言WS-BPEL描述业务流程,在J2EE集成开发环境下设计并实现了基于业务流程思想的贷款审批应用实例,在Web服务执行引擎Active BPEL上进行部署,对Web服务进行了有效的组合。     

面向动态工作流的Web服务组合

利用动态工作流模型,将Web服务的组合过程与工作流的过程模型有机结合起来,从而建立面向动态工作流的复合服务。在复合服务的执行过程中,通过引入服务评价函数,并根据工作流过程模型中所定义的各项任务之间的业务逻辑与业务规则,最终实现工作流任务的动态绑定与执行。     

Process-context aware matchmaking for web service composition

Web service composition can help software developer design more powerful and flexible applications according to requirements of enterprise. But during compositing, how to discover suitable web services is a critical problem in design and implementing application-oriented web service technologies. The traditional keyword-based matchmaking approach is difficult to help developer to find suitable service. Current researches find that to attaching semantics to each registered service can help improve the precision of matchmaking. The improvement can help developer find more suitable service for business process. This paper proposes a novel approach of semantics-based matchmaking, which is named process-context aware matchmaking. The process-context aware matchmaking discovers the suitable service during web service composite modeling. During matchmaking, the approach utilizes not only semantics of technical process but also that of business process of a registered service, thus further improving the precision of matchmaking. We integrate the process-context aware matchmaking with business-process-driven web service composition in an integrated development environment based on Eclipse. The performance evaluation shows that performance overhead of this novel approach is acceptable.     

Semantic web service composition testbed

A huge amount of web services are deployed on the Web, nowadays. These services can be used to fulfill online requests. Requests are getting more and more complicated over time. So, there exists a lot of frequent request that cannot be fulfilled using just one web service. For using web services, composing individual services to create the added-value composite web service to fulfill the user request is necessary in most cases. Web services can be composed manually but it is a too tedious and time consuming task. The ability of automatic web service composition to create a new composite web service is one of the key enabling features for the future for the semantic web. There are some successful methods for automatic web service composition, but the lack of standard, open, and lightweight test environment makes the comparison and evaluation of these composition methods impossible. In this paper we propose an architecture for a light weight and scalable testbed to execute, test and evaluate automatic web service composition algorithms. The architecture provides mandatory components for implementing and evaluation of automatic web service composition algorithms. Also, this architecture provides some extension mechanisms to extend its default functionalities. We have also given reference implementations for web service matchmaking and composition. Also, some scenarios for testing and evaluating the testbed are given. We have found that the performance of the composition method will dramatically decrease as the number of web services increases.     

Computing performance requirements for web service compositions

In order to produce service compositions, modern web applications now combine both in-house and third-party web services. Therefore, their performance depends on the performance of the services that they integrate. At early stages, it may be hard to quantify the performance demanded from the services to meet the requirements of the application, as some services may not be available or may not provide performance guarantees. The authors present several algorithms that compute the required performance for each service from a model of a service composition at an early stage of development. This is also helpful when testing service compositions and selecting candidate web services, enabling performance-driven recommendation systems for web services that could be integrated into service discovery. Domain experts can annotate the model to include partial knowledge on the expected performance of the services. We develop a throughput computation algorithm and two time limit computation algorithms operating on such a model: a baseline algorithm, based on linear programming, and an optimised graph-based algorithm. We conduct theoretical and empirical evaluations of their performance and capabilities on a large sample of models of several classes. Results show that the algorithms can provide an estimation of the performance required by each service, and that the throughput computation algorithm and the graph-based time limit computation algorithm show good performance even in models with many paths.     

Web服务测试研究

Web服务技术为软件测试研究带来了新的挑战。Web服务测试需要能够适应面向服务的新的分布式计算体系架构。为保证服务的质量，Web服务需要从多个层次进行验证与确认，包括基础设施、单元服务、集成服务等；测试需涵盖服务的功能、性能、可靠性、安全等各个方面。本文从web服务体系架构和应用模式出发，讨论了Web服务测试的主要问题。文章分析当前相关研究的现状，并归纳总结了SOAP协议验证、WSDL语言扩展、基于模型的服务集成验证、和测试构架等主要研究成果。本文最后讨论了当前存在的主要问题及进一步的研究方向。     

Web服务核心支撑技术:研究综述

随着电子商务的迅速崛起,基于Web的应用模式迅速发展,Web应用从局部化发展到全球化,从B2C(business-to-customer)发展到B2B(business-to-business),从集中式发展到分布式,Web服务成为电子商务的有效解决方案.Web服务是一个崭新的分布式计算模型,是Web上数据和信息集成的有效机制.Web服务的新型构架,Web服务的高效执行方式,Web服务与其他成熟技术的有机结合以及Web服务的集成是解决现实应用问题的重要技术.从Web服务研究的不同侧面对其进行了综述,阐述了Web服务的基本概念,分析了当前Web服务的主要研究问题及其核心支撑技术,概括了Web服务中的数据集成技术、Web服务的组合、语义Web服务、Web服务发现,Web服务安全,P2P(Peer-to-Peer)新型计算环境下的Web服务解决方案和网格服务等方面的研究内容,并对这些技术进行了总结,结合已有的研究成果,展望了Web服务未来的研究方向及其面临的挑战.     

A high performance backoff protocol for fast execution of composite web services

Using web services to expose applications over the Internet is now a widely accepted practice. Currently, there are several ongoing efforts that provide ways to effectively compose web services distributed across different organizations. One of the problems underlying the deployment of such composite services on the web, however, is service co-allocation that arises when a composite service needs to ensure all the required component services to be available for execution at the same time. Motivated by this, this paper presents a new decentralized protocol, named web service co-allocation protocol (WSCP), which can facilitate fast execution of composite web services. The proposed framework is an enhancement of the famous two phase commit protocol through the incorporation of tentative hold phase as well as the employment of a new high performance backoff protocol developed to better address the dynamics of the service co-allocation problem. The simulation results show that the proposed approach yields significant improvements over existing protocols.     

面向服务的企业应用集成系统描述与验证

在对当前面向服务体系架构(service-oriented architecture,简称SOA)研究的基础上,给出了一个以企业服务总线(enterprise service bus,简称ESB)为中心的面向服务软件体系架构参考模型(SOA reference model,简称SOARM),是集Petri网和时序逻辑于一体的形式化SOA分析、验证和确认方法.基于以客户为中心的面向服务架构设计理念,即根据用户提出系统规范/需求,服务提供者提供服务或组合服务来满足服务消费者,服务接口和ESB作为实现面向服务架构的关键部分.虚拟计算环境下,服务语义的一致性验证是十分必要的,SOARM采用新的模式:通过Petri网为服务的行为建模,时序逻辑来描述服务语义一致性约束,综合运用分而治之的精炼检测思想和SOA模型检测合成方法,通过对这些子服务性质的检验来验证整个系统的规范.用商业银行综合前置系统说明了如何使用这种方法来实现面向服务的设计.