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

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

ID:35059033

大小:3.49 MB

页数:84页

时间:2019-03-17

基于verics的web服务建模与验证_第1页
基于verics的web服务建模与验证_第2页
基于verics的web服务建模与验证_第3页
基于verics的web服务建模与验证_第4页
基于verics的web服务建模与验证_第5页
资源描述:

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

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

2、责任。日占、了,:论文作者签名:幸苟签名期学位论文版权使用授权声明本人同意授权华侨大学有权保留并向国家机关或机构送交学位论文的复印件和电子肢,允许学位论文被查阅和借阅。本人授权华侨大学可L义将本学位论文的全部内容或部分内容编入有关数据库进行检索k乂采用影印、缩印或担描等复制手段保存和汇编本学位论文。,可:论文作者签名:和哨指导教师签華换轉]..日期签名日期签名:从摘要摘要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

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。