有界模型检测完性阈值的优化计算.pdf

有界模型检测完备性阈值的优化计算 摘要 论文题目：有界模型检测完备性阈值的优化计算 专 业：计算机软件与理论 硕士生：陶瑞甫 指导教师：张治国副教授 摘要 有界模型检测是寻找系统错误的一种符号化模型检测技术。它使用可满足性 问题求解器求解模型检测问题，避免了其他模型检测技术面临的状态空间爆炸问 题，然而它的计算时间复杂度是指数级别的。有界模型检测方法的一个最大不足 是，它虽然能有效的证明系统不满足某一性质，但很难或不能证明系统满足某一 性质，即只能证伪不能证实。所以有界模型检测对系统的验证是不完全的或者说 是不完备的。每一个有限状态系统模型M和线性时态逻辑公式万，都存在一个 自然数CT，如果找不到长度小于CT的线性时态逻辑公式万的反例，那么系统 Threshold)。完备性阈值的计算是很困难的，有时候计算出来的值是巨大的。本 文讨论了系统模型的表示，提出系统关键变量和等价简化模型的概念，通过寻找 非系统关键变量来合并系统状态，得到等价简化模型。在这个模型上计算完备性 阈值，提高了计算的效率同时得到简化模型的缩小的完备性阈值。本文实现了基 于深度优先有哪些信誉好的足球投注网站的算法来计算可达性递归直径，修正了以往算法存在的对同一状 态可能重复计算的缺点。最后通过实验分别对本文算法和模型简化策略进行测 试，结果表明：本文算法计算出的可达递归直径是正确的而且在递归直径大于 40的时候开始表现出好于以往算法的效果；采用本文方法构造出优先队列模型 的等价简化模型，计算其递归直径更加直观，而且保证了简化模型同样满足验证 性质。本文的方法可应用于有界模型检测器的实现以提高其有效性。 关键词：有界模型检测、完备性阀值、可达性递归直径、系统关键变量、等价简 化模型 有界模型检测完备性阈值的优化计算 Abstract Title： ofthe Thresholdfor OptimalComputationCompleteness BoundedModel Checking Science Computer Major：Theoretical Name： Tao Ruifu Supervisor：A．P．ZhiguoZhang Abstract Boundedmodel ofthe model checking，onesymboliccheckingtechniques，is used in usesBoolean for systemdesign．It Satisfiability normally detectingbugs Solvertosolvemodel itavoidsthe ofstate checkingproblems，so problem space thatothermodel runsin explosion checkingtechniquesalwaysface，but exponent time．Howeverthemost ofboundedmodel isthatit importantdeficiency checking can cannot isto