论文部分内容阅读
模型检测技术是一种非常重要的形式化验证技术，其最大的优点就是全自动进行验证。模型检测技术已被应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩目的成就，并从学术界辐射到了工业界。但是，模型检测过程中的状态空间爆炸问题严重制约着模型检测技术在工业界的应用。本文以此为背景，对模型检测技术的相关理论知识进行了学习分析，包括时态逻辑、自动机和模型检测算法。围绕基于磁盘的BFS宽度优先搜索模型检测技术，重点分析研究了模型检测过程中的延迟重复检测，主要内容为：1、研究模型检测过程中状态空间搜索时的延迟重复检测，提出了一种基于分区的延迟重复检测方法。该方法针对BFS宽度优先搜索出现的某些层所拥有的状态无法全部存储到内存中，而影响了模型检测的进行，将每一层的状态进行分区划分，以适应内存的限制，提高了模型检测的时间性能。2、研究有限状态系统状态转移局部性的统计特性，提出了将这一统计特性应用于上述基于分区的延迟重复检测的方法。该方法减少了在基于磁盘延迟重复检测过程中需要从磁盘读取的状态数，同时还保证状态空间的搜索能够终止，从而提高了模型检测的效率。3、在开源软件Murphy的基础上实现了上述的新的基于磁盘的BFS宽度优先搜索模型检测工具，并且进行了对比实验验证。实验结果显示本文实现的模型检测工具与开源模型检测工具Murphy相比，提高了8.37%的时间效率。