一种验证Web服务流程的新方法  

Novel method to verify Web services process

作　　者：王晨[1] 王红兵[1] 许迅[1] 

机构地区：[1]东南大学计算机学院,南京210096

出　　处：《计算机应用研究》2008年第12期3785-3789,共5页Application Research of Computers

基　　金：国家自然科学基金资助项目(60673175)

摘　　要：在实际的服务组合中,Web服务流程(process)的验证(verification)对于Web服务的组合实现和应用具有重要意义——通过验证可以证明一个组合服务的控制流满足某个重要或者期望的属性,如不包含死锁或不包含无限循环,诸如此类;而服务提供者可对Web服务流程进行验证,以确保所提供的Web服务是完全正确的。然而,针对这两种语言的验证方法较少被人们注意。提出一种验证Web服务流程的方法,该方法使用时序行为逻辑(TLA)建模服务流程,然后,利用模型检验(model checking)技术验证模型的某些属性。实验证明该方法效果良好,有相当的探索与实用价值。OWL-S and BPEIAWS are two widely used services description language which applied in modeling and implementing service composition. In the real services composition, the verification of Web services process plays an important role. Through the verification, the paper proved that a control flow of the services composition could satisfy some important or expected properties, some key properties such as no deadlock, no infinite loop and so on; also the service provider may verify Web services process to ensure that the Web services which they provided were completely correct. However, little attention had been paid to the methods which verify these two description language. And proposed a verification method of Web services which used TLA to model the services process, and then used the technology, model checking to verify some key properties. Through experiments, proves that it has good effect and is a potential and useful method in real environment.

关 键 词：时序逻辑语言 Web服务本体描述语言 WEB服务业务流程执行语言 WEB服务组合验证 工作流模型分析 

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