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

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

基于上下文感知进程网络的Web服务组合方法

针对Web服务组合的个性化问题,提出一种基于上下文感知进程网络的Web服务组合方法,支持上下文感知组合系统的高层建模与系统的底层实现。采用CCS进程代数和标签转换系统,描述上下文感知组合模型的形式化语义,给出上下文感知系统模型的实现框架。分析结果证明了该组合方法的可行性。     

Web服务动态组合中QoS计算方法研究

通过在Web服务动态组合中引入形式化的服务质量(QoS)描述、服务提供商因子、服务消费者因子,提出基于层次分析法的QoS计算方法。该方法根据服务消费者期望值选择QoS因子,利用QoS权重值计算Web服务的质量,在此基础上给出一个基于QoS计算的Web服务组合模型,并通过实例计算,证明利用该QoS计算方法可以得到更高质量的增值服务。     

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

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

BPEL中基于有限状态自动机的Web服务自动组合

提出了一种基于有限状态自动机的Web服务自动组合方法,该方法能够自动实现BPEL中抽象业务流程与Web服务的绑定.以有限状态自动机模型形式化地定义了业务流程的外模式和内模式,将Web服务组合问题转化为有限状态自动机问题.利用有限状态自动机的笛卡儿积运算,得出了服务组合系统的行为描述.在此基础上,提出了组合服务存在性的判定依据,进一步给出了组合服务的计算方法,设计并实现了一个演示系统.     

基于B方法的Web Service组合描述和验证方法

对于Web Service及其组合来说，保证其组合的正确性是十分必要的。B方法是一个基于模型的形式化方法，有很强的结构化机制和很好的工具支持，对于建模和软件验证是一种有效的方法。该文基于B方法对Web服务及其组合进行了形式化建模，并能够利用B方法相对成熟和完善的模型检查工具，来完成模型的正确性验证。     

基于MDA的Web服务组合的研究及应用

随着已有Web服务数量的不断增加,如何利用这些现有的Web服务创建新的更复杂的Web服务成为一项新的研究课题。特别地,利用MDA进行Web服务合成已经成为研究的热点。提出了一种基于模型驱动架构的Web服务组合方法,将模型驱动软件开发方法学应用到Web服务组合中。针对WSDL语言给出了一个UML Profile for WSDL来建立与WSDL平台相关的静态结构模型,并给出了与WSDL平台相关的静态结构模型和WSDL语言之间的模型转化规则。并通过一个旅行代理服务的实例说明了方法的应用情况,验证了方法的可行性。     

基于拓扑序列归约的Web服务组合QoS度量算法

考虑有向无环图 (DAG)描述的组合服务模型,提出了一种新的组合服务QoS度量方法--基于拓扑序列归约的Web服务QoS度量方法（QCMTSR）。其借鉴迭代归约度量方法中的基本结构及QoS计算公式,定义了DAG图中的两类基本结构,串归约结构和并归约结构,并给出了两种基本结构的QoS属性计算公式;通过逐步归约DAG图拓扑序列中的每个节点,直至最后一个节点的QoS属性值就是组合服务的各QoS属性的度量结果。从理论上证明了QCMTSR算法适用于所有DAG描述的组合服务,并实验证明QCMTSR算法对可靠性和可用性能够更准确的度量。     

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

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

基于CSP的OWL-S语义分析与建模

为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。     

基于UML活动图的Web服务合成动态行为建模方法研究

描述了利用UML进行Web服务合成的建模方法,包括静态结构建模和动态行为建模两个方面,针对Web服务合成的动态行为建模部分,详细说明了利用UML活动图进行建模时需要注意的问题,如活动图的控制流模式与Web服务合成控制流模式的语义对应关系,所支持的数据模式,以及为了方便模型转换对活动图actions元素的概念扩展,给出了动态行为建模方法,并给出了基于OCL的转换规则以及UML活动图元素到BPEL4WS元素的映射关系,最后通过订单管理案例对所述方法进行验证,为Web服务合成提供了新的思路。     

Web服务组装中的隐私暴露分析方法

