语义Web服务组合的语义一致性验证方法

技术领域

本发明属于语义网及Web服务领域，旨在为人们提供一种语义一致性验证方法，能够利用着色Petri网的形式化验证方法对语义Web服务组合的语义一致性进行验证。

背景技术

在面向服务的体系架构(Service-Oriented Architecture，SOA)下，Web服务组合已经成为支撑业务流程执行的主要形式。然而如何实现Web服务的自动组合一直是一个研究难题，因为Web服务不包含机器可读的语义信息。语义Web的出现将语义和Web服务结合起来，吸引了很多研究者的注意，Web服务本体描述语言(Web Ontology Language for Services，OWL-S)已经成为事实上的标准语义Web服务本体建模语言。

OWL-S对Web服务及流程建模，使得Web服务包含机器可读的语义信息，因而可以实现Web服务的自动组合、发现和调用。但是同Web服务组合一样，语义Web服务组合的过程中会存在服务不相容、非功能属性不一致等问题，因此就需要进行语义一致性验证。

为了验证语义Web服务组合的语义一致性，本发明利用Petri网技术，通过将语义Web服务组合模型转换为Petri网模型，从而进行服务组合的语义一致性验证。

下面对Petri网技术作一简单介绍：

Petri网是1960年由卡尔·A·佩特里发明的，是用于描述分布式系统的一种模型。它既能描述系统的结构，又能模拟系统的运行。描述系统结构的部分称为网(net)。从形式上看，一个网就是一个没有孤立结点的有向二分图。

Petri网包括这样几种组成元素(参见图3)：

1.库所(Place)：用一个圆形节点来表示

2.变迁(Transition)：用一个方形节点来表示

3.有向弧(Connection)：是库所和变迁之间的带有方向的弧

4.令牌(Token)：用一个黑点来表示，是库所中的动态对象，可以从一个库所移动到另一个库所。

一个变迁之前的库所称为输入库所，之后的库所称为输出库所。

Petri网的规则是：

1.有向弧是有方向的

2.两个库所或变迁之间不允许有弧

3.库所可以拥有任意数量的令牌

4.如果一个变迁的每个输入库所都拥有令牌，该变迁即为被允许。当变迁被允许时才能被触发(执行)，此时输入库所的令牌将被消耗(即减少)，输出库所将产生令牌(即增加)。

Petri网可以用于描述流程中状态的变化，各个库所表示不同的状态，例如论文的状态(撰写、提交、初审、复审、通过等)，某人的职位变化(实习生、职员、组长、经理等)，四季的不同(春夏秋冬)，或地理位置的不同(西直门、天安门、王府井等)；通过变迁连接不同的库所，变迁可以表示事件、转化或传输；而令牌的位置(即它所在的库所)则表示当前所处的状态；当令牌从一个库所经过变迁跳到另一个库所时，则表示状态发生了变化。例如，图4表示一个四季更替的过程。

Petri网的应用非常广泛，主要包括：软件设计、工作流管理、数据分析、并行程序设计、协议验证等。

由于Petri网不仅可以刻画系统的结构，而且可以描述系统的动态行为；不仅具有直观的图形表示，而且能够引入许多数学方法对其性质进行分析，因而将OWL-S建模的Web流程转化成Petri网模型，就可以利用现有的大量Petri网研究的成果对语义Web服务组合进行验证。相关的研究工作主要有：SriniNarayanan等人提出了DAML+OIL本体描述Web服务的组合方法，并自动将其转换为Petri网从而进行各种性能分析(Narayanan S，M.S.，″Simulation，verification and automated composition of Web services″.In Proc.of the 11th Int’lWorld Wide Web Conf.WWW2002.Honolulu：ACM.2002.)，A.Brogi等人给出了OWL-S到Petri网模型的转换方法(Brogi，A.，S.Corfini，and S.Iardella，″FromOWL-S descriptions to Petri nets″.In WESOA07.2007.Vienna.)，但是他们都没有对服务质量等非功能属性进行验证分析。

