语义Web服务组合的模型转换及形式化验证方法

摘要

语义Web服务组合的模型转换及形式化验证方法属于语义网及Web服务领域，其特征在于，在计算机上建立语义Web服务组合存储单元、模型转换子模块、语义Web服务着色Petri网存储子模块、正确性验证子模块和本体工具Protégé；该方法通过模型转换子模块将OWL-S形式的语义Web服务组合模型转换为语义Web服务着色Petri网模型，转换后的模型不仅能清晰表示服务组合中各子过程之间的逻辑关系，而且能够用着色Petri网的形式化方法进行服务组合的正确性验证。根据本发明，能够通过形式化方法验证语义Web服务组合的正确性，从而保证服务组合的正确执行。

主权项

1.语义Web服务组合的模型转换及形式化验证方法，其特征在于，所述方法是在计算机中依次按以下步骤实现的：步骤(1)，计算机初始化安装本体建模工具Protégé，用于建立、删除、修改本体，并把本体存储为网络Web服务本体建模语言OWL-S的格式，构建语义Web服务组合存储单元，用于存储由所述Web服务本体建模工具Protégé构造、用所述OWL-S格式表示的语义Web服务组合模型，安装语义Web服务组合模型转换与验证模块，包括：模型转换子模块、语义Web服务着色Petri网存储子模块以及正确性验证子模块，其中：模型转换子模块，用于把所述语义Web服务组合存储单元中存储的语义Web服务组合转换为着色Petri网模型，转换后的模型命名为“语义Web服务着色Petri网”，其中：着色Petri网简称CPN，是一个六元组的模型，所述CPN＝(∑，P，T，F，C，E)，其中：∑是颜色集合，表示令牌的不同颜色，P是库所的集合，表示所述着色Petri网模型中所有的库所，T是变迁的集合，表示所述着色Petri网模型中所有的变迁，F是有向弧集，表示所述着色Petri网模型中所有的有向弧，每条有向弧连接一个库所和变迁，C是颜色函数，把所述库所和库所中令牌的颜色对应起来，用C:P→∑表示，E是弧函数，把每一条有向弧映射到某一个颜色集合，所述某一个颜色集合表示要触发该有向弧所需的令牌颜色及个数，所述着色Petri网CPN可以由一个n行m列的矩阵A表示，称为该CPN的关联矩阵，A＝[a_ij]_n×m，m为库所的个数，1≤j≤m，n为变迁的个数，1≤i≤n，$a_{\mathrm{ij}}=a_{\mathrm{ij}}^{+}-a_{\mathrm{ij}}^{-},$，其中，当存在从变迁t_i到库所p_j的输出有向弧时，$a_{\mathrm{ij}}^{+}=1,$否则，$a_{\mathrm{ij}}^{+}=0,$当存在从库所p_j到变迁t_i的输入有向弧时，$a_{\mathrm{ij}}^{-}=1,$否则，$a_{\mathrm{ij}}^{-}=0,$语义Web服务着色Petri网SWS-net是一个八元组模型，SWS-net＝(CPN，DT，DV，P_in，P_out，H_in，H_out，R)，其中，CPN，是所述着色Petri网模型，DT，是数据类型定义的集合，DV，是变量定义的集合，P_in，是所有输入库所的集合，所述输入库所是经输入有向弧指向变迁的库所，P_out，是所有输出库所的集合，所述输出库所是从变迁通过输出有向弧所指向的库所，H_in，是令牌从库所到达变迁所需的时间，H_out，是令牌从变迁到达库所所需的时间，R是变迁发生其本身所需消耗的成本，即该变迁所对应的服务操作在执行时所需的费用，是一个已知量，语义Web服务着色Petri网存储子模块，用于存储所述语义Web服务着色Petri网模型，正确性验证子模块，用于验证转换得到的所述语义Web服务着色Petri网模型的正确性；步骤(2)，依次按以下步骤实现语义Web服务组合的模型转换以及形式化验证方法：步骤(2.1)，用所述模型转换子模块从所述语义Web服务组合存储单元中提取待转换的Web服务组合模型，步骤(2.2)，把所述语义Web服务组合模型OWL-S中的各个组成部分映射到着色Petri网中的组成元素，形成语义Web服务着色Petri网SWS-net，其步骤如下：步骤(2.2.1)，服务的所有消息参数类型对应所述颜色集合∑；步骤(2.2.2)，服务操作运行产生的效果对应变迁发生过程中令牌转移前后的状态；步骤(2.2.3)，存放服务参数的缓冲区对应库所；步骤(2.2.4)，服务的操作对应变迁；步骤(2.2.5)，服务中消息的传输方向对应有向弧集；步骤(2.2.6)，服务的输入、输出参数类型对应颜色函数；步骤(2.2.7)，在输入有向弧上添加时间标识函数值H_in，表示输入参数传输时延，在输出有向弧上添加时间标识函数值H_out，表示输出参数传输时延，当变迁所需参数全部到达时，瞬间完成变迁触发，H_in+H_out表示变迁从发生到完成所需的时延；步骤(2.2.8)，在变迁上添加成本函数R，表示用户使用该服务操作时其自身所需付出的费用；步骤(2.3)，把所述OWL-S中单个服务的一次交互过程，也称原子过程，与所述SWS-net中单个Web服务调用相对应，其转换规则如下：把原子过程映射为变迁t，t命名为原子过程的名称，前提条件映射为输入库所集P_in，结果映射为输出库所集P_out，输入映射为输入库所的初始令牌，步骤(2.4)，把所述OWL-S组合过程转换到SWS-net，用以表示复杂的业务逻辑，所述组合过程由原子服务或子组合过程组合而成，其转换规则如下：对于所述OWL-S中的顺序结构，转换为对应的着色Petri网结构，其中子过程按照顺序依次执行，对于所述OWL-S中的选择结构或者如果-那么结构，转换为对应的着色Petri网结构，其中选择结构表示在一组子过程中随机选择一个子过程执行，如果-那么结构表示在两个过程中选择一个执行，对于所述OWL-S中的任意顺序结构，转换为对应的着色Petri网结构，它表示一组子过程无序地执行，但不能并发执行，对于所述OWL-S中的重复-当结构，转换为对应的着色Petri网结构，首先检查循环条件，条件为真则执行子过程，否则退出循环，对于所述OWL-S中的重复-直到结构，转换为对应的着色Petri网结构，首先执行子过程，条件为假则重复执行子过程，直到条件为真退出循环继续执行后续子过程，对于所述OWL-S中的分支结构或者分支-汇合结构，转换为对应的着色Petri网结构，分支结构表示一组子过程并发执行，当所有子过程都并发执行时，控制结构执行完毕，分支-汇合结构表示一组子过程并发执行后，同步这些子过程，即所有子过程执行完才表示控制结构执行完成，步骤(2.5)，对步骤(2.4)得到的转换后的SWS-net，按以下步骤进行正确性验证：步骤(2.5.1)，把语义Web服务着色Petri网SWS-net输入到所述正确性验证子模块，步骤(2.5.2)，计算所述关联矩阵$A={\left[a_{\mathrm{ij}}^{+}\right]}_{n\times m}-{\left[a_{\mathrm{ij}}^{-}\right]}_{n\times m},$[a_ij⁺]_n×m为所有从变迁i到库所j的输出有向弧a_ij⁺组成的n行m列矩阵，称为输出矩阵，[a_ij^-]_n×m为所有从库所j到变迁i的输入有向弧a_ij^-组成的n行m列矩阵，称为输入矩阵，步骤(2.5.3)，设置各库所在初始状态下的令牌数序列M₀，M₀＝{P₁(0)，P₂(0)，…，P_m(0)}，步骤(2.5.4)，设置各库所在第K个状态时的令牌数序列M_K，K表示从初始状态到目标状态所经历的状态数，M_K＝{P₁(K)，P₂(K)，…，P_m(K)}，步骤(2.5.5)，令变量i＝1，Z＝0，步骤(2.5.6)，令$M_i=M_{i-1}+{\left(A_{i*}\right)}^T,$其中M_i-1表示第i-1个状态，表示关联矩阵A的第i个行向量，M_i表示第i个状态，计算得到M_i，它表示为一个m维行向量M_i＝{P₁(i)，P₂(i)，…，P_m(i)}，将该行向量中最大的数与变量Z比较，若该最大值大于Z则令Z等于该最大值，否则Z值不变，步骤(2.5.7)，若i大于等于K，将i的值加1，重复步骤(2.5.6)，若i小于K，继续进行下一步，K表示从初始状态到目标状态所经历的状态个数，步骤(2.5.8)，若Z等于1，表示该模型是安全的，否则进行下一步，所述该模型是安全的表示该模型的任一库所中最多可能出现的令牌数为1，即在状态变迁过程中每个库所最多可能出现一个令牌，因此该模型能够安全无溢出的执行完毕，步骤(2.5.9)，若Z大于1且小于正无穷，表示该模型的界为Z，否则表示该模型错误，所述该模型的界为Z表示模型的任一库所中最多可能出现Z个令牌，Z也称为状态边界，若Z是一个有限的正整数，则该模型也能够正确执行，若Z等于正无穷，说明令牌溢出，模型会出现死锁，若Z等于0，说明模型中从没有令牌，模型没有执行，若Z等于负数，说明系统错误，步骤(3)，把步骤(2)得到的分析结果反馈给用户，若结果显示该模型正确，即模型是安全的或有界的，则用户可直接使用该模型对服务进行组合并执行，若结果显示该模型不正确，则用户需要对模型修改(使用protégé)并再次执行步骤(2)。