车载无线自组织网络(VANET)是建立在移动车辆上的分布式移动通信和计算机网络相结合的自组织通信网络,有助于实现智能化的导航服务,降低交通事故发生的概率。高可靠路由协议是车载无线自组织网络的关键技术,要求在无基础设施支持下实现可信和稳定的多跳信息传输,以保证智能交通系统中车辆安全。概率模型检验能够遍历系统全局状态空间,缓解系统验证中的状态空间爆炸问题,有希望为VANET的高可靠路由协议分析与设计提供重要的手段。本学位论文首先深入研究城市车载节点移动特点,提出基于曼哈顿移动模型的改进模型,为车载无线自组织网络(VANET)路由协议的研究打下基础;接着利用概率模型检验技术研究VANET的AODV路由协议,并对该协议进行了优化;最后研究VANET的GPSR路由协议,建立该协议的概率时间自动机模型并对比分析。本文的工作创新主要体现在以下三个方面:(1)提出一种基于改进曼哈顿移动模型的VANET城市车载移动模型,利用概率模型检测技术将其建成离散时间马尔科夫链模型(CTMCs),并使用概率模型检测工具PRISM分析其节点移动状态特征。(2)将概率模型检测方法应用于VANET的AODV协议中,建立AODV协议的概率时间自动机模型,设计车载自组织无线网络路由协议的可靠性、概率可达性、期望可达性等模型检测中的评价公式,使用模型检测工具PRISM对协议进行验证,提出AODV协议路由维护过程的优化方案。(3)建立VANET的GPSR路由协议概率时间自动机模型,设计GPSR协议的可靠性、概率可达性、期望可达性等模型检测中评价公式,使用模型检测工具PRISM对协议进行验证与分析。