《web服务组合的互模拟验证》

《《web服务组合的互模拟验证》》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第26卷第10期计算机应用Vol.26No.102006年10月ComputerApplicationsOct.2006文章编号:1001一9081(2006)10一2466一04Web服务组合的互模拟验证衰勇福，高春鸣，刘荣胜(湖南师范大学数学与计算机科学学院，长沙湖南410081)(jem_yuan@hotmail.com)摘要:为检验Web服务组合的实现与用户需求的一致性，在开互模拟形式化理论和检验工具的基础上，提出了一个自动化检验方法。首先，用二一演算分别对用户需求和商业流程可执行语言(BPEL4WS)程序实现建模，然后对它们进行弱

2、开互模拟检验，当它们不互模拟时，检验工具能自动标识关键的不互模拟的BPEL4WS程序片段。最后通过实例说明这一方法的可行性。关键词:二一演算;商业流程可执行语言;开互模拟;on-the-伪算法;模型验证中图分类号:TP18文献标识码:AOpen-bisimulationcheckingofWebServicescombinationYUANYong-fu,GAOChun-ming,LIURong-sheng(CollegeofMathematicsandComputerScience,HunanNormalUniversity,Changs

3、haHunan410081,China)Abstract:Inordertocheckthecongruencebetweentheuser'sdemandandimplementationofWebServicescombination,anauto-checkingmethodwasproposedinthispaper.Itwasbasedontheknowledgeofopen二一bisimulationandcheckingtools.First,theuser'sdemandandBPEL4WSprogramweremodele

4、dby二一calculusrespectively.Then,weakopen-bisimulationwasdonetothem.Whentheyweredissimulating,thecheckingtoolcanmarkthedissimulationpartofBPEL4WSprogram.Intheend,acasestudywasmadetoshowthefeasibilityofthemethod.Keywords:rr-calculus;BPEIAWS;open-bisimulation;on-the-fly;model-

5、checking范中的哪一个动作不匹配。为了解决人工识别不互模拟的规0引言范形式化描述片段与程序实现形式化描述片段的困难，整个Web服务组合服务模型是组合服务实现逻辑的高层描检验过程完全自动化:自动地转换，自动地检验，自动地标识。述，其正确性对于保证组合服务的正确运行至关重要。基于为使不互模拟时自动标识程序片段，本文对文献【2〕中提出业务流程的建模方法(BPEL4WS)是目前主流的组合服务建的开互模拟检验算法进行了扩充。模方法之一，由于基于流程的建模方法直观地反映了组合服1概念务的执行过程，并且易于实现相应的解释运行系统，因此在当前服务组合

6、研究项目和原型系统中得到了广泛的采用。但是1.1二一演算组合服务建模的正确性主要依赖于对于建模语言的语义的准二一演算分为两种基本的类型:在每一个同步通信时只有确把握和建模者的经验，对于复杂流程逻辑的组合服务而言一个名字被传递的单元二一演算川，和可以传递零个或者多个这显然是不够的。因此在建模阶段提供模型正确性保证对于名字的多元二一演算(330组合服务的正确执行十分重要。由于多元二一演算能更容易和更好的用来建模，并且它的现在某些研究借鉴了工作流建模理论的成果，通过将组分类特性与函数语言的类型有点相似，所以我们在这里采用合服务模型与形式化的建模方

7、法，如Petri网、自动机或时态多元pi演算来建模BPEL4WS。多元pi演算的语法〔’〕如下:逻辑等形式化工具之间建立映射关系，从而为服务组合增强A::二FICIXagents模型性质分析和验证的能力。F::=PI(Ax)Fl(。)Fabstractions本文主要研究了嵌人程序验证工具的Web组合服务开C::=PI[x]CI(。)Cconcretions发环境，并以程序验证工具为支撑实现模型的互模拟检验制P::=01a·AIP+QIPIQ(vx)PI导的Web服务组合。为了检验BPEL4WS程序的正确性，由[a二b]Pprocesses

8、于二一演算在描述移动进程这类问题上具有一定的优势〔’〕，故a::二x(input)Ix(output)I:(internal)本文采用了二一演算来进行形式化的验证。首先，把BPE