基于petri网的带宽共享协议建模与验证研究

《基于petri网的带宽共享协议建模与验证研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号密级ＵＤＣ采考善硕±学位论文基于Ｐｅｔｒｉ网的带宽共享协议建模与验证研究．．，，辨齡疋ｒ窜謂输豐择闕鄰鑛１＾：蕾藏作者键名：周蠢；：—学科、专业程盤住王＿＿—；学：号：２１２０１３０８３５００００１＜指导教师：宋文：？＃＼藥？户－億＇－ｆ完成日期：４？，．．．．．，。．．。．．，，抑巧年巧；＇＾卢如、．：過＂一＂■－；－；－芯＂山：：；；－、－’斬－＇啤＇二＇＇：．．；，．一Ｓ？－＾５：；３１＾．．节，一為ｉClassifiedInd

2、ex:XihuaUniversityUDC:MasterDegreeDissertationTheStudyofModelandVerificationforBandwidthSharingProtocolsbasedonPetriNetsCandidate:XHUJR2016M10Major:SoftwareEngineeringStudentID:212013083500001Supervisor:Prof.SongWenApril,2016西华大学学位论文独创性声明作者郑重声明：所呈交的学位论文，是本人在导师的指导下进行研究工作所

3、取得的成果。尽我所知，除文中己经注明引用内容和致谢的地方外，本论文不包含其他个人或集体己经发表的研究成果，也不包含其他邑申请学位或其他用途使用过的成果一。与我同工作的同志对本研究所做的贡献均己在论文中做了明确的说明并表示了谢意。若有不实之处，本人愿意承担相关法律责任。学位论文作者签名：尚务指导教师签名：＾曰期；曰期；？４．‘方瓜．；方含寺６西华大学学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，在校攻读学位期间论文工作的知识产权属于西华大学，同意学校保留并向国家有关部

4、口或机构送交论文的复印件和电子版，允许论文被查阅和借阀，西华大学可将本论文的全部或部分内容编入有关数据库进行检索，可Ｗ采用影印、缩印或扫描等复印手段保存和汇编本学位论文。（保密的论文在解密后遵守此规定）学位论文作者签名：指导教师签名间寨曰亂曰期：‘ｙｉＵ－户令吉西华大学硕士学位论文摘要Petri网(PetriNet)是一种重要的形式化建模分析和验证工具，有别于其它建模工具，具有图形化特征和严格的数学分析双重能力。对于多数的离散异步并发系统，Petri网能够很好地进行构建分析。经过半个多世纪的成长，从原型Petri网

5、衍生的高级Petri网[4]应用于很多领域。网络资源的下载速度和种类是衡量用户网络体验的重要指标，内网（局域网）具有网内传输速度快但资源缺乏的特点，外网（广域网）资源丰富但无法突破网络服务商提供的带宽。可将传统的网络文件传输机制分为外网和内网的文件传输，大都只能顾此失彼：外网下载资源存在部分计算机下载速度慢而同时若干计算机闲置的尴尬；内网资源相对缺乏。即使是结合内外网两种环境的传输机制（如局域网中带宽更大的服务器先从外网下载文件，普通计算机再通过传输速度更快的局域网环境从服务器中获取文件，以此来提高文件的下载速度，此方法可以称为代理加速）存在服

6、务器端的下载瓶颈。设计一种在现有硬件环境下能够兼顾资源丰富和下载速度快两大优点的网络文件传输协议是一个值得研究的课题。针对局域网单台计算机下载外网资源速度慢的问题，本文以Petri网为系统逻辑设计工具，提出一种基于P2P（PeertoPeer）分布式结构的外网带宽共享协议。该协议指定内网多台计算机在外网下载所需文件的不同片段，再由局域网传输给任务发起者所属计算机进行原文件整合。协议充分利用多台计算机的并行下载能力以及局域网的快速传输能力，从理论层面提高了单台计算机的下行带宽。本文进一步通过基于Petri网的可达标志图，S_不变量和流程图方法对协

7、议的逻辑正确性和行为许可性进行了验证，验证结果表明：本带宽共享协议可以保证系统是可循环运行的（即系统是不死的）以及下载资源的完整性。关键词：Petri网；建模与验证；P2P网络；网络加速；带宽共享；文件传输协议；分布式系统I基于Petri网的带宽共享协议建模与验证研究AbstractPetriNetsareanimportantformaltoolformodelingandverification.Theyhavethegraphicalandmathematicalcharacteristicsmakethemdifferentwithot

8、hers.PetriNetsaresuitabletomodelthediscreteconcurrentsystems.Formorethanhal