一种新的Web服务描述方法.pdf

一种新的Web服务描述方法1 刘慧，王红兵，王晨 东南大学计算机科学与工程学院，江苏南京（211189） E-mail：liuhui621@ 摘要：本文针对很多描述Web 服务的语言虽然从不同方面对Web 服务进行建模和规范，但 在Web 服务的行为表示上仍缺乏清晰语义和概念化模型的问题，基于有限状态自动机（FSA ） 理论，将Web 服务建模成一个有限状态自动机，对WSDL 进行扩展以表示服务行为，并引 入了动作时序逻辑（Temporal Logic of Action ，简称TLA ）的概念，用TLA 来形式化的描 述和规范服务行为，从而为形式化描述Web 服务提供了一个新的方法和途径。TLA 作为一 种强大的并发系统描述工具，研究其在Web 服务中的应用（如组合等）非常有意义。 关键词：Web 服务，WSDL ，TLA ，有限状态自动机 中图分类号：TP391 1．引言 [1] 在面向服务的计算（SOC ）中，服务已成为Web应用中的最主要的元素 。服务的广泛 应用因此也带来了很多问题和挑战，突出表现为服务的可组合性、同步性、协调性、正确性 验证等等[2] 。事实上，要以一种有效并且正确的方式处理这些问题，就需要形式化的方法来 表示服务的动态行为。 近年来，人们已经提出相当多的服务描述语言，从不同方面对服务进行建模和规范。在 工业标准中，WSDL[3]被用来描述单个Web服务的详细信息。WSDL定义了服务做什么，却 [4] 没有定义如何实现该服务。总之，WSDL建立的服务模型本质上是无状态的。就WSCI ， WSFL[5]，XLANG[6]，BPEL4WS[7]而言，它们都是协作和协调语言，旨在规范多个服务组合 时的协调问题以及协调中所需的逻辑状态。尽管这些语言从某方面处理了服务行为的表示问 题，但仍缺乏一个清晰的语义，也不适用于形式化规范和验证。 [8]正是一种基于模型检验的逻辑，它将时 动作时序逻辑TLA （Temporal Logic of action ） 序逻辑与传统逻辑结合起来，能够很好的描述并发系统的行为，对实时系统也有着较强的描 述能力和推理能力。由于TLA描述的Web服务都可用一个TLA公式表示，从而模型性质的验 证范围较其他形式化方法更为广泛，只要能写成TLA公式的性质都可以用TLA 的模型检验器 TLC进行验证。因此我们认为使用TLA进行描述并验证Web服务具有一定优势。 本文的主要工作是：（1）基于有限状态自动机理论，将对WSDL 进行扩展，从概念上 表示服务的行为；（2 ）引入动作时序逻辑 TLA 来形式化描述和规范服务行为，并用 TLC 对其进行验证。本文内容安排结构如下：第 2 节介绍 TLA 的基本概念；第 3 节对 WSDL 结 构进行扩展；第 4 节用 FSA 对服务进行建模；第 5 节实现 FSA 模型到 WSDL 扩展部分的转 换；第 6 节用 TLA 对 Web 服务进行描述；第 7 节对文章进行总结与展望。 2．TLA 介绍 TLA用于描述和推理并发系统，结合了标准时序逻辑和动作逻辑的特点。虽然TLA 的语 [8] 法和形式化语义很简单，它的表达能力在原理验证和实际应用上却非常强大 。 本课题得到国家自然科学基金资助（电子市场匹配模型与算法研究，批准号Web 服务组合模型 与算法，批准号）。 - 1 - TLA 的语义解释是基于“行为(behavior)”、“状态