云应用的建模与验证方法基于soaml和模型检验的云应用正确性验证

《云应用的建模与验证方法基于soaml和模型检验的云应用正确性验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、隶．初大·粤硕士学位论文万方数据云应用的建模与验证方法基于SoaML和模型检验的云应用正确性验证万方数据MODELD呵GANDVERIFICATIoNMETHoDFORCLOUDAPPLICATIONASOAMLANDMODELCHECⅪNGBASEDVERIFICATIONMETHODFORCLOUDAPPLICATIONCOI眦CTNESSAThesisSubIIli仕edtoSoutheastUniversityFortheAcademicDegreeofMasterofEngineeringBYGe

2、ngGuoqingSupervisedbyProf．LiBixinSchoolofComputerScienceandEngineeringSoutheastUniversityJune2014万方数据东南大学学位论文独创性声明本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论义中不包含其他人已经发表或撰写过的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我一刷工作的同志对本研究所做的任何贡献均己在论文中

3、作了明确的说明并表示了谢意。研究生签名：东南大学学位论文使用授权声明东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其他复制手段保存沦文。本人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅私I借阅，可以公布(包括刊登)论文的全部或部分内容。论文的公布(包括刊登)授权东南大学研究生院办理。研究生签名：磊Q氢盅导师签名：{越El期：仞f俐万方数据摘要云计算是伴随互联网的蓬勃发展应运而生的一种新型计算方式，它突破了传统计

4、算的局限，增强了当下急需的计算能力，同时又提供了灵活的可扩展性。云应用是基于云计算思想实现，并部署在云计算环境中的软件系统。云应用大多应用于一些对性能要求很高的领域，因此保障系统的正确性就显得极为关键。本文重点关注云应用与用户、云应用之间和云应用内部的交互正确性。测试和验证是保障软件正确性的主要方法，但是在云环境下，测试技术面临着代价昂贵且操作难度极大等问题。形式化的验证方法规避了上述不足，因而适用于云应用的正确性保障工作。基于模型检验的验证工具SPIN能有效地应用于云应用的验证。但是其支持的建模语言PRO

5、MELA却难以进行通用直观的建模工作，特别在云应用设计阶段难以体现设计的一般化。SoaML是UML的一种扩展。后者是一种标准建模语言，软件行业的广泛实践已经证明了它在系统建模中的有效性和通用性。SoaML秉承了UML通用直观的特性，同时具备了更高的抽象层次。它弥补了UML没有精确语义和很难描述云应用的不足，可用于云应用的建模。本文首先采用SoaML对云应用进行建模。然后，针对SoaML中的ServiceInterface模型的特点，采用层次自动机来描述ServiceInterface，再根据自动机的语义将其

6、转换为PROMELA。同时，将SoaML中的ServiceContract模型采用线性时序逻辑描述。最后将转换而来的PROMELA和线性时序逻辑公式输入SPIN中就可以进行云应用的自动验证。实验表明，该方法可以有效地验证云应用的正确性。关键词：云应用：SoaML；模型检验：形式化验证：模型转换万方数据AbstractCloudcomputingisanewtypeofcomputing，accompaniedbytherapiddevelopmentoftheInternet．Itbreaksthrough

7、theliraitationsoftraditionalcomputing，enhancesimperativecomputingcapacity,whileprovidingflex弛iescalability．Cbudapplicationisakindofsoftwarewhichishnplementedusingtheideaofcloudcomputinganddeployed访thecloudenvironment．Cloudapplicationsaremostlyappliedinsome

8、fieldswithhighperformancerequirements．Asaresult，itbecomesexlremelycriticaltOguaranteethecon'oct／lessofthesystem．ThispaperfocusesontheinteractioncorrectnessbetweencloudapplicationandUSeS，amongcloudapplications