着色Petri网(Coloured Petri Nets，简称CPN)是经典Petri网的一个衍生和扩展。它通过对令牌着色丰富了Petri网表达的内涵。不同颜色的令牌代表不同属性的对象，例如红色令牌表示28岁的张三，蓝色令牌表示25岁的李四，绿色令牌表示30岁的王五。令牌的颜色由构建者来定义，库所和变迁的设置与经典Petri网相同，都表示状态变化。

因为着色Petri网(参见Jensen，K.，Coloured Petri Nets：Basic Concepts，Analysis Methods，and Practical Use.1997：Springer.)结合了Petri网和高级语言的优点，在对复杂系统建模时，可以使得模型更加简单、清晰，因此本发明使用着色Petri网来验证语义Web服务组合的语义一致性，包括参数和服务质量(Quality of Service，QoS)的一致性。

发明内容

针对现有技术中存在的问题，本发明的目的是提出一种基于着色Petri网的语义Web服务组合的语义一致性验证方法，能够利用Petri网的形式化验证技术对语义Web服务组合的参数语义一致性和QoS属性一致性进行验证。

下面首先给出着色Petri网的定义。

定义1着色Petri网CP-Net是一个六元组CPN＝(∑，P，T，F，C，E)，其中：

∑是颜色集合，表示令牌的不同颜色，令牌是指库所中的动态对象，令牌的位置是指该令牌所在库所当前的状态；

P是库所的集合，表示Petri网模型中所有的库所，库所表示不同的状态；

T是变迁的集合，表示Petri网模型中所有的变迁，变迁表示事件、转化或传输，通过变迁连接不同的库所；

F是有向弧集，表示Petri网模型中所有的有向弧，每条有向弧连接一个库所和变迁；

C是颜色函数，令牌的颜色表示不同属性的对象，它将库所和其中令牌的颜色对应起来，C:P→∑；

E是弧函数，E(p_j，t_i)表示从库所j到变迁i的弧函数，把每一条弧映射到一个颜色集合，用于表示要触发该条弧所需的令牌颜色及个数，其中：1≤i≤m，1≤j≤n。

下面定义输入输出矩阵与关联矩阵：

定义2着色Petri网CPN的网结构可以用一个n行m列矩阵

A＝[a_ij]_n×m来表示，称A为CPN的关联矩阵，它描述了该着色Petri网中各条有向弧的分布。其中m表示库所的个数，n表示变迁的个数，

即当存在从变迁t_i到库所p_j的有向弧时，a_ij⁺等于1，否则a_ij⁺等于0；

即当存在从库所p_j到变迁t_i的有向弧时，a_ij^-等于1，否则a_ij^-等于0；

即所有a_ij⁺组成的n行m列矩阵，称A⁺为输出矩阵；

即所有a_ij^-组成的n行m列矩阵，称A^-为输入矩阵；

i∈{1，2，…，n}，j∈{1，2，…，m}

将语义Web服务转换为着色Petri网，需要对现有的着色Petri网加以扩展，扩展后的着色Petri网定义为语义Web服务着色Petri网，如下：

定义3语义Web服务着色Petri网(Semantic Web Services Net，SWS-net)是一个八元组SWS-net＝(CPN，DT，DV，P_in，P_out，H_in，H_out，R)，其中：

CPN是定义1中定义的着色Petri网；

DT是数据类型定义的集合；

DV是变量定义的集合；

P_in是所有的输入库所的集合，输入库所是指到达变迁的库所；

P_out是所有的输出库所的集合，输出库所是指变迁到达的库所；

H_in是令牌从库所到达变迁所需的时间；

H_out是令牌从变迁到达库所所需的时间；

R是变迁发生其本身所需消耗的成本，即该变迁所对应的服务操作在执行时所需的费用，是一个已知量。

语义Web服务着色Petri网SWS-net的表示参见图5。

一般来说，Web服务组合的语义一致性包括参数一致性、功能和非功能属性(服务质量，Quality of Service，QoS)上的一致性。本发明主要给出参数一致性和非功能属性一致性的验证方法。

参数一致性是指组合的Web服务在参数上保持一致，它又包括：

●每个服务操作所用参数类型应该包含在系统定义的参数类型中。库所的令牌类型要包含在颜色集中。

