基于内存和状态管理的模型检测方法

发布时间：2019-11-25 10:55

【摘要】：模型检测是一种自动化形式验证技术，主要用于检测软硬件设计模型，，这些模型规范通过时序逻辑公式给出。模型检测从用户所描述的模型开始，然后发现用户断言的假设对该模型是否有效。如果无效，模型检测工具可以产生由执行轨迹所构成的反例。然而模型检测存在因状态空间爆炸而导致内存不够的问题，这也是大规模并发系统验证的瓶颈。很多研究人员做了很多相关研究，虽然没有彻底地解决这个问题，然而提出了一些技术在特定的情况下可以大大地提高检测效率。其中效果较为理想的就是on-the-fly模型检测。 on-the-fly模型检测将自动机理论应用到模型检测中，在很多情况下并不需要构造整个系统的状态空间。这是因为在检测系统的自动机A和属性自动机S的乘积时，A的状态仅当需要它们时才被构造出来。 on-the-fly模型检测优势是，当检测系统的自动机A和属性自动机S的乘积自动机时，根本就不会生成A的某些状态。另外一个优势是，在完成构造两个自动机的交之前，可能已经找到了一个反例。一旦找到了一个反例，就没有必要再继续构造乘积自动机。在on-the-fly模型检测中，乘积自动机的状态由双深度优先算法按需产生。本文分析了这个双深度优先算法在检测过程中的内存使用情况。双深度优先遍历中需要用到两个堆栈，当系统规模很大时，要找的反例路径可能非常长，这就是使得堆栈上要存放很多状态。通过利用数据库，可以将搜索堆栈里暂时用不到的状态存储到外存上，在需要的时候再调回内存，这样可以减少在检验器运行过程中对内存的需求，从而提高了模型检测的能力。本文提出了两种利用数据库的方法。一种是静态的状态和内存管理，一种是动态的状态和内存管理。由于使用了数据库，将内存中的状态存储到磁盘上可能出现的内存抖动问题。针对两种不同的内存和状态管理策略，分别提出了相应的内存状态管理策略以很好的解决内存抖动的问题。在开源软件SPIN的基础上，将本文描述的算法实现，这样做主要是利用SPIN原有的存储状态的数据结构，以及它的输入输出方法。算法实现后，通过实验分析了动态管理内存中的状态的算法的实际效果，并分析了在实际运行中算法的优势和未来的工作。
【学位授予单位】：电子科技大学
【学位级别】：硕士
【学位授予年份】：2012
【分类号】：TP274;TP333.1

【参考文献】