普适环境下基于抽象状态机服务组合分析的研究与验证

《普适环境下基于抽象状态机服务组合分析的研究与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、上海交通大学硕士学位论文DissertationSubmittedtoShanghaiJiaoTongUniversityforMasterDegreeofEngineeringTheAnalysisandValidationofServiceCompositioninPervasiveComputingBasedonASMAuthor：YiLiangchenStudentID:1100339111Specialty:ComputerTechnologySupervisor:Prof.HuangLinpengSchoolofElectronicsandEl

2、ectricEngineeringShanghaiJiaoTongUniversityShanghai,P.R.ChinaDecember,2012万方数据上海交通大学硕士学位论文第62页万方数据上海交通大学硕士学位论文第63页万方数据上海交通大学硕士学位论文上海交通大学学位论文原创性声明本人郑重声明：所呈交的学位论文《普适环境下基于抽象状态机的服务组合的分析与验证》，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明

3、确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：日期：年月万方数据上海交通大学硕士学位论文上海交通大学学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。保密□，在年解密后适用本授权书。本学位论文属于不保密□。（请在以上方框内打“√”）学位论文作者签名：指导教师签名：日期：年月日日期：年月万方数据

4、上海交通大学硕士学位论文普适环境下基于抽象状态机的服务组合的分析与验证摘要[1,2]自20世纪90年代Weiser提出“普适计算”概念以来，嵌入式系统，无线通信等技术的发展为“服务无时不在，无处不在”的普适计算从理论变成现实提供了客观的技术基础。普适计算的目标是将由网络和传感器以及移动设备组成的信息空间和现在的物理空间结合起来，支持用户随时随地获取所需的服务。因此如何在普适环境下进行有效的服务组合逐渐成为了一个热点。在普适环境下，不仅有网络上的web服务，还有传感器和移动设[3]备等提供的设备服务以及各类其他的服务，结合SOA思想，共同组成了组合服务并将其

5、最终构建应用模型。但是，由于普适计算环境所具有的自治性，动态性和设备资源的约束性，使得在这样的环境下进[4]行服务组合时面临着特有的问题和挑战,比如服务组合过程中错误的处理、检测，比如设备的动态加入和删除等。因此在普适环境中，如何为用户提供可信的服务组合成为了普适环境下服务组合的关键问题。本文分析了已有的服务组合的技术以及服务组合模型，并在此基础上提出了一个基于抽象状态机的服务组合模型，并提出验证方法。使用抽象状态机对服务的行为进行刻画，能够很好地对服务进行不同第I页万方数据上海交通大学硕士学位论文精化层级上的形式化描述，从而达到不同层级的正确性验证需求。

6、然后结合SPIN进行安全性、可达性的模型检测。最后本文在实验中利用工具CoreASM和SPIN对文中提出的服务组合模型进行验证，从而保证服务组合的正确性。实验结果表明，我们所提出的服务组合模型和验证方法能够较好地适应普适环境下服务组合系统的需求，验证其正确性，对后续的基于这样的服务组合的实际应用和开发带来积极的意义。关键词：抽象状态机、服务组合、模型验证第II页万方数据上海交通大学硕士学位论文TheAnalysisandValidationofServiceCompositioninPervasiveComputingBasedonASMABSTRACTT

7、heconceptofPervasiveComputingisinitiatedbyWeisersince1990s.Thedevelopmentofembeddedsystems,wirelesscommunicationtechnologyisacceleratingtheprocesstomakepervasivecomputingfromtheoryintoreality.ThegoalofPervasiveComputingistocombinethephysicalspaceandthedigitalspaceusingnetwork,sens

8、orsaswellasmobiledevices,soastosu