●用户提供的输入参数类型应该能够满足服务操作发生所需的输入参数类型。输入弧函数的令牌类型集应是输入库所中令牌类型集的子集。

●用户提供的输入参数个数能够满足服务操作发生所需的输入参数个数。输入变迁输入弧函数的令牌数要小于等于输入库所中预含的令牌数。

●前驱输出弧函数和后继输入弧函数的令牌数目匹配，令牌类型匹配。

服务功能一致性是指所选服务在功能上与用户需求是否匹配。

服务的非功能属性一致性是指所选服务在非功能属性上与用户需求是否匹配，例如时间、成本、有效性等，非功能属性又称服务质量，其一致性验证具体包括：

●每个服务操作运行产生的参数个数要在系统的缓冲容量之内。它对应于变迁输出弧函数的令牌数要小于等于输出库所的上界。

●时间和费用上的约束。由于每个服务操作的运行需要一定时间，并要付出一定的使用费用，用户可以对于组合服务的运行时间提出能够容忍的最大上限，也可以提出使用该组合服务必须承担的最高费用。可以通过在Petri网的有向弧和变迁上添加权值表示每个操作运行的时延和所需费用，然后求出组合服务的运行时间和所需费用，并与用户约束进行比较。

下面定义一些基本变量，A^-和A⁺是Petri网的输入矩阵和输出矩阵(参见定义2)；i表示变迁数量，1≤i≤n；j表示库所数量，1≤j≤m；t_i和p_j分别表示一个变迁和库所；表示有一条从p_j到t_i的有向弧，反之，表示没有从p_j到t_i的有向弧；类似的，或0表示是否有从t_i到p_j的有向弧；E(p_j，t_i)表示从p_j到t_i的有向弧。

此外，为了检测服务的服务质量(QoS)，定义S_in为输入有向弧上时间标识函数值的总和，S_out为输出有向弧上时间标识函数值的总和，通过对组合服务所有参数输入和输出时延的加和来计算；S_R为所有服务操作消耗成本的总和。

本发明的特征在于，提出了一种基于着色Petri网的语义Web服务组合语义一致性验证方法。将语义Web服务组合转换为语义Web服务着色Petri网SWS-net后，通过本发明提出的语义一致性验证方法能够验证模型的参数语义一致性和QoS属性一致性，从而使用户能够根据分析结果调整Web服务组合，保证模型的语义一致性，满足用户对服务质量方面的要求。

附图说明

图1是一个描述了语义Web服务组合语义一致性验证系统的详细结构图；

图2是一个描述了语义Web服务组合语义一致性验证方法的具体步骤的图；

图3是一个描述了Petri网模型的组成元素的示例图；

图4是一个用Petri网模型表示四季更替的过程的示例图；

图5是一个描述了语义Web服务着色Petri网模型的组成元素的示例图；

图6是一个描述了语义Web服务着色Petri网的参数语义一致性验证算法流程图；

图7是一个描述了语义Web服务着色Petri网的QoS属性一致性验证算法流程图。

具体实施方式

所述方法是依次按以下步骤实现的：

步骤(1)，初始化

构建待验证的语义Web服务着色Petri网模型的存储单元，所述模型是一个八元组，表示为SWS-net，

SWS-net＝(CPN，DT，DV，P_in，P_out，H_in，H_out，R)，

CPN定义为着色Petri网，表示为CPN，是一个用于描述流程中状态变化的六元组，CPN＝(∑，P，T，F，C，E)，其中：

∑是颜色集合，表示令牌的不同颜色，令牌是指库所中的动态对象，令牌的位置是指该令牌所在库所当前的状态，

P是库所的集合，表示Petri网模型中所有的库所，库所表示不同的状态，

T是变迁的集合，表示Petri网模型中所有的变迁，变迁表示事件、转化或传输，通过变迁连接不同的库所，

F是有向弧集，表示Petri网模型中所有的有向弧，每条有向弧连接一个库所和变迁，

C是颜色函数，令牌的颜色表示不同属性的对象，

E是弧函数，E(p_j，t_i)表示从库所j到变迁i的弧函数，把每一条弧映射到一个颜色集合，用于表示要触发该条弧所需的令牌颜色及个数，其中：1≤i≤n，1≤j≤m，

