文档介绍：论文作者签名:互垒叠苏州大学学位论文独创’胜声明本人郑重声明:所提交的学位论文是本人在导师的指导下,独立进行研究工作所取得的成果。除文中已经注明引用的内容外,本论文不含其他个人或集体已经发表或撰写过的研究成果,也不含为获得苏州大学或其它教育机构的学位证书而使用过的材料。对本文的研究作出重要贡献的个人和集体,均已在文中以明确方式标明。本人承担本声明的法律责任。.日
●
::型:乏五日‘期:型:笸:在——年一月解密后适用本规定。苏州大学学位论文使用授权声明非涉密论文∥本人完全了解苏州大学关于收集、保存和使用学位论文的规定,即:学位论文著作权归属苏州大学。本学位论文电子文档的内容和纸质论文的内容相一致。苏州大学有权向国家图书馆、中国社科院文献信息情报中心、中国科学技术信息研究所蚍绞莸缱映霭嫔、中国学术期刊馀贪电子杂志社送交本学位论文的复印件和电子文档,允许论文被查阅和借阅,可以采用影印、缩印或其他复制手段保存和汇编学位论文,可以将学位论文的全部或部分内容编入有关数据库进行检索。涉密论文口本学位论文属导师签名::.
基于谓词抽象与精化技术的裱橹ぱ芯中文摘要面向服务体系结构羌堂嫦蚨韵蟆⒒诠辜7⒅蟮囊恢中滦腿砑发、部署和集成模式,为软件开发提供了灵活的设计和开发方案。褡魑猄的一种实现方法,突破了传统的分布式计算模型在通信、应用范围等方面的限制,通过服务组合的方式,灵活、快速构建的网络应用已经渗透到国民经济的许多关键行业。在现有的裱橹し椒ㄖ校P图觳庖蚱渥远潭雀摺⒛芄惶峁┓蠢径等优势,得到了广泛应用。但在模型检测过程中,会因系统规模庞大而导致状态爆炸问题,如何选取合适的方法缓解状态爆炸已成为服务验证领域的一个研究热点。本文在传统的模型检测方法中引入谓词抽象和精化技术,提出一种用于裱橹的抽象精化验证框架,用以验证衲诓苛鞒搪呒陌踩院妥楹戏窦涞募主要工作如下:褂肒峁苟訵服务建模,通过分解待验证性质得到原子命题从而获取谓词公式集合,使用谓词抽象技术建立竦某橄竽P停再将各抽象模型组合得到待验证系统的组合抽象模型。龀橄竽P偷絇语言的转换规则,使用模型检测工具验证模型是否满足待验证性质,如果不满足,则给出反例。将得到的反例在裆献鐾队安僮鳎蟹蠢啡希圆伪反例的癯橄竽P徒芯ɑ尚碌淖楹铣橄竽P停俅味孕灾式醒证。谏鲜隽椒矫婀ぷ鳎岢鰓服务抽象精化验证框架,并通过实例说明其在缓解状态爆炸方面的可行性。关键词:瘢晃酱食橄螅荒P图觳猓籗怀橄缶ɑ作者:任强指导教师:张广泉容性。
琧琣,,琩琣瓵瑃,,甀,,.瑃.,,,.●
:籑甌,;瑆,;;
目录第一章绪论⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.研究背景及意义⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯国内外研究现状⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本文研究内容⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..本文组织结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..第二章抽象精化技术概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..抽象技术概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..抽象技术主要方法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。.⋯⋯⋯⋯⋯⋯⋯⋯⋯.:⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯...⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本章小结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第三章基于谓词抽象的窠!裼隬服务组合概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.多个竦淖楹夏P汀.
第四章産服务抽象精化验证方法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.模型检测概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯结构到P偷淖;弧癯橄缶ɑ橹ぁ本章小结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第五章实例分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯基于谓词抽象的裨闯绦蚰P图觳狻缓冲区管理系统的抽象精化验证⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第六章总结与展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯本文工作总结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯未来工作展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯参考文献⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.攻读硕士学位期间参加的科研项目和发表加的论文⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.致谢⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