基于有限状态机的Web服务测试用例生成方法

提出了一种基于有限状态模型（FSM）的测试用例生成方法。首先,FSM中的状态由Web服务与用户交互产生的中间状态表示,FSM中的状态迁移及其标注由Web服务与用户间的消息交换表示;其次,借助正则表达式来描述Web服务交互过程的所有消息交换序列,并与Web服务的WSDL文档结合产生测试数据;最后,给出了满足FSM迁移覆盖准则的测试用例生成算法,并通过实验验证了该方法的有效性。     

基于符号模型检测的Web服务组合形式化验证

随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求。Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题。针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息会话的Web服务有限状态自动机的形式化定义。最后实例验证了Web服务组合交互的正确性和有无死锁状态现象,进一步证明了方法的可行性。     

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

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

物联网需求驱动的服务组合方法

为实现依据用户需求动态地组合原子服务, 形成服务集合, 提出一种基于本体的服务组合方法。首先对物联网服务进行多视图建模, 使用服务交互模型描述服务与物理实体的交互过程, 服务功能模型刻画物理世界中服务的属性和行为, 服务状态模型表示服务引起的期望状态变化, 并采用扩展的OWL描述面向物理对象的服务。同时, 采用多维QoS模型对用户的需求进行建模, 使用语义的方法进行服务的匹配与组合, 并基于QoS选择满足约束的服务。最后, 通过案例研究和实验验证了所提方法的正确性和有效性。     

语义标记Petri网的组合Web服务建模与验证(英文)

随着Web服务组合的发展,整合业务过程成为可能。组合Web服务可以被看作是基于过程的工作流。由于死锁、不安全和不可达等流的设计错误会影响组合Web服务的有效执行,因此这些错误应在组合Web服务执行前被检测出并修改。提出了基于语义标记Petri网的组合Web服务建模与验证方法。首先提出语义标记Petri网(SaPNs),并给出其语义;用受限描述逻辑tableau算法获得组合Web服务;使用SaPNs描述组合Web服务及其组成部分;最后,使用基于SaPNs的分析方法验证了组合Web服务。使用该方法在开放的Internet环境下可以获得满足客户需求的、可靠的组合Web服务。     

EDG—DCR：一种基于扩展有向图Web服务组合关系描述方法

Web服务组合是充分利用已有的Web服务,生成满足不同用户实际需要的组合服务的重要技术,Web服务组合关系的描述是Web服务组合的基础。目前,Web服务组合关系描述主要有两类方法,一是基于有向图的描述方法,二是基于Petri网、语义的描述方法。前一种方法简单,但不能描述所有的组合关系;后一种方法虽然能描述所有的组合关系,但是它们的组成元素过于复杂,用户难以理解和使用。文章以工作流模式为基础,提出一种基于扩展有向图的Web服务组合关系描述方法,使得其可以描述所有的组合关系。该描述方法使用XML Schema表示组合关系,保证描述过程的简单性、开放性和可扩展性。     

基于Petri网的Web服务自动组合研究

根据Web服务中消息和行为的关系,Web服务被描述为面向消息的基于行为Petri网模型(Moap)．该模型包括消息域和服务过程,前者是服务协同以及和用户通信的通道,后者是基于Petri网的Web服务行为过程描述．Moap支持组合服务的重用,可以很好地描述可用服务的并行调用,另外元消息机制也有利于服务的自动组合．在Moap基础上,定义了服务组合系统和服务的协同;给出了服务自动组合规则,并证明了其有效性和完备性．最后,通过一个实例直观描述了服务组合系统的工作方式．     

一种验证服务组合中消息语义匹配的方法

介绍一种服务组合模型中服务消息语义化匹配验证的方法.该方法先介绍基于服务行为模型的服务组合,并将其转换为形式化的有限状态自动机.利用有限状态自动机中服务行为可以转换为线性逻辑表达式描述的原理,使用线性逻辑的演绎方法对服务消息的匹配性可满足性进行验证.     