DT是数据类型定义的集合，

DV是变量定义的集合，

P_in是所有的输入库所的集合，输入库所是指到达变迁的库所，

P_out是所有的输出库所的集合，输出库所是指变迁到达的库所，

H_in是令牌从库所到达变迁所需的时间，

H_out是令牌从变迁到达库所所需的时间，

R是变迁发生其本身所需消耗的成本，即该变迁所对应的服务操作在执行时所需的费用，是一个已知量，

在所述计算机中构建以下子模块单元，构成一个语义Web服务组合语义一致性验证模块，包括：参数语义一致性验证子模块、QoS属性一致性验证子模块，以及一致性分析结果存储子模块，其中：

参数语义一致性验证子模块，用于验证所述语义Web服务着色Petri网的模型的参数语义一致性，

QoS属性一致性验证子模块，用于验证所述语义Web服务着色Petri网的模型的QoS属性的一致性，

一致性分析结果存储子模块，用于存储参数语义一致性和QoS属性一致性的验证结果；

步骤(2)，按以下步骤验证语义Web服务着色Petri网模型的参数语义一致性：

步骤(2.1)，所述参数语义一致性验证子模块从所述语义Web服务着色Petri网存储单元中提取待验证的模型SWS-net，

步骤(2.2)，对变量j从1到m循环，判断库所j的数据类型是否错误，

若：表示库所p_j包含的令牌的颜色有不属于所述颜色集合∑的颜色，则库所p_j的数据类型错误，m为库所的数量，

若：则正确，

步骤(2.3)，对每一个从库所p_j指向变迁t_i的有向弧a_ij^-进行判断，以确认输入所述变迁t_i的弧函数数据类型是否错误，

若：且表示存在有向弧E(p_j，t_i)，且要触发该有向

弧所需的令牌的颜色集type(E(p_j，t_i))中有不属于C(p_j)的颜色，则所述库所p_j输入到所述变迁t_i的弧函数数据类型错误，

若：且则正确，

步骤(2.4)，对每个从变迁t_i指向库所p_j的有向弧a_ij⁺进行判断，以确认输出到所述库所p_j的弧函数数据类型是否错误，

若：且表示存在有向弧E(t_i，P_j)，且要触发该有向弧所需的令牌的颜色集type(E(t_i，P_j))中有不属于所述库所p_j包含的令牌的颜色集C(p_j)的颜色，则判定所述变迁t_i输出的输出弧函数数据类型错误，

若：且则正确，

步骤(2.5)，对所述每个有向弧a_ij⁺进行判断，以确认前驱服务操作的输出数据类型与后继服务操作所需的输入数据类型是否匹配，

若：且表示存在有向弧E(t_i，P_j)，且要触发该有向弧所需的令牌的颜色集type(E(t_i，P_j))不包含其下一条有向弧所需的令牌颜色集type(Nex(E(t_i，p_j)))，则确认前驱服务操作的输出数据类型与后继服务操作所需的输入数据类型不匹配，

若：且则正确，

步骤(2.6)，对所述每个有向弧a_ij⁺进行判断，以确认前驱服务操作的输出参数个数与后继服务操作的输入参数个数是否匹配，

若：且|E(t_i，p_j)|＜|Nex(E(t_i，p_j))|，表示具有从变迁t_i到库所p_j的有向弧E(t_i，P_j)，但对应于服务操作参数个数的弧函数E(t_i，P_j)的参数个数小于其下一个弧函数的参数个数Nex(E(t_i，p_j))|，则确认前驱服务操作的输出参数个数与后继服务操作的输入参数个数不匹配，

若：且|E(t_i，p_j)|≥Nex(E(t_i，p_j))|，则输出参数语义一致；

步骤(3)，按以下步骤验证语义Web服务着色Petri网模型的QoS属性一致性：

步骤(3.1)，所述QoS属性一致性验证子模块从所述语义Web服务着色Petri网存储单元中提取待验证的模型SWS-net，

步骤(3.2)，初始化以下三个参数：

S_in，表示输入到变迁的输入有向弧上的时间标识函数值的总和，S_in0＝0，

