鉴于一种web服务组合的自动化模型检测方法

《鉴于一种web服务组合的自动化模型检测方法》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号密级UDC学号桂林电子科技大学硕士学位论文题目：一种Web服务组合的自动化模型检测方法(英文)AnAutomaticModelCheckingApproachtoCompositeWebServices研究生姓名：谭征指导老师姓名、职务：骆翔宇(副教授)申请学科门类：工学硕士学科、专业：计算机应用技术提交论文日期：2010年4月论文答辩时间：2010年6月年月日万方数据独创性（或创新性）声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文

2、中不包含其他人已经发表或撰写过的研究成果；也不包含为获得桂林电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处，本人承担一切相关责任。本人签名：日期：关于论文使用授权的说明本人完全了解桂林电子科技大学有关保留和使用学位论文的规定，即：研究生在校攻读学位期间论文工作的知识产权单位属桂林电子科技大学。本人保证毕业离校后，发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有权保留送交论文的复印件，允许查阅和

3、借阅论文；学校可以公布论文的全部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。（保密的论文在解密后遵守此规定）本学位论文属于保密在年解密后适用本授权书。本人签名：日期：导师签名：日期：万方数据摘要摘要如今Web服务广泛分布于互联网中，它们通过彼此之间的交互实现对问题的协作求解。然而，在交互过程中，一些非预期、“不正常”的信息交互时有发生，严重影响了系统的质量及健壮性，有可能使用户得不到正确结果。因此，模型检测Web服务组合的时态认知性质，保障Web服务的正确运行就成为了模型检测领域的热门研究方向。目前，国内外针对W

4、eb服务组合的形式化验证正处于起步阶段，整个验证过程的自动化程度很低，各个技术环节都需要大量的人工操作。为了提高Web服务流程验证的自动化程度，本文提出将Web服务组合的BPEL流程自动转化为模型检测工具MCTK输入代码的一系列转换算法。最后利用这些算法在MCTK环境下对VTA协议和STS协议进行了形式化验证，并自动构建了贷款服务协议的状态转换图。取得的研究成果有：(1)针对Web服务描述语言BPEL，给出相关活动语义。引入迁移七元组概念，基于活动语义，建立BPEL活动与能够反映系统状态迁移关系的迁移七元组的一一对应，为实现流

5、程的自动化验证打下基础；(2)分别提出将BPEL控制流、数据流转化为迁移七元组集合的转换算法B2T和F2T。这些算法自动将BPEL流程转化为迁移七元组集合，实现了将组合业务流程自动转化为多分支状态转换图的功能；(3)提出根据迁移七元组集合自动生成MCTK代码的转换算法T2M。为了实现控制流的全自动检测，T2M算法根据迁移七元组集合中各元组的相互关系，结合MCTK语言自身特点，自动生成用来描述流程的MCTK代码，避免了繁琐的人工编码工作，实现控制流的自动化检测；(4)运用模型检测工具MCTK验证VTA的时态认知规范以及STS中存

6、在的特征交互问题，说明了论文提出方法的正确性及有效性，同时，利用F2T算法自动构建了贷款服务协议的状态转换图，为下一步验证做好了准备。关键词：模型检测；Web服务组合；特征交互；BPEL。–I–万方数据AbstractAbstractToday,WebservicesarewidelydistributedovertheInternet,thetasksofcompositeWebservicesaresolvedthroughtheinteractionsbetweentheseWebservicesinvolved.How

7、ever,intheinteractionprocess,itispossiblethatsomeunexpectedor"notnormal"informationinteractionswilloccur,whichmaycausesomeincorrectresultgeneratedandseriouslylowerthequalityandrobustnessofasystem.Therefore,toensureWebservicescanprovidecorrectfunction,itisnecessaryto

8、applyformalverificationtechniques,suchasmodelchecking,totheverificationofthetemporalandepistemicspecificationsofWebservicecomposition,whic