基于Event-B的ad hoc路由协议及任务级时间约束的形式化建模与验证

发布时间：2020-12-06 15:39

　　移动ad hoc网络是由移动节点搭建的临时通信网络。网络中没有任何固定的基础设施和中心管理设备。因为节点可以自由移动,网络拓扑随时可能发生变化。所以ad hoc路由协议必须能在动态的环境中找到从源到目标的有效路径。这使得在此种网络中的路由选择比在有线网络中的路由选择更具有挑战性。当前研究人员已经提出许多在可信的网络环境下工作的ad hoc路由协议,可以分为三类:主动式路由协议、反应式路由协议和混合路由协议。移动ad hoc网络中节点采用无线通信方式,并且没有固定基础设施和中心的安全控制。同固定网络相比,移动ad hoc网络更容易受到物理和通信攻击。此类网络的安全性越来越受到重视。基于在可信环境下工作的路由协议,研究人员提出在非可信环境下工作的安全ad hoc路由协议。如何保证研究人员提出的路由协议或算法的正确性成为一项具有挑战性的任务。本文对当前ad hoc路由协议形式化验证工作进行研究,总结采用Event-B方法从系统需求到形式化建模和验证的分析流程。此外,针对Event-B不支持时间属性描述的问题,提出了任务级时间约束模式。本文的主要贡献如下:·在可信的网络环境下,大多数研究者对单... 

【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校

【文章页数】：170 页

【学位级别】：博士

【部分图文】：

图１．１移动ａｄ?ｈｏｃ网络??

浙江大学博士学位论文?第２章Ｅｖｅｎｔ－Ｂ方法及Ｒｏｄｉｎ工具??ｓｅｅｓ??Ｍａｃｈｉｎｅ?？?Ｃｏｎｔｅｘｔ??ｒｅｆｉｎｅｓ?ｅｘｔｅｎｄｓ??ｓｅｅｓ??Ｍａｃｈｉｎｅ?■?＇■?？?Ｃｏｎｔｅｘｔ??ｅｘｔｅｎｄｓ??ｒｅｆｉｎｅｓ??图２．１机器和环境关系图??ｍａｃｈｉｎｅ?Ｍ??

图２．１机器和环境关系图??


本文编号：2901622