S_out，表示从变迁输出的输出有向弧上的时间标识函数值的总和，S_out0＝0，

S_R，表示所有服务操作消耗成本的总和，成本表示执行此服务操作所需的费用，S_R0＝0，

步骤(3.3)，对每一条所述输入有向弧进行服务操作输出参数的个数是否溢出的判断，

若：|E(p_j，t_i)|＞M，表示对应于所述服务操作输出参数个数的弧函数E(p_j，t_i)的参数个数大于所述Petri网内任一库所允许拥有的最多令牌参数M，则确认溢出，

若：|E(p_j，t_i)|≤M，则表示输出参数的个数不溢出；

步骤(3.4)，从任意选定的起始库所开始，遍历所有从库所到达变迁的输入有向弧，按下式计算所有令牌沿着各自的输入有向弧从库所p_j到达变迁t_i所需要消耗的时间，即输入时间标识函数值的总和，1≤i≤n，1≤j≤m，m为库所数量，n为变迁数量：

S_in后＝S_in前+H_in(E(p_j，t_i))，其中：

S_in前，表示此前所有j-1个库所的令牌沿着各自的输入有向弧到达对应的i-1个变迁所消耗的时间，用输入时间函数值的总和表示，

S_in后，表示所有各库所p_j的令牌沿着各自的输入有向弧到达变迁所需要的输入时间标识函数值的总和，

H_in(E(p_j，t_i))，表示在“S_in后-S_in前”这一段时间内，所有令牌从各自选择的库所p_j沿着输入有向弧到达变迁t_i的输入时间标识函数值，

步骤(3.5)，从对应于步骤(3.4)中所述的起始库所所需到达的变迁开始，遍历所有的变迁沿着输出有向弧到达所对应的库所，按下式计算所有令牌沿着各自的输出有向弧从变迁t_i到达库所p_j所需的输出时间标识函数值的总和，1≤i≤n，1≤j≤m，m为库所数量，n为变迁数量，

S_out后＝S_out前+H_out(E(t_i，p_j))，其中：

So_ut前，表示此前所有i-1个变迁的令牌沿着各自的输出有向弧到达对应的j-1个库所的输出时间标识函数值，

S_out后，表示所有各变迁t_i的令牌沿着各自的输出有向弧到达对应各库所p_j所需的时间标识函数值的总和，

H_out(E(t_i，p_j))，表示在“S_out后-S_out前”这一段时间内，所有令牌从各自现在的变迁t_i沿着输出有向弧到达对应的现在的库所p_j所需要的时间标识函数值，

步骤(3.6)，若：输入有向弧上消耗的时间S_in后加上输出有向弧上消耗的时间S_out后的值，大于用户对组合服务执行时间给定的最大阈值Q，则确认不满足时间约束，否则，确认满足，

步骤(3.7)，从对应于步骤(3.4)中所述的起始库所所需到达的变迁开始，遍历所有的变迁，按下式计算所有变迁其自身所需消耗的成本的总和，1≤i≤n，

S_R后＝S_R前+R(t_i)，其中：

S_R前，表示此前所有i-1个变迁所消耗的成本的总和，

S_R后，表示从初始变迁一直到变迁t_i所消耗的成本的总和，

R(t_i)，表示变迁t_i发生时其自身所需要消耗的成本，即对应的服务操作在执行中所需的费用，

步骤(3.8)，若：所有变迁消耗成本之和S_R后大于用户对组合服务消耗成本给定的最大阈值W，则确认不满足成本约束，否则，确认满足，并说明该Petri网模型的非功能属性一致；

步骤(4)，将一致性分析结果存储子模块中存储的分析结果反馈给用户，若结果显示该模型的参数语义一致以及非功能(QoS)属性一致，则用户可直接使用该模型对服务进行组合并执行；若结果显示该模型有错误或者不匹配或者不满足约束，则用户需要对服务组合进行调整，并重新进行语义一致性验证(即执行步骤(2)和步骤(3))。

为了实现上述目的，本发明所采用的技术方案如下：

1.建立语义Web服务组合语义一致性验证系统的运行环境，参阅图1，该系统的主要构件及建立过程如下：

