基于属性的层次移动IPv6(HMIPv6)协议的验证.pdf

《基于属性的层次移动IPv6(HMIPv6)协议的验证.pdf》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、研究生：鏖蟹耀指导教师：吐堑丝熬援专业：盐篡扭型堂皇撞丕研究方向：．圈终迹这丝式丝撞鲨皇测达所在学院：让篡扭堂暄2011年5月9日原创性声明IIIIIIIIIIllUllIIIIIIIY1887457本人声明：所呈交的学位论文是本人在导师的指导下进行的研究工作及取得的研究成果。除本文己经注明引用的内容外，论文中不包含其他人己经发表或撰写过的研究成果，也不包含为获得囱苤直太堂及其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。学位论文作者签名：攀竖指导教师签名：日期：22丝：≤：12日期：、，、刀产一>杉毛2忽f7．‘．门

2、在学期间研究成果使用承诺书本学位论文作者完全了解学校有关保留、使用学位论文的规定，即：内蒙古大学有权将学位论文的全部内容或部分保留并向国家有关机构、部门送交学位论文的复印件和磁盘，允许编入有关数据库进行检索，也可以采用影印、缩印或其他复制手段保存、汇编学位论文。为保护学院和导师的知识产权，作者在学期间取得的研究成果属于内蒙古大学。作者今后使用涉及在学期间主要研究内容或研究成果，须征得内蒙古大学就读期间导师的同意；若用于发表论文，版权单位必须署名为内蒙古大学方可投稿或公开发表。、，学位论文作者签名：篷坌聋指导教师签名：∑空簦兰鱼日期：2翻：Z：12日期：互4L』：12内蒙古大学硕士学位论文

3、基于属性的层次移动IPv6(HMIPv6)协议的验证摘要随着互联网的高速发展，网络协议标准也不断地更新和完善。如何更有效地提高网络服务，已成为网络协议工程领域的关键问题之一。层次移动IPv6协议作为移动IPv6协议的扩展，在移动IPv6的基础上对移动节点在小范围内快速切换作出了改进。CPN(ColouredPetriNets)是一种形式化建模语言，适用于通信和并发系统。CPN为使用者提供了直观的图形化的形式化描述方法，并且CPN的模型语言是通用目的的建模语言。本文通过形式化方法对自然语言描述的HMIPv6(砌℃5380)协议规范进行建模，并对HMIPv6协议的基本属性进行形式化验证。由于

4、协议并发行为引发的状态爆炸问题严重影响了验证工作的进行，本文提出了模型化简和抽象的方●法，化简法将模型化检为多个并发子模型，抽象法将并发子模型进行抽象层次的提升，合并二些库所和变迁，以减少状态空间规模，保证属性验证工作的效果。最后，本文将以上方法应用于HMIPv6协议模型，验证了方法的有效性。关键词：HMIPv6协议，形式化建模，ColouredPetriNets，属性，形式化验证，模型检测．基于属性的层次移动口v6(HM口v6)协议的验证HMIPV6FOR^压ALVER【F．ICATIONRESEARCHBASEDONCOLORPETRINETSABSTRACTW油therapidde

5、velopmentofIntcrnct，networkprotocolstandardsareconstantlyupdatedandimproved．Howtoeffectivelyimprovethenetworkserviceshasbecomeoneofkeyproblemsofthenetworkprotocolengineeringfield．AsanextensionofmobileIPv6(MIPv6)，HierarchicalmobileIPv6(HMIPv6)ismadetoimprovetheⅣ【N(mobilenodes)fast—movinginasmallra

6、ngeregionbasedonMIPv6(MobileIPv6)．’：CPN(ColouredPetriNets)isaformalmodelinglanguage，whichissuitablefordescribingasystemwithconcurrencyandcommunication．TheCPNprovidesaformaldescriptionmethod，whichismoreintuitiveandgraphicalfortheusers．AndtheCPNmodelinglanguageisageneral—purposemodelinglanguage．。：I

7、nthisthesis，aformalmodelisgivenfortheHM口v6protocolwhichhasbeendescriptionbynaturallanguage，andthebasicpropertiesofHMIPv6protocolmodelisverified．Becauseofthestateexplosionproblemcausedbyconcurrentbehavior,verificationha