摘 要： Web 服务组合研究领域的一个重要的问题是如何形式化描述Web 服务组合,如何验证服务组合的正确性。Web 服务组合的形式化模型可以用来检查、验证Web 服务组合以保证组合的正确性。针对目前最主要的一种语义Web 服务组合的规范WEB本体论语言（Ontology Web Langage-Semantic,简称OWL-S）,给出基于Pi演算的形式化描述，定义了Pi演算和OWl-S之间的概念映射,并给出了OWl-S的基于Pi演算的形式化模型,最后通过一个案例给出了模型验证的方法。
关键词：Web 服务;Web 服务组合;WEB本体论语言;Pi演算
引言
WOL-S( Ontology Web Langage-Semantic)是一个基于语义Web 服务的重要规范，是语义网活动的一个组成部分，可以用来描述Web文档和应用中内在的类和关系。通过增加相关资源的信息，使网络资源能够更容易地被自动进程访问，由于语义网络固有的分布性，OWL-S必须允许信息能够从分布的信息源收集起来。其中，允许本体间相互联系，包括明确导入其他本体的信息，使信息收集自动化。
从技术上讲WOL-S缺乏一个形式化的模型来对组合的Web 服务进行模型检查和验证。因此,本文提出了一个基于Pi演算的WOL-S的形式化模型,本文还通过一个案例给出了模型验证方法。本文包括以下内容:第1节介绍了WOL-S的基本语法;第2节定义了Pi演算到WOL-S的概念映射,给出了基于Pi演算的WOL-S的形式化描述;第3 节对Web 服务组合模型进行验证;最后给出全文总结和未来的工作。
1、WOL-S的基本语法
1.1 OWL-S主要元素
一个OWL本体中的大部分元素是与类（class）、属性（property）、类的实例（instance）以及这些实例间的关系有关的。使用本体是为了用它进行关于个体的推理。因此需要一种机制来描述个体所属的类以及这些个体通过类成员关系而继承得到的属性及基于类的推理。
1.2 OWL-S的主要性质
1.2.1 属性特性
（1）传递属性
如果一个属性P被声明为传递属性，那么对于任意的x,y和z：P(x,y) 与 P(y,z) 蕴含 P(x,z)
（2）对称属性
如果一个属性P被声明为对称属性，那么对于任意的x和y：P(x,y)当且仅当P(y,x)
（3）函数型属性
如果一个属性P被标记为函数型属性，那么对于所有的x, y, 和z: P(x,y) 与P(x,z) 蕴含 y = z
（4） 逆
如果一个属性P1被标记为属性P2的逆, 那么对于所有的x 和 y: P1(x,y) 当且仅当P2(y,x)
（5）反函数型
如果一个属性P被标记为反函数型的，那么对于所有的x, y 和 z: P(y,x) 与 P(z,x) 蕴含 y = z
（6）属性限制
allValuesFrom与 someValuesFrom，是局部的，它们仅仅在包含它们的类的定义中起作用。
（7）基数限制
使用owl:cardinality，这一约束允许对一个关系中的元素数目作出精确的限制
hasValue 能够根据“特定的”属性值的存在来标识类。因此，一个个体只要至少有“一个”属性值等于hasValue的资源，这一个体就是该类的成员。
1.2.2 本体映射
（1）等价类，等价属性
当我们要把一些本体组合在一起作为另一个新的本体的一部分时，能说明在一个本体中的某个类或者属性与另一个本体中的某个类或者属性是等价的.
（2）个体间的同一性
描述个体之间相同的机制与描述类之间的相同的机制类似.
（3）不同的个体
这一机制提供了与等价相反的效果。
（4）复杂类
集合运算符：交、并、补，枚举类，不相交类 。
1.3 葡萄酒主体的描述
某人正在筹划一个晚宴，希望能够使用与菜单上的菜肴最合适的酒来招待客人。也希望自己能够对晚宴的用酒显得学识渊博。并且，决定主菜为番茄做成的意大利面条酱和新鲜的意大利面条。
为了能够提供与餐宴合适的葡萄酒，主人需要葡萄酒和食物搭配方面的知识。为了显得对葡萄酒有相当的了解，主人需要获得关于宴会用酒的有关信息。为了配上合适的附属品，主人还需要有关在该情况下（以及在主人认可价格范围内）的附属品的信息。
通过一个相关背景的葡萄酒本体，根据对餐宴的一定的描述，葡萄酒主体能够给出适合该餐宴的酒的类型的建议。葡萄酒主体可能会建议使用馨芳葡萄酒（Zinfandel）作为这次宴会的用酒类型。除此之外，通过相关背景的本体，葡萄酒主体可以给出建议使用某种特定的馨芳葡萄酒，葡萄酒主体可能会去某个地点进行搜寻，它可能得到的是一系列的馨芳葡萄酒，也可能得到某种特定的馨芳葡萄酒
根据不同领域的背景本体知识和不同的信息以及不同的服务站点，葡萄酒主体可能应用到不同复杂程度的情况中去。在本例中，我们仅仅考虑了关于酒、品种类型、食物和酒的组合、某些酒的附属品和它们相关属性的一些信息。当然，我们能够根据顾客要求将本例扩展以包含更多的信息和更多的约束。
OWL_S的葡萄酒主体的服务描述：
即使相对简单的服务也可能包含复杂的交互,我们以一个本体论例子葡萄酒服务为例具体说明这些问题.因为重点是讨论如何建模Web 服务及其组合,所以我们的葡萄酒服务适当作了一些简化,省略了部分细节问题.
饮食与酒搭配服务Match接受客户Client的请求,根据客户提出的约束条件搜索到数据Data,初步满足客户的请求. 当客户再次提出约束条件后，再次根据约束条件搜索到满足客户的请求数据返回给客户。
其中各消息表示如下(为了简化后面的表示,在此给每个消息都定义一个缩写) :
Request :客户的搭配请求(Req) ;
AskInfo :搭配服务详细询问客户的需求(Ask) ;
ProvInfo :客户将客户的具体需求返回给搭配服务, 如餐食、价位、酒的品种等信息( Pro) ;
WineInfo :搭配服务返回相关酒数据( Wine) ;
GetWineInfo :搭配服务向酒数据服务请求当前可获得的酒数据( Get) ;
WineInfo :酒数据服务返回相关酒数据(Wine) ;
2、基于Pi演算的OWL-S 的形式化描述及建模
本文中采用基于OWL_S描述Web服务组合的方法,讨论它如何与Pi演算对应和结合起来。
OWL_S与Pi演算的对应关系：
（1）OWL_S规范中定义的一个类(Class) 和一个Pi演算进程相对应。
（2）OWL_S规范中定义的一个个体(Individual) 和一个Pi演算进程相对应。
（3）OWL_S中的定义的变量(variables) 可以被映射为Pi演算进程间通信所交换的信息。
（4）子类subClassOf，属性Property描述了本体与个体互相交互的Web 服务的访问点,它们和Pi 演算进程通信使用的通道相对应。
（5） OWL_S中的属性特性对应Pi演算的通
道的性质。例如：属性传递特性对应通道的传递特性，属性的对称性对应通道的对称性，属性的函数型属性对应通道的函数型特性，其它特性都可以对应到Pi演算的通道的性质。
（6） OWL_S中的类或个体经过属性赋变值变为另外的类或个体对应Pi演算中进程经过通道发出或接受信息到另外的进程。
在此给出寻找代理和通道的三条规则.
规则1. 逻辑上单独的原子服务作为一个代理,也就是说Web 服务组合中的每个子Web 服务作为一个代理出现;当需要对某个复杂的单一服务进行内部逻辑验证和流程分析时, 也可将其分割为几个相对独立的代理.
规则2. 当消息在两个代理间以一定顺序出现时(非并行) ,它们将在某一通道上进行传递;
规则3. 需要通信的两个代理间至少存在一条通道.
设x为客户Client与搭配服务Match之间的通道, y 为搭配服务Match与数据服务Data之间的通道.对系统进行建模如下(为了清楚地表示沿通道收到与发出消息,收到的消息均增加圆括号，发出的消息均增加了尖括号〈〉) :
设客户服务
。
类似地,搭配服务、数据服务分别建模如下:
搭配服务.
数据服务.
。
于是葡萄酒主体可建模如下：
3、Web 服务组合模型的验证
对Web 服务形式化建模是为了验证服务的正确性。Mobility Workbench(MWB) 是一个用来分析基于Pi演算描述的并发系统的工具 http://y/mwb.
