基于着色Petri网的语义Web服务组合形式化验证  

Formal verification for semantic Web services composition based on coloured Petri nets

作　　者：倪悦[1,2] 范玉顺[1] 

机构地区：[1]清华大学自动化系,北京100084 [2]桂林空军学院一系,桂林541003

出　　处：《清华大学学报（自然科学版）》2010年第5期714-717,723,共5页Journal of Tsinghua University(Science and Technology)

基　　金：国家自然科学基金资助项目(60674080;60704027);国家"八六三"高技术项目(2007AA04Z150);欧盟第六框架资助项目(FP6-033610)

摘　　要：为了对语义Web服务组合进行形式化验证,提出一种语义Web服务组合模型到着色Petri网组合模型的转换方法,定义了语义Web服务着色Petri网(SWS-net)。转换后的模型不仅能清晰表示服务组合中各子过程之间的逻辑关系,而且能用着色Petri网的形式化方法进行服务组合正确性验证。给出了组合服务的语义一致性验证算法,最后以一个协同设计过程为例对组合服务流程进行仿真验证并在工作流引擎中部署执行。仿真及执行结果表明,服务组合后的流程无死锁并且能够顺利执行。This paper presents a composition model for colored Petri nets transformed from Web ontology language for services to validate semantic Web services composition,and defines semantic Web services net（SWS-net）.The model can explicitly express the logical relations among sub-processes of services composition and verify the correctness of services composition using formalized methods of coloured Petri nets,with the verification algorithm then proposed for the semantic consistency of composed services.A cooperative design process was taken as an example to simulate and execute the model.The results show that the composed services do not contain any deadlocks and are smoothly executed in the workflow engine.

关 键 词：语义WEB服务 服务组合 着色PETRI网 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]