基于verics的web服务建模与验证

《基于verics的web服务建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码：10385分类号：研究生学号：1300220006密级：基于VerICS的Web服务建模与验证AModelingandVerificationMethodforWebServicesBasedonVerICS作者姓名：杜万萧指导教师：骆翔宇副教授学科：计算机科学与技术研究方向：形式化方法所在学院：计算机科学与技术学院论文提交日期：二零一六年六月一日学位论文独创性声明本人声明兹呈交的学位论文是本人在导师指导下完成的研究成果。论文写作中不包含其他人己经发表或撰写过的研究内容，如参考。他人或集体的科研成果，均在论文中Ｌ乂明确的方式说明本人依法享有和承担由此论文所产生的权利和

2、责任。日占、了，：论文作者签名：幸苟签名期学位论文版权使用授权声明本人同意授权华侨大学有权保留并向国家机关或机构送交学位论文的复印件和电子肢，允许学位论文被查阅和借阅。本人授权华侨大学可Ｌ义将本学位论文的全部内容或部分内容编入有关数据库进行检索ｋ乂采用影印、缩印或担描等复制手段保存和汇编本学位论文。，可：论文作者签名：和哨指导教师签華换轉］．．日期签名日期签名：从摘要摘要SOA的出现和快速发展，使得Web服务在软件开发过程中成为了一个举足轻重的角色。由于单一Web服务功能受限，它们很难满足用户日益复杂的需求，很多情况下需要将已存的原子Web服务组合起来以实

3、现目标需求。然而，受到服务本身的特性、复杂多变的网络运行环境及服务开发模式的影响，服务组合的正确性、安全性、时效性性等可信性质很容易受到威胁，为保证Web服务组合的正确运行，有必要对Web服务组合进行可信性质的验证工作。形式化方法中的模型检测技术通常被用来建模Web服务组合的运行过程以及验证Web服务组合的可信性质。针对传统的模型检测方法并不能验证带有时间约束的Web服务组合相关性质的缺陷，本文提出了一种基于VerICS的Web服务建模与验证方法，该方法不仅能够验证带有时间约束的Web服务组合的时态逻辑性质，还能够验证Web服务组合的认知逻辑性质。本文的工作分为以下几个方面：（1）为了能够使用

4、VerICS验证带有时间约束属性的Web服务组合的相关性质，首先提出了Web服务业务流程描述语言BPEL的时间约束属性扩展方法；（2）提出BPEL流程与VerICS输入语言IL的“中间桥梁”BPEL输入输出状态迁移系统BIOSTS形式模型的概念，给出BPEL流程各基本活动与结构活动的的BIOSTS形式化建模过程，为下一步提供BPEL流程的自动化验证程度打下基础；（3）提出BPEL流程到BIOSTS的转化算法BP2BS，以及BPEL各结构活动到BIOSTS的转化算法。这一系列算法实现了BPEL流程的自动形式化建模，提高了Web服务组合的自动化验证程度；（4）提出BIOSTS到VerICS的输入语

5、言IL的转化算法BS2IL。该算法综合考虑形式模型BIOSTS的特征与IL的语法特征，将BIOSTS包含的各元素转化为IL语言中的各个组成部分；实现了二者之间的自动转化，减少转化过程中繁琐的人工编码工作，实现BPEL流程的自动化模型检测；（5）运用模型检测工具VerICS对虚拟旅游系统VTA的时态认知逻辑性质I华侨大学硕士学位论文进行验证，根据验证结果判定该Web服务组合是否满足目标需求。这个实例说明了本文所提出的针对Web服务组合建模与验证的方法的可行性及有效性。关键词：Web服务组合模型检测BPELVerICS时态认知逻辑IIAbstractAbstractTheemergenceandr

6、apiddevelopmentofservice-orientedarchitecturemakestheWebservicebecomingaveryimportantroleintheprocessofsoftwaredevelopment.AsingleWebservicecan'tsatisfyincreasinglycomplexrequirementsofusersbecauseofit'slimitedfunctions.Inmostsituations,weneedtocombinetheexistingsingleWebservicestoachieveourtargetre

7、quirements.However,thecredibilityofWebservicecompositionwhichincludescorrectness,security,reliabilityandsoon,isthreatenedeasilybecauseofthecharacteristicsoftheserviceitself,openandvolatileoperatingdev