Print

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 展望
  • 致谢
  • 参考文献
  • 攻读学位期间的研究成果

    • 相关论文文献

    本文来源: https://www.lw50.cn/article/02d44c52758d4ab2b1a7aa1e.html