对具有随机性的网络协议进行验证是一个新的有价值的研究方向,该方向目前的研究方法主要有两种:一是使用概率进程代数的方法;另一种是使用概率模型检测方法。概率模型检测技术它结合了概率分析和通用模型检测技术,能够对具有随机行为的系统进行建模,规约概率性质并进行验证,是硬件和协议验证的主要技术。本文基于概率模型检测技术,针对 Ad Hoc网络中节点的相邻概率、重传协议和概率合同协议进行了研究,构造了系统的概率模型并进行了分析。取得了如下成果:　　(1)分析了Ad Hoc网络中两个节点的相邻概率,应用概率模型检测技术,建立了系统的离散时间马尔可夫链DTMCs模型,描述了性质并进行了验证。分析结果有助于建立与目标节点的有效通信路径和网络性能分析及预测。　　(2)通过对网络重传协议进行深入剖析,将重传协议应用于 Ad Hoc网络环境中。基于概率模型检测技术,对重传协议建立了马尔可夫链和概率有限状态机模型,用概率模型检测工具PRISM进行了验证。量化分析了各种因素对Ad Hoc网络中信息发送和接收的影响,调整协议各参数来提高网络的质量。　　(3)基于概率模型检测技术,建立了概率合同签订协议离散马尔可夫链和概率有限状态机模型,用概率模型检测工具对公平性进行了验证,发现已有缺陷,在此基础上对原协议从双方交换信息的策略上进行了扩充改进,使协议更为公平,满足了合同签订的基本要求。