SPIN模型检测的形式化分析机理研究及应用

论文摘要

随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。确保这些系统的可靠性成为计算机科学领域中重要研究领域。为此提出的诸多方法和理论中,模型检测以其简洁明了和自动化程度高而倍受注目。模型检测是一种重要的形式化自动验证技术,此技术的成功应用归功于有效验证工具的开发和支持。SPIN是一种著名的分析验证并发系统逻辑一致性的模型检测工具。模型检测的瓶颈问题是状态爆炸问题,如何以使用精简方式描述系统,避免因为模型复杂而引起状态爆炸是一个值得研究的方向。本文在阐述SPIN模型检测形式化分析机理及线性时态逻辑LTL性质的基础上,详细分析了基于SPIN的系统建模语言Promela中的并发进程、通道操作、基本数据结构及其功能,设计了模型检测求解离散化问题的方法——通过Promela建立模型,在描述系统属性(性质)中运用分支界限技术,验证过程中LTL公式动态变化,旨在减少模型状态空间,提高搜索效率,实例分析验证了此方法的正确性;同时采用了启发式策略优化模型,即根据SPIN模型检测深度优先搜索的原则,通过静态分析和动态分析方法优化模型,实验结果分析表明SPIN不但可以验证所求解系统模型的正确性,还可以寻找模型的最优解。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 研究背景
• 1.2 研究内容
• 1.3 本文结构
• 第2章 模型检测及相关技术
• 2.1 模型检测技术
• 2.1.1 简述
• 2.1.2 状态爆炸问题
• 2.2 常见模型检测器的应用
• 2.2.1 硬件和协议验证
• 2.2.2 软件验证
• 第3章 SPIN模型检测的形式化分析机理
• 3.1 概述
• 3.1.1 SPIN的发展历史
• 3.1.2 SPIN的特点
• 3.2 SPIN的理论基础
• 3.2.1 SPIN的基本结构
• 3.2.2 SPIN的工作原理
• 3.3 SPIN的基本数据结构及实例解析
• 3.3.1 状态矢量（State vector）
• 3.3.2 Depth-first stack
• 3.3.3 Seen state set
• 3.4 线性时序逻辑LTL
• 3.4.1 Stutter不变性
• 3.4.2 线性时序逻辑LTL语法
• 3.4.3 线性时序逻辑LTL语义
• 3.4.4 时态逻辑对系统性质的描述
• 3.5 有限自动机
• 3.6 从线性时序逻辑到有限自动机的转换
• 第4章 SPIN的建模语言PROMELA
• 4.1 进程说明
• 4.2 数据类型
• 4.3 消息通道
• 4.4 可执行性
• 4.5 流向控制
• 4.6 断言类型
• 4.7 其他特点
• 4.8 实例分析
• 第5章 SPIN模型检测求解离散化问题
• 5.1 一般方法
• 5.1.1 实例一:士兵过桥问题
• 5.1.2 分析离散化问题算法
• 5.2 改进方法
• 5.2.1 SPIN中嵌入C代码的原语说明
• 5.2.2 结合分支界限技术分析实例一
• 5.2.3 实例二:个性化卡片问题
• 5.3 启发式方法优化模型
• 5.3.1 深度优先搜索算法
• 5.3.2 静态分析方法
• 5.3.3 动态分析方法
• 5.4 小结
• 第6章 结论与展望
• 6.1 结论
• 6.2 展望
• 致谢
• 参考文献
• 攻读学位期间的研究成果