文档介绍：论文作者签名::丕筮翊兰浚后停荷苏州大学学位论文独创性声明本人郑重声明:所提交的学位论文是本人在导师的指导下,独立进行研究工作所取得的成果。除文中已经注明引用的内容外,本论文不含其他个人或集体已经发表或撰写过的研究成果,也不含为获得苏州大学或其它教育机构的学位证书而使用过的材料。对本文的研究作出重要贡献的个人和集体,均已在文中以明确方式标明。本人承担本声明的法律责任。期:
墨鲎垄适在——年一月解密后适用本规定。苏州大学学位论文使用授权声明塑』兰:厶至本人完全了解苏州大学关于收集、保存和使用学位论文的规定,即:学位论文著作权归属苏州大学。本学位论文电子文档的内容和纸质论文的内容相一致。苏州大学有权向国家图书馆、中国社科院文献信息情报中心、中国科学技术信息研究所蚍绞莸缱映霭嫔、中国学术期刊馀贪电子杂志社送交本学位论文的复印件和电子文档,允许论文被查阅和借阅,可以采用影印、缩印或其他复制手段保存和汇编学位论文,可以将学位论文的全部或部分内容编入有关数据库进行检索。本学位论文属论文作者签名:导师签名:涉密论文口非涉密论文口日期:’,
异步褡楹戏治鲇胙橹し椒ㄑ芯中文摘要随着网络技术的迅速发展,面向服务的体系架构云淞己玫目芍赜眯浴松耦合性和互操作性,已成为一种工业界和学术界广泛接受的网络化软件应用模式。褡魑猄的主流实现方式,正逐步成为网络环境中资源封装的标准方式。目前,裾鸩接傻ヒ坏拿嫦蚬δ芟蛎嫦蛞滴窳鞒套1洌裰芷谒嬷映ぃ使得同步通信模式的褚盐薹阌没枨螅拮枞囊觳絎服务成为研究热点。由于单个的裉峁┑墓δ苡邢蓿A烁映浞值乩霉蚕淼腤服务构建企业级应用系统,褡楹霞际醣涞糜又匾!服务组合研究领域的一个重要的问题是如何形式化描述褡楹弦约叭绾窝橹し褡楹系恼沸浴在对褡楹系哪P徒醒橹な保唤鲆?悸亲楹戏袷欠衤愎δ苄枨螅需要检查是否存在时间冲突或数据不一致等问题,确保构建高效正确的服务组合。本文以异步裎Q芯慷韵螅治鱿喙厥奔浜褪菰际苑窠换サ挠响,对异步褡楹涎橹そ辛松钊胙芯俊V饕D谌莅ǎ从软件体系结构的角度研究褡楹希治龌谑毙蚵呒娜砑逑到峁姑枋鲇镅訶/在描述褡楹戏矫娴挠攀疲捎肵/疵枋龇褡楹系慕换バ形#关的时间和数据约束用疪硎尽基于有限状态自动机理论,建立异步服务的形式化模型。针对仅涉及时间约束的窠⑹奔湟觳酵ㄐ拍P,该模型符合规约,用消息队列模拟异步通信,用时间自动机中的标准时钟来表示时间约束;对于同时涉及时间和数据约束的情况,则建立异步衲P分别提出基于和基于的异步褡合验证方法,并通过贯穿整个分析和验证过程的实例加以说明。关键词:异步褡楹希籜/篨/:时间约束;数据约束作者:石慧娟指导老师:张广泉异步褡楹治觥甹验证方法研究
甌,甇甌琖琖,’甀..疉瓵甀Ⅱ
疪..:籜/籜/;,.
目录章绪论⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.研究背景及意义⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.研究现状⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本文主要研究内容⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.本文组织结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.第二章相关技术概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.窦跋喙丶际酢窀拍罴疤氐恪裉逑到峁埂璤⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯褡楹稀褡楹细攀觥褡楹辖!褡楹涎橹ぁ本章小结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第三章基于疉的褡楹稀衩枋鲇镅浴疉的优点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..
第四章异步裥问交P汀带时间约束的异步窠!.⒋!.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.本章小结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第五章异步褡楹涎橹ぁ模型检测工具简介⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.;⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⒊橄蟆第六章总结与展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本文工作总结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯未来工作展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯参考文献⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯攻读硕士学位期间参加的科研项目和发表的论文⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.致洹.