OWL-S过程模型的形式化描述与相容性分析

J4 ›› 2016, Vol. 38 ›› Issue (03): 478-485.

OWL-S过程模型的形式化描述与相容性分析

唐郑熠1,3,王金水1,韦立2,3,薛醒思1,胡文瑜1

（1.福建工程学院信息科学与工程学院，福建福州 350118；
2.贵州师范大学数学与计算机科学学院，贵州贵阳 550001；3.贵州大计算机科学与技术学院，贵州贵阳 550025）

收稿日期:2015-03-20 修回日期:2015-07-22 出版日期:2016-03-25 发布日期:2016-03-25
基金资助:
国家自然科学基金(61309006);福建省自然科学基金(2012J01245);福建省中青年教师教育科研基金(JB14069);福建工程学院科研启动基金(GYZ13112,GYZ13113)

Formal description and compatibility
analysis of OWLS process model

TANG Zhengyi1,3,WANG Jinshui1,WEI Li2,3,XUE Xingsi1,HU Wenyu1

(1.School of Information Science and Engineering,Fujian University of Technology,Fuzhou 350118;
2.School of Mathematics and Computer Science,Guizhou Normal University,Guiyang 550001;
3.School of Computer Science and Technology,Guizhou University,Guiyang 550025,China)

Received:2015-03-20 Revised:2015-07-22 Online:2016-03-25 Published:2016-03-25

摘要/Abstract

摘要：

构建组合服务的形式化模型是对其进行验证的前提与基础，然而缺乏统一的构建框架使得建模过程变得难以把握且无法实现自动化。通过对确定型有限自动机的扩展，建立了用于描述OWLS过程模型的有限迁移系统——服务过程自动机，为组合服务的形式化建模提供了统一框架和自动化基础。同时，通过分析服务过程自动机的可接受位置及其在组合过程中可能产生的约束，将相容性划分为三个等级，从而能够在不同强度的可靠性要求下进行组合服务的验证工作。

关键词: 服务组合验证, OWLS, 形式化模型, 服务过程自动机, 相容性分

Abstract:

Building the formal model of composite services is the basis of verification. But in the absence of a unified modeling framework, automatic operations of the modeling process are difficult to realize. We build a services process automata by expanding the deterministic finite automata. It is a finite migratory system which is suitable for describing the process model of OWLS. This work provides a unified framework and a foundation of automatic operations for the formal modeling of composite services. In addition, we divide the compatibility into three grades by analyzing the acceptable locations of the services process automata and the constraints possibly produced during the composition process. So the proposal can be adaptive to verification of composite services with different reliability requirements.

Key words: services composition verification;OWL-S;formal model;services process automata;compatibility analysis

唐郑熠1,3,王金水1,韦立2,3,薛醒思1,胡文瑜1. OWL-S过程模型的形式化描述与相容性分析[J]. J4, 2016, 38(03): 478-485.

TANG Zhengyi1,3,WANG Jinshui1,WEI Li2,3,XUE Xingsi1,HU Wenyu1. Formal description and compatibility
analysis of OWLS process model [J]. J4, 2016, 38(03): 478-485.

参考文献［6］

［1］	Ni Yue,Fan Yushun.Formal verification for semantic Web services composition based on coloured Petri nets［J］.Journal of Tsinghua University,2010,20(5):105112.
［2］	Hu Jing,Rao Guozheng,Feng Zhiyong.Polybasic Picalculus based description and verification for Web service［J］.Journal of Tianjin University(Science and Technology),2013,46(6):520525.(in Chinese)
［3］	Yuan Min,Huang Zhiqiu,Li Xiang,et al.Towards a formal verification approach for business process coordination［C］∥Proc of International Conference on Web Services,2010:1.
［4］	Shi Huijuan,Rong Mei,Zhang Guangquan,et al.Description and verification of asynchronous Web service composition based on XYZ/ADL［J］.Computer Science,2011,38(12):139143.(in Chinese)
［5］	Guermouche N,Godart C.Timed model checking based approach for Web services analysis［C］∥Proc of International Conference on Web Services,2009:1.
［6］	Zhang Guangquan,Rong Mei,Wang Sheng.Research on interaction modeling and mismatch checking of timeaware Web services［J］.Chinese Journal of Electronics,2011,39(11):25682575.(in Chinese)
［7］	Ji Shunhui,Li Bixin,Qiu Dong.Verification for the concurrent properties of evolving BPEL composite service［C］.IEEE International Conference on Software Engineering and Service Sciences,2014:1.
［8］	David M,Massimo P,Sheila M,et al.Bringing semantics to Web services:The OWLS approach［J］.Lecture Notes in Computer Science,2005,3387:2642.
［9］	Zhang Jiangwei,Zeng Yi,Hu Yanqiang,et al.An approach for service composition based on OWLS process model［C］∥IEEE Conference Anthology,2013:1.
［10］	Cristian M,Marco C,Alejandro Z,et al.Revising WSDL documents:Why and how［J］.IEEE Internet Computing,2013,17(5):4653.
	附中文参考文献:
［2］	胡静,饶国政,冯志勇.基于多元Pi演算的Web服务组合描述与验证［J］.天津大学学报(自然科学与工程技术版),2013,46(6):520525.
［4］	石慧娟,戎玫,张广泉,等.基于XYZ/ADL的异步Web服务组合描述与验证［J］.计算机科学,2011,38(12):139143.
［6］	张广泉,戎玫,王昇.时间感知Web服务交互行为建模与失配检测方法研究［J］.电子学报,2011,39(11):25682575.