(1)在计算机上安装操作系统。操作系统可选用微软公司的视窗(Windows)系列操作系统中的Windows 2000及以上版本；

(2)在计算机上构建语义Web服务着色Petri网存储单元，用于存储语义Web服务着色Petri网。所述语义Web服务着色Petri网通过语义Web服务组合转换而来，在着色Petri网的基础上加以扩展，其转换方法可参照文献(Brogi，A.，S.Corfini，and S.Iardella，″From OWL-S descriptions to Petri nets″.In WESOA07.2007.Vienna.)和(Vidal，J.C.，M.Lama，and A.Bugar′m，Petri Net Semantics forOWL-S Service Choreography.2007.)；

(3)在计算机上安装语义Web服务组合语义一致性验证系统，该系统主要包含如下三个部分：

(3.1)参数语义一致性验证子模块：用于验证所述“语义Web服务着色Petri网”模型的参数语义一致性。

(3.2)QoS属性一致性验证子模块：用于验证证所述“语义Web服务着色Petri网”模型的QoS属性的一致性。

(3.3)一致性分析结果存储子模块：用于存储参数语义一致性及QoS属性一致性验证的分析结果。

2.一种语义Web服务着色Petri网模型的参数语义一致性验证方法，该方法采用的具体方案参阅图6，包括如下的步骤：

步骤1，用参数语义一致性验证子模块从语义Web服务着色Petri网存储子模块中提取待验证的模型SWS-net；

步骤2，对变量j从1到m循环，判断库所j的数据类型是否错误，

若：表示库所p_j包含的令牌的颜色有不属于所述颜色集合∑的颜色，则库所p_j的数据类型错误，m为库所的数量，

若：则正确；

步骤3，对每一个从库所p_j指向变迁t_i的有向弧a_ij^-进行判断，以确认输入所述变迁t_i的弧函数数据类型是否错误，

若：且表示存在有向弧E(p_j，t_i)，且要触发该有向弧所需的令牌的颜色集type(E(p_j，t_i))中有不属于C(p_j)的颜色，则所述库所p_j输入到所述变迁t_i的弧函数数据类型错误，

若：且则正确；

步骤4，对每个从变迁t_i指向库所p_j的有向弧a_ij⁺进行判断，以确认输出到所述库所p_j的弧函数数据类型是否错误，

若：且表示存在有向弧E(t_i，P_j)，且要触发该有向弧所需的令牌的颜色集type(E(t_i，P_j))中有不属于所述库所p_j包含的令牌的颜色集C(p_j)的颜色，则判定所述变迁t_i输出的输出弧函数数据类型错误，

若：且则正确；

步骤5，对所述每个有向弧a_ij⁺进行判断，以确认前驱服务操作的输出数据类型与后继服务操作所需的输入数据类型是否匹配，

若：且表示存在有向弧E(t_i，P_j)，且要触发该有向弧所需的令牌的颜色集type(E(t_i，P_j))不包含其下一条有向弧所需的令牌颜色集type(Nex(E(t_i，p_j)))，则确认前驱服务操作的输出数据类型与后继服务操作所需的输入数据类型不匹配，

若：且则正确；

步骤6，对所述每个有向弧a_ij⁺进行判断，以确认前驱服务操作的输出参数个数与后继服务操作的输入参数个数是否匹配，

若：且|E(t_i，p_j)|＜Nex(E(t_i，p_j))|，表示具有从变迁t_i到库所p_j的有向弧E(t_i，P_j)，但对应于服务操作参数个数的弧函数E(t_i，P_j)的参数个数小于其下一个弧函数的参数个数|Nex(E(t_i，p_j))|，则确认前驱服务操作的输出参数个数与后继服务操作的输入参数个数不匹配，

若：且|E(t_i，p_j)|≥|Nex(E(t_i，p_j))|，则输出参数语义一致。

3.按以下步骤验证语义Web服务着色Petri网模型的QoS属性一致性，参阅图7：

步骤1，所述QoS属性一致性验证子模块从所述语义Web服务着色Petri网存储单元中提取待验证的模型SWS-net；

步骤2，初始化以下三个参数：

S_in，表示输入到变迁的输入有向弧上的时间标识函数值的总和，S_in0＝0，

