近年来，关于下一代互联网和物联网的研究成果日渐丰富，新的数据通信和传输方法不断涌现。其中，新的路由协议是新型网络的关键部分，其正确性直接影响着网络的稳定性。然而路由协议在设计上具有自身特殊的复杂性，在设计过程中经常会出现一些人工方法难以察觉的缺陷。模型检测是一种形式化的验证技术，能够对系统进行自动验证，并在发现系统缺陷时，给出导致此缺陷出现的执行路径。借助模型检测的这种特性可以发现路由协议中隐含的缺陷，从而提高路由协议的可靠性。基于时间自动机的模型检测工具UPPAAL是一个高效的可达性分析工具，常常被应用于包括网络协议在内的各类实时系统的验证。然而，使用模型检测方法对路由协议进行验证时，还存在以下两方面的问题，一方面是协议建模困难，其中的关键在于复杂定时数据的建模；另一方面是状态爆炸问题严重。本文首先对路由协议中存在的复杂定时数据进行研究。针对复杂定时数据建模困难的问题，提出了一种基于离散化的抽象建模方法。通过实验测试了这种建模方法的有效性，并通过进一步实验分析了这种建模方法的性能。针对模型检测的状态爆炸问题，本文在建模过程中采用抽象技术与组合技术把原模型分解为两个子模型，分别对其进行验证，并通过假设/保证的组合策略验证了原模型的性质。最后，在抽象与组合技术以及复杂定时数据建模方法的基础上，对OLSR路由协议进行验证。实验结果表明，OLSR协议具有无死锁、行为一致性以及连通性。实验结果同时表明，OLSR协议中的路由表计算部分存在冗余计算，可通过延迟路由表计算的策略减少冗余计算。