移动ad hoc网络是由移动节点搭建的临时通信网络。网络中没有任何固定的基础设施和中心管理设备。因为节点可以自由移动,网络拓扑随时可能发生变化。所以ad hoc路由协议必须能在动态的环境中找到从源到目标的有效路径。这使得在此种网络中的路由选择比在有线网络中的路由选择更具有挑战性。当前研究人员已经提出许多在可信的网络环境下工作的ad hoc路由协议,可以分为三类:主动式路由协议、反应式路由协议和混合路由协议。移动ad hoc网络中节点采用无线通信方式,并且没有固定基础设施和中心的安全控制。同固定网络相比,移动ad hoc网络更容易受到物理和通信攻击。此类网络的安全性越来越受到重视。基于在可信环境下工作的路由协议,研究人员提出在非可信环境下工作的安全ad hoc路由协议。如何保证研究人员提出的路由协议或算法的正确性成为一项具有挑战性的任务。本文对当前ad hoc路由协议形式化验证工作进行研究,总结采用Event-B方法从系统需求到形式化建模和验证的分析流程。此外,针对Event-B不支持时间属性描述的问题,提出了任务级时间约束模式。本文的主要贡献如下:·在可信的网络环境下,大多数研究者对单独的主动式路由协议或者反应式路由协议完成了形式化建模与分析。本文采用Event-B方法对混合路由协议ZRP进行建模与分析。本文对协议突出的方面进行了建模:网络拓扑的连接性;节点根据周期性交换的邻居信息构建路由区域;采用边界广播服务的路由发现过程;反应式模块的路由更新。利用Rodin工具,证明了模型构建过程中产生的证明义务,从而确保精化的正确性以及发现路径的无环性和有效性。此外,本文利用ProB对模型与需求描述的一致性进行了确认。因此证明了ZRP协议中路由发现机制的正确性。·在不可信的网络环境下,对安全按需源路由协议SRP的形式化建模与分析。首先,提出了正确发现路径的定义,作为判断协议是否正确的标准。然后根据系统假设和系统需求构建Event-B模型:环境模型,路由发现过程和攻击模型。环境模型考虑了网络拓扑的不稳定性。在攻击模型中考虑了节点丢弃攻击,创建循环路径和创建不存在路径三种攻击行为。通过对不可证明的路径存在性的分析,得出该协议不能防止节点丢弃攻击和创建不存在路径攻击,并给出实例对这些情况进行说明。·在不可信的网络环境下,对安全按需源路由协议Ariadne的形式化建模与分析。由于攻击通常发生在特定的网络拓扑上,在模型构建时,假设网络环境是稳定的。因此,模型对于正确发现路径的存在性,以及网络环境的建模会与SRP协议构建的模型有所不同。模型中考虑了创建循环路径、创建不存在路径、节点删除攻击和虫洞攻击。通过对不可证明的路径存在性的分析,得出该协议不能防止创建不存在路径、节点删除攻击和虫洞攻击。最后,本文给出实例对这些情况进行说明。·针对Event-B不支持时间属性描述的问题,本文提出了任务级时间约束模式。采用Event-B构造用于描述重合、互斥、优先和子事件任务级时间约束的模式。首先构建描述单个任务时间属性的任务最后期限模式。在此模式基础上,通过精化机制构建不同的任务级时间约束模式。它们适用于实时系统的形式化建模和分析。最后,采用提出的重合和优先模式对实例进行形式化描述与分析。