一种高效大规模系统的LTL模型检测方法

摘要

本发明公开一种高效大规模系统的LTL模型检测方法，采用LHS算法主要针对于快速找到磁盘中哈希表中存储的哈希值，无论内存中的哈希表的分类是否为空，都会在外存中存储哈希表并且存储到外存当中以一个新的技术，I/O的复杂度是哈希表一样的线性大小；CDD技术允许在内存中的副本通过有效访问检测出来，通过HLS，CDD可以降低副本检测的复杂度，DPM的计划使得嵌套的两个深度优先栈可以动态的共享内存单元，并且通过有效对栈和状态的管理可以解决内存的抖动为题，其中内存抖动指的是状态在内存当中的频繁移动，可能会显著的增加I/O的操作次数从而降低算法的效率。

主权项

一种高效大规模系统的LTL模型检测方法，其特征在于，包括：S1、初始化存储结构跟内存使用情况：数据库DB包括四张表，具体为：第一张表tableDD1和第二张表tableDD2用于检测重复状态和两个由相同状态字段和哈希字段组成的数据结构；第三张表tableP1存储着路径在第一个DFS的状态；第四张表tableP2存储着路径在第二个DFS的状态；将内部存储器划分为代码段和数据段，然后将数据段划分为两个相同大小的第一存储模块T1和第二存储模块T2，第一存储模块T1被进一步分为两个大小相同的第一存储单元T11和第二存储单元T12，第一存储单元存储第一DFS的第一哈希表H1，第二存储单元T12存储第二DFS的第二哈希表H2；第二存储模块T2通过第一堆栈stack1和第二堆栈stack2共享动态内存；第一哈希表H1和第二哈希表H2当中的每一个元素都是一个元祖(h,s)，其中，s是表示被访问过的状态，h代表s的哈希值，H1和H2当中的所有元素都存储在时间序列当中；S2、当检测第一堆栈stack1和第一存储单元T11为满状态，执行步骤S3；S3、则将二元组中的一部分第一哈希表H1放到tableDD1当中，并且用调用函数Merge‑sort()对tableDD1进行排序；S4、对于当前状态x，首先通过CDD去执行重复检测；对于每一个成功的状态s，如果s为新的状态，那么将s入栈stack1，同时将二元组(hash(s),s)入栈H1；S5、当所有的成功的状态都被遍历，则从第一堆栈stack1中取出各个成功状态；如果该成功状态是可接受的状态，则进入第二个DFS。