基于模型检验的系统可靠性和安全性验证

摘要

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

目录

声明

缩略词

第一章 绪论

1.1 课题研究背景和意义

1.2 国内外研究现状

1.3 论文的选题依据和内容

1.4 论文的结构安排

第二章 相关知识

2.1 模型检验概述

2.2 SPIN模型检验工具

2.3 LLVM/Clang编译器介绍

2.4 本章总结

第三章 基于模型检验的路由协议研究与验证

3.1 路由协议的模型检验研究

3.2路由协议的抽象描述方法

3.3 RIP路由协议

3.4 BGP路由协议

3.5本章总结

第四章 模型自动转化技术的研究与实现

4.1 模型转化工具CSPIN Tool

4.2 模型转化的实现方法

4.3 代码转化的实现

4.4 本章总结

第五章 面向ARINC-653接口的研究与验证

5.1 ARINC-653接口简介

5.2 ARINC-653接口的模型抽象

5.3 ARINC-653接口的建模与分析

5.4 本章总结

第六章 总结与展望

6.1 论文总结

6.2 工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文