基于工作流模式的OWL-S过程模型分析及其应用

确定OWL-S过程模型描述Web服务之间交互协议的能力和缺陷，为组合Web服务执行提供有效支持。将组合web服务视为基于Web服务的工作流，利用OWL-S过程模型的控制结构给出工作流模式的实现方案，分析出OWL-S描述web服务之间交互协议的能力及缺陷；在此基础上，设计并实现基于OWL-S的组合web服务执行工具，通过验证Web服务调用的有效性及Web服务之间交互协议的有效性，提高组合Web服务执行的健壮性。     

Web服务编排场景的XML Schema消息类型精化

Web服务(Web Services)编排描述了Web服务组合的交互行为,在实际开发中,Web服务组合的实现可能存在交互的数据类型、交互序列与编排规范不相符的情况,为了测试Web服务(组合)与编排的相符性,需要从编排规范生成测试用例。由于编排场景描述了编排中各个参与方的交互序列及其交互消息的XML Schema类型,从而可以根据场景中的XML Schema类型生成测试数据。由于XML Schema类型中指示器的作用导致类型的不确定性,需要解决XML Schema类型精化问题,为此提出了基于组合测试的XML Schema类型精化方法。通过定义XML Schema类型树,给出了基于组合测试工具Cascade的类型精化算法,并通过实例表明该方法的有效性。     

基于答案集的Web服务组合验证

语义Web服务组合的形式化描述和验证,是保证组合服务能正确运行的重要前提基拙。首先描述基于答案集编程(Answer Set Programming)的OWL-S建模方法,并分析基于答案集编程建模的优势。然后给出OWL-S流程模型中几种控制结构到中间模型Petri网的映射,并提出由Petri网生成答案集编程的算法。同时将时态约束引入到 组合服务验证中,利用时态约束表达待验证性质,将验证问题转换为求解逻辑程序的答案集。最后通过一个具体的实例说明该方法的有效性。     

航空订票业务的Web服务建模及组合兼容性验证

Web服务通过组合基本服务为解决复杂问题提供了方法,于是近年来越来越受到关注。当前交互式下的Web服务在实际组合中还存在诸多问题,其中就包括Web服务组合验证问题。运用Pi演算对航空订票业务的Web服务进行形式化建模,改进基于Pi演算的推理,提供一种验证多个Web服务组合是否兼容的方法。为证实该验证方法,进一步采用MWB工具展示了Web服务组合兼容性的验证过程。     

Synchronizability of conversations among Web services

We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the reliability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.     

Using Policies to Manage Composite Web Services

When no single Web service can fulfil a user's request, providers often turn to composite Web services. However, developing a composite Web service is not simple and deploying the composition specification at runtime consists of several processes. Developers and deployers of composite Web services can use policies in various scenarios, from the announcement of Web services to the compatibility between Web services and composite Web services. Mapping guidelines for a Web service's behavior to policies can ensure an individual Web service's smooth engagement into a composite Web service     

基于Petri网的Web服务组合验证方法

对服务组合进行结构验证分析的目的在于发现结构中固有的致命弱点,保证运行时的Web服务组合是良结构的.Web服务组合的有界性验证用来判断是否存在影响Web服务组合实施的Web服务或子Web服务组合;死锁验证用来发现是否存在可能的服务盲区;陷阱验证用来发现是否存在可能的服务异常区.给出了上述各项验证的实现算法,测试实验验证了该算法的正确性.     

服务组合BPEL测试序列生成研究

为更好地对Web服务组合的控制流进行分析和验证,提出一种映射转换模型和测试序列生成算法。首先解析基于BPEL的Web服务组合流程描述文件,然后对流程描述文件进行图形化转换,形成业务流程编排控制流程图,再采用路径推导算法对控制流程图进行解析,获取基于BPEL的服务组合的所有测试执行路径,最后通过一个服务组合实例证明模型及算法的有效性。该方法解决了测试路径的自动生成和全覆盖问题,保证了测试的充分性,提高了路径生成效率。