基于SAT的有界模型检测及其应用研究

摘要

无论在计算机系统硬件设计方面还是在软件设计方面，随着设计规模越来越复杂和庞大，会产生越来越多的设计缺陷和错误等。用一些传统的方法往往是代价很高，但还难以检测出它们。形式化验证的优点是在一个设计或系统的研制周期的前期进行。在研制周期的早期进行分析和验证，可大大降低返工的成本，提高效率。基于这些原因，有界模型检测(Bounded Model Checking简称BMC)作为一种重要的形式化验证的方法，它的相关技术的研究和应用在当前具有相当重要的价值和意义。 有界模型检测是通过把有限状态机(FSM)和LTL逻辑验证规范否定形式编码成SAT实例，再由各种SAT工具来求解，以获得反例。该方法相比基于OBDD技术的模型检测，进一步减轻的状态空间爆炸问题，且给出的反例是最短的。 因为BMC较晚出现，它的很多相关的技术不完善、相关的应用也不普遍。本文围绕BMC的相关技术和应用进行了一定的研究。主要工作如下： BMC编码技术的优化可生成规模小易于求解的SAT实例，对提高有界模型检测的效率至关重要，近年其是BMC研究中一个热点问题。本文结合FSM状态转移的特性和线性时序逻辑的语义，在现有的编码基础上，对有界模型检测中对验证G(p)和G(p→F(q))这两个很重要很常用的模态算子转换公式进行了优化，给出了简洁高效的递推公式；证明了递推公式和原公式的逻辑关系；基于递推公式设计了编码算法。通过实验比较分析，基于递推公式编码算法在生成SAT实例规模和求解效率方面，都优于现有的两个主流的编码算法。所给出的方法和思想对有界模型检测的其他模态算子编码的优化，有直接的参考价值。 SAT工具是BMC的后端求解工具。SAT问题的研究对包括BMC在内的许多领域都很有意义。局部搜索方法是求解SAT实例的一类重要的方法。本文提出用初始概率的方法对局部搜索算法中的变量的初始随机指派进行适当的约束，用该方法对目前的一些重要的SAT问题的局部搜索算法进行改进，通过对不同结构、不同规模的SAT问题的实例测试表明，改进后的这些局部搜索算法的效率有了较大的提高。 提出用BMC和串空间结合的方法对安全协议进行验证。主要是通过串空间理论先确定不安全协议的丛结构，依此来约束协议运行的的规模和角色行为，然后用BMC对该丛结构进行建模验证。这种方式结合了模型检测和定理证明的优点，通过几个安全协议的分析和实验，验证了本方法较传统的模型检测方法的验证效率高。

目录

文摘

英文文摘

声明

第1章绪论

1.1形式化验证及相关知识

1.2模型检测技术

1.3定理证明方法

1.4论文的安排和贡献

第2章BMC的基础

2.1 BMC的语法

2.2 BMC的语义

2.3 BMC的特点和优势

2.4 BMC国内外研究现状

第3章BMC的编码技术

3.1 BMC转换公式及有关定理

3.2 BMC的递推公式编码优化

3.3相关的工作

3.4实验结果及分析

3.5本章小结

第4章SAT问题

4.1 SAT问题的术语

4.2 SAT的表达格式

4.3 SAT算法的研究

4.4实验结果及分析

4.5本章小结

第5章串空间理论基础

5.1基础知识

5.2串空间模型简介

5.3串空间模型测试原理

5.4本章小结

第6章BMC和串空间相结合的协议验证

6.1安全协议形式化验证的方法

6.2 Needham-Schroeder Public Key协议的分析

6.3 Helsinki协议的分析

6.4实验结果及分析

6.5本章小结

第7章结论与展望

参考文献

读博期间的主要科研成果

致谢