保护Web服务用户的隐私已经成为目前服务计算领域的一个研究热点,但它们很少关注Web服务组装中的隐私暴露问题。针对上述不足,提出了一种Web服务组装隐私暴露分析方法。首先利用超图对服务组装隐私暴露进行建模,并给出了相应的转换方法。在此基础上提出了最小隐私暴露代价算法,利用该算法分析了隐私暴露最小的服务组装方案。最后通过实例说明了该方法的正确性及有效性。     

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

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

动态Web服务组合研究

Web服务作为一种崭新的分布式计算模型，是Web上数据和信息集成的有效机制。动态Web服务组合作为一种灵活、快速集成信息的重要方法，成为开放异构环境中复杂分布应用的新的研究热点。本文首先分析了几种Web服务描述方式并给出了动态Web服务组合定义及模式；其次，结合目前存在的一些组合平台和框架，重点分析了基于工作流和基于AI规划的动态Web服务组合原理与典型应用，并分析了其它相关的一些动态Web服务组合策略；最后提出了动态Web服务组合面临的挑战和进一步的研究方向。     

UML模型到FSM模型的转换

通常可采用UML的各种图从Web应用不同方面对其进行建模.当对Web应用模型进行测试和验证时,需要分别考虑这些采用了不同图形描述的模型,这就带来了测试和验证的繁琐.如果将UML各种图转换到有限状态机(FSM)模型,则可以统一用FSM模型来表示、验证和测试.提出了基于状态迁移特性保持规则的UML到FSM的模型转换方法,特别针对UML状态图中的3种基本组成单元到FSM模型的转换,给出了各自的转换方法,并实现了原型工具UML2FSM.     

一个基于有色Petri网的自动Web服务合成模型

提出了一个基于有色Petri网的自动Web服务合成模型,为Web服务的合成提供语义支持,提高合成服务的可靠性和可维护性.该模型将服务的合成结构分成顺序、并发、选择、循环、置换5种合成结构.给出了Web服务基于有色Petri网的形式化定义.定义了一个封闭的Web服务合成算法,通过算法获得的框架能够对Web服务进行说明性的合成.定义了一个自动Web服务合成算法,通过该算法,可以对Web服务进行有人工指导的半自动合成和无人工指导的自动合成.     

基于价格进程代数的Web服务组合描述和成本分析

进程代数可有效地用于Web服务组合的描述和验证,然而缺乏对服务组合成本建模和分析的能力.提出一种扩展了价格信息的进程代数PPA, 在CCS基础上为进程动作和状态扩展价格函数, 给进程动作的执行标记价格,给进程的迁移状态标记成本.给出了PPA的语法和语义,定义了PPA成本弱互模拟并分析了其与CCS弱互模拟的关系,证明了PPA在CCS基础上扩展了成本建模能力,给出了成本状态空间构造算法,该算法支持选择成本优化的组合服务.实验分析了PPA用于Web服务组合成本建模和分析的可行性.     

支持Web服务组合与验证的形式化模型

针对Web服务的组合与验证问题,在范畴理论描述框架的基础上,引入进程代数描述服务组件的外部行为,为Web服务系统的架构描述建立了一种形式化的语义模型。Web服务作为范畴理论中的对象节点,服务间的交互和组合关系作为态射,从而以范畴图表的形式来描述服务网络。在形式化定义服务接口、Web服务、服务组合等概念的基础上,进一步分析讨论了服务组合和交互过程中的语义特性,给出了Web服务可替代性和服务请求可满足性的形式化定义。实例研究表明,该框架增强了Web服务架构的语义描述能力。     

Symbolic model checking composite Web services using operational and control behaviors

This paper addresses the issue of verifying if composite Web services design meets some desirable properties in terms of deadlock freedom, safety (something bad never happens), and reachability (something good will eventually happen). Composite Web services are modeled based on a separation of concerns between business and control aspects of Web services. This separation is achieved through the design of an operational behavior, which defines the composition functioning according to the Web services’ business logic, and a control behavior, which identifies the valid sequences of actions that the operational behavior should follow. These two behaviors are formally defined using automata-based techniques. The proposed approach is model checking-based where the operational behavior is the model to be checked against properties defined in the control behavior. The paper proves that the proposed technique allows checking the soundness and completeness of the design model with respect to the operational and control behaviors. Moreover, automatic translation procedures from the design models to the NuSMV model checker’s code and a verification tool are reported in the paper.