基于ZING的Web服务建模与验证  

Modeling and verification for Web services based on ZING

作　　者：陆晶晶[1] 骆翔宇[2] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,广西桂林541004 [2]华侨大学计算机科学与技术学院,福建厦门361021

出　　处：《桂林电子科技大学学报》2011年第3期202-207,共6页Journal of Guilin University of Electronic Technology

基　　金：国家自然科学基金(60763004)

摘　　要：为了验证Web服务的正确性和可靠性等性质以及提高Web服务流程验证的自动化程度,提出了一种适合构造BPEL4WS(Web服务的业务流程执行语言)结构模型的输入输出标记迁移系统(I/OLTS)作为中间形式化模型,将BPEL转化为中间形式模型I/OLTS,然后再转化为软件模型检测工具ZING的输入语言的转化算法,并应用ZING对Web服务的正确性进行验证。通过该建模和转换算法,可有效提高Web服务流程验证的自动化程度,简化转化过程中复杂繁琐的人工编码操作。To verify the correctness and reliability of Web services and improve the automation in the process validation of Web services,the input/output labeled transition system（I/OLTS） as an intermediate formal model that was suitable to Business Process Execution Language for Web Services（BPEL4WS） structure model was proposed,and an algorithm was designed to transform BPEL into I/OLTS,which would be further transformed into the input language of the software model checking tool ZING,such that the correctness and reliability of Web services could be verified via ZING.The automation in the process validation of web services is improved by the modeling and the transformation algorithm,and a lot of tedious and complex manual operation in the transformation process is simplified.

关 键 词：WEB服务 BPEL4WS I/OLTS 软件模型检测 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]