基于LSC的Web服务组合模型验证方法研究

《基于LSC的Web服务组合模型验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、随着Web服务技术的迅速发这些单一的Web服务功能有限，Web服务，允许其他应用程序通便用于表达业务流程。因此，如何确保组合起来的Web服务的正确性，成为Web服务研究领域中的热点。形式化方法在对基于消息通信和并发系统建模和分析方面已经成为非常重要的手段，其中模型检测作为一种自动验证技术被许多学者应用于Web服务组合的验证。本文首先介绍了模型检测和时态逻辑的基本概念及业务流程执行语言(BPEL)和时间自动机的相关知识，并基于模型检测方法对Web服务组合验证开展研究，完成的主要工作如下：l、在分析LSC的语法和基于路径的语义基础上，改进了LSC图到时态逻辑公式的转换方法

2、，得到较短的时态逻辑公式，以便降低传统的模型检测对Web服务组合进行验证的复杂性。2、提出了一种基于LSC的Web服务组合验证方法。该方法首先扩展了WS．BPEL的时间属性，并给出了BPEL描述的业务流程到时间自动机网络转化方法；其次，对LSC语法及语义进行时问属性方面的扩展，Web服务组合需要满足的场景用扩展后的LSC图来描述，并将LSC图转换为观察时间自动机；最后，通过将观察时间自动机与BPEL转化来的时间自动机网络同时嵌入到模型检测工具UPPAAL中，完成BPEL描述的业务流程是否满足LSC表示的性质的检测。3、通过一个实例并使用UPP丸～L工具对转换后的Web

3、服务组合和场景性质进行验证。实例分析表明了本文给出的验证方法的有效性。关键词：web组合服务，BPEL，模型检测，时间自动机，时态逻辑，UPPAALAbstract一——————————————————————————————————————一WiththerapiddevelopmentofWebservicestechnology，agrowingnumberofWebservicesrunningontheIntemet，theseatomicWebservicefunctionislimited，andincreasinglyunabletomeetthene

4、edsofusers，buttheseatomicWebservices，allowingotherapplicationsassembledintoacomplextobesousedtoexpressbnsinessprocessesviaanIntemetconnectionandcall．Therefore，inthefieldofWebseⅣicesrese棚rchhowtoensurethecorrectnessofthecombinedWebservicesisbecomingahotspot．Formalmethodsbymanyresearchers

5、basedmessagingandconcurrentsystemsmodelingandanalysishasbecomeaveryimportantmeansofmodelcheckingasanautomatedverificationtechnologyisusedinWebservicecompositionverification．ThispaperfirstintroducesthebasicconceptsofmodelcheckingandtemporallogicandthebasicsknowledgeaboutBPELlanguageandti

6、meautomataaswe儿asresearchmethodsofWebservicecompositionbaseonmodelchecking，completedthemainworkisasfollows：1、ThepapergiveaimprovedtranslationofLSCbetweentheLSCmapandtenlporallogicbasedonanal37zethesyntaxandsemanticsofLSCareshorterandconcisetemporallogicformulaisobtainedwhichareabletored

7、ucethecomplexityoftraditionalverificationofWebservicecomposition．2、AnapproachWasproposedtoverifycompositeservicesbymodelcheckingbasedonLSC．Firstly，expandtheWebservicesbusinessprocessexecutionlanguage(ws．BPEL)TimeProperties，andgivesthebusinessprocessesdescribedinBPELtotimedautom