S_out，表示从变迁输出的输出有向弧上的时间标识函数值的总和，S_out0＝0，

S_R，表示所有服务操作消耗成本的总和，成本表示执行此服务操作所需的费用，S_R0＝0；

步骤3，对每一条所述输入有向弧进行服务操作输出参数的个数是否溢出的判断，

若：|E(p_j，t_i)|＞M，表示对应于所述服务操作输出参数个数的弧函数E(p_j，t_i)的参数个数大于所述Petri网内任一库所允许拥有的最多令牌参数M，则确认溢出，

若：|E(p_j，t_i)|≤M，则表示输出参数的个数不溢出；

步骤4，从任意选定的起始库所开始，遍历所有从库所到达变迁的输入有向弧，按下式计算所有令牌沿着各自的输入有向弧从库所p_j到达变迁t_i所需要消耗的时间，即输入时间标识函数值的总和，1≤i≤n，1≤j≤m，m为库所数量，n为变迁数量：

S_in后＝S_in前+H_in(E(p_j，t_i))，其中：

S_in前，表示此前所有j-1个库所的令牌沿着各自的输入有向弧到达对应的i-1个变迁所消耗的时间，用输入时间函数值的总和表示，

S_in后，表示所有各库所p_j的令牌沿着各自的输入有向弧到达变迁所需要的输入时间标识函数值的总和，

H_in(E(p_j，t_i))，表示在“S_in后-S_in前”这一段时间内，所有令牌从各自选择的库所p_j沿着输入有向弧到达变迁t_i的输入时间标识函数值；

步骤5，从对应于步骤4中所述的起始库所所需到达的变迁开始，遍历所有的变迁沿着输出有向弧到达所对应的库所，按下式计算所有令牌沿着各自的输出有向弧从变迁t_i到达库所p_j所需的输出时间标识函数值的总和，1≤i≤n，1≤j≤m，m为库所数量，n为变迁数量，

S_out后＝S_out前+H_out(E(t_i，p_j))，其中：

S_out前，表示此前所有i-1个变迁的令牌沿着各自的输出有向弧到达对应的j-1个库所的输出时间标识函数值，

S_out后，表示所有各变迁t_i的令牌沿着各自的输出有向弧到达对应各库所p_j所需的时间标识函数值的总和，

H_out(E(t_i，p_j))，表示在“S_out后-S_out前”这一段时间内，所有令牌从各自现在的变迁t_i沿着输出有向弧到达对应的现在的库所p_j所需要的时间标识函数值；

步骤6，若：输入有向弧上消耗的时间S_in后加上输出有向弧上消耗的时间S_out后的值，大于用户对组合服务执行时间给定的最大阈值Q，则确认不满足时间约束，否则，确认满足；

步骤7，从对应于步骤4中所述的起始库所所需到达的变迁开始，遍历所有的变迁，按下式计算所有变迁其自身所需消耗的成本的总和，1≤i≤n，

S_R后＝S_R前+R(t_i)，其中：

S_R前，表示此前所有i-1个变迁所消耗的成本的总和，

S_R后，表示从初始变迁一直到变迁t_i所消耗的成本的总和，

R(t_i)，表示变迁t_i发生时其自身所需要消耗的成本，即对应的服务操作在执行中所需的费用；

步骤8，若：所有变迁消耗成本之和S_R后大于用户对组合服务消耗成本给定的最大阈值W，则确认不满足成本约束，否则，确认满足，并说明该Petri网模型的非功能属性一致。

4.将一致性分析结果存储子模块中存储的分析结果反馈给用户，若结果显示该模型的参数语义一致以及非功能(QoS)属性一致，则用户可直接使用该模型对服务进行组合并执行；若结果显示该模型有错误或者不匹配或者不满足约束，则用户需要对服务组合进行调整，并重新进行语义一致性验证(即执行步骤2和步骤3)。

按照发明内容中的初始化设定中的步骤依次完成系统的部署和设定，根据发明内容中的语义一致性验证方法验证语义Web服务着色Petri网模型的参数语义一致性和QoS属性一致性。用户根据分析结果决定是否要对模型进行修改，从而保证服务组合能够满足用户的需求。