由于计算机技术的快速发展,系统的可靠性与安全性问题也成为了人们重点关注的问题。目前为了确保系统的可靠性与安全性,一般采用测试或者模拟仿真的技术来对其进行分析。但是这种方法只能考察系统的部分行为,检测出系统的部分问题,难以发现隐蔽的系统缺陷,所以我们在本文中使用了模型检验技术来对系统进行验证。目前已有大量模型检验技术的研究应用于各个领域,但想要完全取代软件测试等技术却还面临着很大的问题。一方面模型验证是一种基于模型的方法,模型的构造便显得尤为重要,目前的计算机系统规模日趋庞大,系统模型在验证的过程中很容易产生状态空间爆炸的问题。另一方面模型检验方法的理论较深,规约、建模方法多种多样,用来进行验证的模型检验工具也大多不具有很强的通用性,所以想要熟练掌握模型检验的方法需要花费大量的时间与精力,这在一定程度上阻碍了模型检验技术的推广。本文中首先使用模型检验的技术来对路由协议进行验证。为了简化研究人员对于协议的分析,我们提出了一种抽象描述的方法来对复杂的网络协议进行抽象表示,保留协议性质相关的属性与行为,删除冗余的的部分,减少系统规模。然后以两种协议为研究实例,分别提出了三种不同的性质,对它们分别进行网络协议的可靠性和安全性验证。这两种协议分别代表了小型网络和大型网络的路由协议,验证目标也包括协议内部的设计缺陷和外部攻击,可以说明我们的验证方法在路由协议上的适用性。为了解决手动建模带来的不足,保证系统与模型的一致性,我们开发了一款模型转化工具来将C语言源码自动转化成验证模型,并以ARINC-653为研究实例说明了该工具的可用性。