模型检测形式化分析中若干关键问题研究

论文摘要

模型检测是近二十年来最成功的形式化自动验证技术之一。其因自动化程度高,效率高等优点而被广泛应用于并发系统的分析与验证中。与定理证明等其他形式化验证方法相比,模型检测的主要优点在于:当断言被违反时,模型检测方法能够给出反例,以解释断言被违反的原因。然而,由于复杂系统的反例通常很长,导致非常难以理解,需要花费大量时间检查大量的变量和事件,才能够找到错误的根源。这些客观因素都影响了模型检测验证的效率。状态爆炸问题一直是模型检测的瓶颈问题。为了能够有效地应用模型检测方法,研究人员提出可以减少和压缩状态空间以缓解状态爆炸问题。因此,论文主要从模型检测的反例最小化分析、解决状态爆炸问题以及扩充Promela三个方面进行了研究,具体内容如下:1、介绍了Gastin.P最小反例算法思想,结合著名的Needham-Schroeder公钥身份认证协议对算法进行了非形式化分析,实例分析的结果表明了算法的有效性。在算法的基础上结合语法重定序策略提出了一种新的算法框架,解决了算法在搜索最小反例的过程中对状态的重复遍历的缺点。2、针对模型检测中存在的状态爆炸问题,从原子性、缩减随机数变量的取值范围、语法重定序以及偏序归约技术四个方面进行了研究。通过理论论述和实验验证相结合的方式说明了这些优化策略能有效地减少状态数。3、在Promela基本数据结构的基础上,扩充了栈和队列两种数据结构。主要是对顺序栈和循环队列进行了定义和实现。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 研究背景
• 1.2 论文的主要工作
• 1.3 论文的结构及章节安排
• 第2章 模型检测
• 2.1 并发系统
• 2.2 模型检测
• 2.2.1 主要步骤
• 2.2.2 状态爆炸问题
• 2.2.3 模型检测工具
• 第3章 模型检测工具SPIN及建模语言Promela
• 3.1 模型检测工具SPIN
• 3.1.1 SPIN工作机理
• 3.1.2 SPIN的特征
• 3.1.3 基本数据结构
• 3.2 Promela及系统建模
• 3.2.1 建模语言Promela
• 3.2.2 系统建模
• 3.3 SPIN对网络认证协议的安全性分析
• 3.3.1 对认证协议的建模
• 3.3.2 时态逻辑
• 3.3.3 验证
• 3.3.4 对NS协议实例分析
• 第4章 反例最小化分析
• 4.1 反例及其定义
• 4.2 Gastin.P提出的最小反例算法思想
• 4.3 利用NS协议对算法进行非形式化分析
• 4.4 结合语法重定序策略进行优化
• 4.5 本章小结
• 第5章 解决状态爆炸问题的几个策略
• 5.1 原子性
• 5.2 缩减随机数变量的取值范围
• 5.3 语法重定序
• 5.4 偏序归约技术
• 5.4.1 独立性与不可见性
• 5.4.2 LTL-x的偏序归约
• 5.5 本章小结
• 第6章 Promela数据结构的扩充
• 6.1 顺序栈
• 6.2 循环队列
• 6.3 本章小结
• 第7章 总结与展望
• 7.1 总结
• 7.2 展望
• 致谢
• 参考文献
• 攻读学位期间的研究成果