无线网络己经被广泛运用于人们日常生活中的许多方面。尤其是在缺少固定基础设施的情况下,无线网络和无线技术是合适的通信解决方案,并且正在被广泛应用于实现信息传输的各种通讯场景中。构成无线网络的基础物理器件是无线网络节点设备,这些无线节点设备为无线网络应用的实现提供了基础的通信功能。无线网络节点设备通常是以无线电波为载体进行广播式的信息发送,这种无线网络的广播信息发送模式与传统的有线以太网络中的全局广播信息发送模式有所不同。在无线网络中,信息数据的广播发送是局部的,也就是说每个无线节点所发送的信息的传输范围是有限的,只有那些处于节点传输半径覆盖范围内的部分接收节点才能够接收到所对应的节点广播发送的信息。受限于有限的信息传输范围,为了使得不在传输范围内的两个无线节点之间能够实现交互,就需要借助其他的中间节点来建立起一条能够传输信息的路由路径。路由协议是实现无线网络中路由路径的建立和维护的一种重要机制,主要是通过各种报文信息在无线网络中的广播来建立路由路径。形式化方法被认为是对无线网络系统进行描述和验证的一种可行并且合适的方式。本文研究面向无线网络系统的形式化方法。我们主要研究无线网络中与通信交互相关的无线网络特性,包括无线节点之间的广播通信交互行为以及无线网络中路由协议建立路由路径的机制。无线网络中无线节点之间的通信实现了无线网路中最根本的信息交互功能。我们考虑无线广播通信的各种物理特征,包括了无线节点的位置、通信范围、通信频率等物理因素。针对通信交互等无线节点底层物理行为的形式化描述和建模通常采用基于通信交互的进程代数演算系统。因此,我们扩展无线系统演算引入无线网络卫兵选择的概念,基于程序统一理提出了无线演算系统的代数语义和指称语义。我们给出了一系列无线系统演算的代数规则,研究从代数语义计算推导出操作语义的方法。无线网络中的路由协议借助无线节点之间的通信交互实现了无线网络中的全局信息交互。针对无线网络中路由协议在路由建立和维护路由路径时的特点,我们主要考虑路由协议实现路由时的各种路由信息数据的处理机制。因此我们采用形式化描述语言对无线网络AODV路由协议进行形式化建模、分析和验证工作并且将底层的无线节点的通信交互行为抽象为针对变量的赋值效果。通过使用这种在更高层次的抽象描述方式,我们能够更直接地分析无线网络路由协议的本质特性。本文的主要贡献包括：·我们提出了无线系统演算的代数语义,给出了一组用于描述无线系统演算并行组合线性展开的代数规则,并且定义了无线网络系统的规范型。借助无线网络系统的规范型,我们给出了从代数语义计算生成操作语义的方法,并且证明了代数语义和操作语义的一致性,从代数语义的角度保证了操作语义的正确性和完备性。我们使用重写逻辑工具Maude实现了从代数语义自动计算操作语义的过程。我们提出了无线系统演算的指称语义,引入了无线网络执行状态和执行轨迹的概念用来描述无线网络的行为。基于指称语义模型,我们证明了无线网络系统的代数性质。·我们使用形式化建模语言Z对无线网络中使用的AODV路由协议进行建模,并且使用基于Rely/Guarantee方法的形式化验证技术证明了协议的性质。通过形式化建模语言,我们在建模过程中消除了路由协议相关文档中自然语言描述的二义性。我们使用程序变量赋值的效果来描述无线节点之间的通信交互。我们对使用形式化语言Z构建的协议模型进行重写得到基于共享变量并行程序语言的改进协议模型。以共享变量并行程序所描述的路由协议形式化模型为基础,我们使用Rely/Guarantee推理规则证明了路由协议建立的路由路径不存在路由环路等性质。