（计算机软件与理论专业论文）有界模型检测完备性阈值的优化计算.pdf

有界模型检测完备性阈值的优化计算摘要 论文题目：有界模型检测完备性阈值的优化计算 专业：计算机软件与理论 硕士生：陶瑞甫 指导教师：张治国副教授 摘要 有界模型检测是寻找系统错误的一种符号化模型检测技术。它使用可满足性 问题求解器求解模型检测问题，避免了其他模型检测技术面临的状态空间爆炸问 题，然而它的计算时间复杂度是指数级别的。有界模型检测方法的一个最大不足 是，它虽然能有效的证明系统不满足某一性质，但很难或不能证明系统满足某一 性质，即只能证伪不能证实。所以有界模型检测对系统的验证是不完全的或者说 是不完备的。每一个有限状态系统模型m 和线性时态逻辑公式万，都存在一个 自然数c t ，如果找不到长度小于c t 的线性时态逻辑公式万的反例，那么系统 模型满足公式万，记作m i - 8 ，这个自然数称为完备性阂值c t ( c o m p l e t e n e s s t h r e s h o l d ) 。完备性阈值的计算是很困难的，有时候计算出来的值是巨大的。本 文讨论了系统模型的表示，提出系统关键变量和等价简化模型的概念，通过寻找 非系统关键变量来合并系统状态，得到等价简化模型。在这个模型上计算完备性 阈值，提高了计算的效率同时得到简化模型的缩小的完备性阈值。本文实现了基 于深度优先搜索的算法来计算可达性递归直径，修正了以往算法存在的对同一状 态可能重复计算的缺点。最后通过实验分别对本文算法和模型简化策略进行测 试，结果表明：本文算法计算出的可达递归直径是正确的而且在递归直径大于 4 0 的时候开始表现出好于以往算法的效果；采用本文方法构造出优先队列模型 的等价简化模型，计算其递归直径更加直观，而且保证了简化模型同样满足验证 性质。本文的方法可应用于有界模型检测器的实现以提高其有效性。 关键词：有界模型检测、完备性阀值、可达性递归直径、系统关键变量、等价简 化模型 有界模型检测完备性阈值的优化计算 a b s t r a c t t i t l e ： o p t i m a lc o m p u t a t i o no ft h ec o m p l e t e n e s st h r e s h o l df o r b o u n d e dm o d e lc h e c k i n g m a j o r ：t h e o r e t i c a lc o m p u t e rs c i e n c e n a m e ： r u i f ut a o s u p e r v is o r ：a p z h i g u oz h a n g a b s t r a c t b o u n d e dm o d e lc h e c k i n g ，o n eo ft h es y m b o l i cm o d e lc h e c k i n gt e c h n i q u e s ，i s n o r m a l l yu s e df o rd e t e c t i n gb u g si ns y s t e md e s i g n i tu s e sb o o l e a ns a t i s f i a b i l i t y s o l v e rt os o l v em o d e lc h e c k i n gp r o b l e m s ，s oi ta v o i d st h ep r o b l e mo fs t a t es p a c e e x p l o s i o nt h a to t h e rm o d e lc h e c k i n gt e c h n i q u e sa l w a y sf a c e ，b u tr u n si ne x p o n e n t t i m e h o w e v e rt h em o s ti m p o r t a n td e f i c i e n c yo fb o u n d e dm o d e lc h e c k i n gi st h a ti t c a nd i s p r o v ep r o p e r t i e s ，b u tc a n n o tp r o v ep r o p e r t i e s t h a ti st os a y , 晰t l lb o u n d e d m o d e lc h e c k i n g ，w ec a l lo n l yp r o v ef a l s i f i c a t i o nb u tc a nn o tp r o v ec o r r e c t n e s s ，s o b o u n d e dm o d e lc h e c k i n gi sap a r t i a ld e c i s i o no ri n c o m p l e t ep r o c e d u r e f o re v e r y f i n i t em o d e lma n da nm p r o p e r t y 万，t h e r ea l w a y s e x i s tan u m b e r c t ( c o m p l e t e n e s st h r e s h o l d ) ，w i t ht h i sn u m b e ri fw ec a n n o tf m dac o u n t e r e x a m p l et o 艿i nmo fl e n g t hc to rl e s s ，t h e nw ec a nc o n c l u d et h a t mi - 万i ti s a l w a y s d i f f i c u l tt oc o m p u t et h ev a l u eo fc t ，s o m e t i m e st h ev a l u eo fc ti sh u g e i nt h i s p a p e r , w ef i r s td i s c u s s e dt h ep r o b l e mo fh o w t or e p r e s e n ts y s t e mm o d e l s ，a n dt h e nw e d e f m e dt h en o t i o no fs y s t e mc r i t i c a lv a r i a b l e sa n ds i m p l i f i e de q u i v a l e n tm o d e l t h r o u g hp u t t i n gs y s t e ms t a t e st o g e t h e rb yo m i t t i n gn o n - s y s t e mc r i t i c a lv a r i a b l e s ，w e c a ng e ts i m p l i f i e de q u i v a l e n tm o d e lo ft h eo r i g i n a ls y s t e mm o d e l c o m p u t i n go nt h i s s i m p l i f i e dm o d e l ，w ec a ni m p r o v et h ee f f i c i e n c yo ft h ec o m p u t a t i o na n dg e ts m a l l e r c tv a l u e b a s e do nt h ed e p t h - f i r s ts e a r c hs t r a t e g y , w ei m p l e m e n t e do u ra l g o r i t h m f o rc o m p u t i n gt h er e a c h a b l er e c u r r e n td i a m e t e r ( a nu p p e rb o u n do fc t ) o ft h e s y s t e mm o d e l s o u ra l g o r i t h mc a na v o i dt h ed e f e c to fr e v i s i t i n gs y s t e ms t a t e st h a t p r e v i o u sa l g o r i t h m sh a d t l l i st h e s i se n d e d 、j l ，i t l le x p e r i m e n t st e s t 吨o u ra l g o r i t h ma n d 有界模型检测完备性阈值的优化计算 a b s t r a c t m o d e lr e d u c t i o ns t r a t e g yr e s p e c t i v e l y t h er e s u l t ss h o w e do u ra l g o r i t h mc a ng e n e r a t e r i g h tr e a c h a b l e r e c u r r e n td i a m e t e ra n do u r a l g o r i t h mo u t p e r f o r m e dp r e v i o u s a l g o r i t h m sw h e nt h er e c u r r e n td i a m e t e rw a sl a r g e rt h a n4 0 c o m p u t i n go nt h e s i m p l i f i e de q u i v a l e n tm o d e lo ft h ep r i o r i t yq u e u em o d e lw ec o n s t r u c t e d ，w ec a i lg e t i t sr e c u r r e n td i a m e t e re a s i e ra n dr e t a i nt h ec o r r e c t n e s so fi t sp r o p e r t y o u rc o n c l u s i o n s c a nb ea p p l i e dt ot h e i m p l e m e n t a t i o no fb o u n d e dm o d e lc h e c k e rt oi m p r o v ei t s e f f e c t i v e n e s s k e yw o r d s ：b o u n d e d m o d e l c h e c k i n g ，c o m p l e t e n e s st h r e s h o l d , r e a c h a b l e r e c u r r e n c ed i a m e t e r , s y s t e mc r i t i c a lv a r i a b l e s ，s i m p l i f i e de q u i v a l e n tm o d e l m 论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论 文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文 韵研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本 人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：囱婆武 e l 期：丝鲤垒耳垄旦 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即：学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版，有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆、院系资料室被查阅，有权将学位论文的内容编入 有关数据库进行检索，可以采用复印、缩印或其他方法保存学位论文。 学位论文作者签名：俏磷誉 日期：沙i o 年6 月7 e l 有界模型检测完备性阑值的优化计算 第1 章引言 1 1 研究背景 第1 章引言 模型检测【l 】 2 】这个概念是为了解决并发程序验证【1 4 】这一类重要的问题而 提出来的。由于并发程序特有的并发交错执行的特点，这类程序的并发错误就很 难重复再现，使用常规的程序测试的方法找出这种类型错误的难度就特别的大。 从模型检测这个概念在1 9 8 1 年首次被提出到现在，它的发展大致经历了下面四 个重要阶段： ( 1 ) 1 9 8 1 年e d m u n dm c l a r k e 和他的博士生a l l e ne m e r s o n 在【2 0 】中首次 提出模型检测【2 】的概念，它是一种形式化的检验有限状态并行系统的自动验证 技术。在模型检测中，把受验证的系统抽象成一个有限状态机，用时态逻辑公式 表示要验证的性质，遍历有限状态机的可达性状态空间，计算这些状态是否满足 时态逻辑公式。我们称这个阶段为模型检测的萌芽阶段。 ( 2 ) 最初的模型检钡l j 2 0 称为清晰状态的模型检测( e x p l i c i t - s t a t em o d e l c h e c k i n g ) ，这种方法明确列举出系统的每一个可达性状态来检验给定的验证性 质在这些状态上是否满足。由于系统状态的数量会随状态变量的大小呈指数增长 ( 这种现象称为状态空间爆炸) ，这种模型检测算法很快表现出它的局限性，它 只能用于状态数量不超过百万的小型系统，对于工业级的系统则无能为力。这个 阶段我们称为初期发展阶段。 ( 3 ) 1 9 9 2 年j r b u t c h 和e m c l a r k e 提出了符号化模型检测【3 】f 2 1 】 ( s y m b o l i cm o d e lc h e c k i n g ) ，这种方法把多个状态组成的集合隐式的表示成布 尔函数，并使用二叉决策图( b d d ) 【4 】来表示和操作布尔函数，模型检测能够验 证的系统状态规模扩展到了1 0 2 0 ，之后大量的实际系统第一次能够得到验证。然 而布尔函数也会随模型和性质呈指数增长，这种方法也存在一个瓶颈：需要很大 的内存空间来存放和管理b d d 结构，而且需要人为的对变量序进行选择，甚至有 的时候并不存在好的变量序。近年来对于这些问题的研究很多，但仍然无法对 状态规模特别大的系统进行完全彻底的验证。我们称这个阶段为逐渐成熟阶段。 有界模型检测完备性阈值的优化计算第1 章引言 ( 4 ) 1 9 9 9 年a r m i nb i e r e 等人首次提出了有界模型检测【6 】的概念，有界模 型检测也是一种符号化模型检测技术，这种技术不使用状态空间的概念，而是将 系统模型和将要验证的时态逻辑公式转换成一个大的合取范式，使用可满足性问 题求解器( s a ts o l v e r ) 代替b d d 结构，用s a t 求解器求解这个大的合取范式的 可满足性。s a t 没有b d d 的状态空间爆炸问题，然而s a t 问题是第一个证明了 的n p 完全问题，求解的时间复杂度很高，近年来在s a t 求解效率上的研究很多， 并且取得了很大的进展，一些高效率的算法不断提出，这为有界模型检测使用 s a t 进行求解带来了可能，有界模型检测也借助于s a t 的快速发展而不断发展。 这个阶段称为模型检测的新发展阶段。 有界模型检测 6 】是一种基于可满足性决策过程的符号化模型检测技术，它 主要用来检测系统的设计缺陷。有界模型检测的主要思想是：对于给定的有限状 态转移系统m ，线性时态逻辑公式厂和一个自然数k ，计算m 中是否存在一条 长度不大于k 的转移路径使得时态逻辑公式厂不成立，这样的路径称为厂的一个 反例路径。 1 5 给出有界模型检测的主要过程： ( a ) 把受验证的系统构造成有限状态转移系统m ，要验证的性质表示成线性 时态逻辑公式厂，并设定一个自然数k ； ( b ) 然后将m 的转移关系和厂的否定式进行逻辑与运算构成有界模型检测的 转换公式： ( c ) 把这个转换公式编码成可满足性问题实例，交由可满足性问题求解器进行 计算。 有界模型检测是一个迭代执行的过程 7 】，k 一般从零开始不断增加1 直到： ( 1 ) 检验发现错误。( 2 ) l h - j 题变得太复杂，生成的合取范式s a t 无法在有限的 资源内得到求解。( 3 ) 计算超过了预设的最大的k 值。有界模型检测的主要优势在 于：充分利用s a t 工具，能很快找到反例提高模型检测的效率；它找到的反例 是长度最短、最简明的反例，有利于用户更好的理解生成的反例以改正系统存在 的错误；有界模型检测没有基于b d d 数据结构的模型检测技术的状态空间爆炸 问题，也不需要人工设定逻辑公式中的变量顺序来减少逻辑公式对应的b d d 结 构的存储空间、检测变量等问题。【2 2 】的实验表明当验证上界k 小于6 0 时，有界 2 有界模型检测完备性阈值的优化计算第1 章引言 模型检测优于传统模型检测技术。然后，有界模型检测也存在着它明显的不足之 处，它只能验证系统不满足某一性质，而无法验证系统满足某一性质，即只能证 伪而无法证实，也就是说有界模型检测是不完全的或者说是不完备的。 有界模型检测作为模型检测研究的最新技术，已经成为一个研究的热点。 1 5 】 指出有界模型检测研究的主要问题是如何提高检测的性能。根据有界模型检测的 执行过程，要提高有界模型检测的性能就要对b m c 的转换公式进行优化、编码 【8 】成s a t 实例时对其变量和子句进行优化、定制并优化s a t 求解器，提高s a t 求解器效率。总的来说就是要生成尽可能少的变量和子句，句子结构尽可能地简 单，以方便求解。有界模型检测过程中7 0 - 8 0 的时间用于产生转换公式，所 以在提高效率方面最主要的方法还是采用把有界模型检测转换公式转化为逻辑 等价而结构简单、易于实现的有界模型检测公式，这样的公式在以后进行编码时， 可直接生成变量和字句数量都较少而且易求解的s a t 实例，从而更大幅度的提 高有界模型检测的效率。有界模型检测的另一个重要问题是研究k 值的上界，使 得当k 达到这个上界时如果还没有发现反例存在，那么受验证系统就满足验证的 性质。这个上界称作完备性阈值 9 ( c o m p l e t e n e s st h r e s h o l d ) 记作c t 。对于给定 的系统m 和l 1 几性质厂，c t 是满足公式mi 盯一ml - f 的最小自然数，其 中m i = c rf 是指m 中任何长度不大于c t 的路径都使得厂成立。很显然，如果 有m | _ 厂，那么最小的c t 值等于0 ，否则c t 等于最短的反例路径的长度，由 此可以看出，计算最小的c t 值至少和验证m 是否满足性质厂一样难。【1 7 】指出 完备性阈值c t 的大小与模型m 、时态逻辑公式厂( 厂的构造和它所包含的原子 命题) 以及将m 和厂转换成命题公式的转换方法有关。要使有界模型检测完备 化，就必须计算出完备性阈值，否则我们就无法判断时态逻辑公式厂在m 上是 已经满足还是预设的k 值的最大值还没有达到足够大的值。然而目前在这方面的 研究却很少。采用基于句法的转换方法，我们只能知道时态逻辑公式g 厂和巧的 c t 值，对于一般的时态逻辑公式，计算c t 值仍是一个没有解决的问题。【7 】中 c l a r k e 等人提出了通过计算由受验证系统和与时态逻辑性质等价的自动机构造 的系统的递归直径 9 】来计算完备性阈值c t ； 1 6 】中a w e d h 和s o m e n z i 对这种计 3 有界模型检测完备性阈值的优化计算第1 章引言 算方法进行了优化。这种方法在实现时采用清晰完整的自动机表示；【1 7 q bk e i j o h e l j a n k o 等人采用了模型增量的方法，并且对自动机进行了等价简化；【1 1 q b d a n i e lk r o e n i n g 等人根据硬件电路的局部化原理，对设计进行分割，然后分别计 算各个模块的c t 值，再计算整个设计的c t 值。上面提到的方法都涉及到模型 转换方法，在计算c t 值时比较复杂。 1 2 问题陈述 在第一节里我们提到了有界模型检测完备性阈值的概念，我们知道对于一个 有限状态的系统或者模型，它都存在一个边界，这个边界完全涵盖了整个系统或 模型，在这个边界内的系统都有一个尺寸来衡量这个系统的大小，完备性阈值就 是这样的一个尺寸。我们这篇论文主要是讨论的如何计算完备性阈值的问题。 1 目前c t 计算方法存在的问题 目前有界模型检测的研究主要集中在如何提高效率方面，对于有界模型检测 完备性方面的研究比较少。已有的一些研究如【9 】首次提出了有界模型检测完备 性阈值的概念，给出了计算完备性阈值的几个上界值；【7 】通过将验证系统和时 态逻辑公式转换成b u c h i 自动机来计算系统的递归直径，这个递归直径是c t 的 一个上界。【1 6 】采用了与【7 】相同的方法并对这种方法进行了优化。这几种方法都 考虑模型及编码问题，计算复杂性都比较高，实现起来难度也比较大。还有一些 研究如【1 1 】和【1 7 】分别从硬件电路的结构和增量式有界模型检测模型编码方面考 虑从而达到完备化的有界模型检测。现有的方法通常不能找到计算一般性时态逻 辑公式的c t 值，或者计算时的复杂度过高，通用而有效的计算c t 值的方法还 有待发现。 2 论文的目的 本文主要是在【9 】 7 】和 1 8 】的基础上进行的，本文根据 7 】和【1 8 】介绍的有界模 型检测的编码方法对【9 】提到的变量约减方法进行总结与扩展，提出系统关键变 量和极小等级简化模型的概念，通过状态合并的方法来减小系统的状态规模，达 到提高计算c t 效率的目的，本文给出了基于深度优先搜索的算法来计算c t 上 界，我们的算法避免了已有算法可能对状态重复计算的缺点，最后通过实验表明 4 有界模型检测完备性阈值的优化计算第1 章引言 本文算法的正确性和简化策略的有效性。 3 论文的假设 有界模型检测的编码方法有很多种，本文只介绍基于句法的编码方法和基于 语义的编码方法，其他的很多方法都是在这两种方法的基础上进行改进的，以提高 编码效率。本文在计算完备性阈值的时候计算的是它的一个上界值，应用抽象的 状态图作为实验模型，在这个模型上忽略状态转移时的标签函数，因为标签函数 对我们计算完备性阈值不产生影响，忽略它可以简化我们的计算。系统状态的表 示假设为一个变量赋值序列，这些变量的取值都有一定的范围，一般取0 和1 ， 我们只用状态的序号来标记状态，本文我们采用基于语义的有界模型检测编码方 法，在计算完备性阈值的时候我们假设将系统模型和线性时态逻辑性质表示成一 个抽象的简化状态图形式，我们的计算就是在这个状态图上进行的，这样整个问 题就变成了图论上的计算问题，最后我们借用图的算法来求解完备性阈值的上 界。在本文的模型简化策略方面；我们寻找那些显而易见的非系统关键变量，通 过忽略这些非系统关键变量由于赋值不同而造成的冗余状态，达到合并状态简化 系统模型的目的，本文的实验采用手工的方法对状态进行合并，得到等价简化模 型，然后再拿这个简化模型来计算递归直径。 4 计算方法的基本思路及预期目标 本文考虑基于语义的编码方法，将受验证模型和时态逻辑性质转换成状态 图，通过状态合并，得到一个简化的状态图模型，使用本文介绍的基于深度优先 搜索的算法对这个简化的状态图模型进行搜索，计算出缩小的完备性阈值，在实 验部分我们首先对规模在1 - - 1 0 0 的十个抽象的状态图模型进行测试，验证我们 算法的正确性和效率，然后我们用一个优先队列的模型来测试本文介绍的模型简 化策略的有效性和正确性。 1 3 立题意义 在理论计算科学中，模型检测 2 0 】是提出比较晚的一个概念，自1 9 8 1 年提 出以来已经有了很大的发展，然而模型检测一直面临着状态空间爆炸的问题，这 大大阻碍了模型检测技术在实际系统中的使用，基于a d d 4 数据结构的符号化 有界模型检测完备性阈值的优化计算 第1 章引言 模型检测技术的提出大大扩展了模型检测可解决的系统规模，然而由于b d d 结 构很容易急速增大，系统存储空间很快消耗完毕，状态空间爆炸的问题仍然没有 彻底解决，基于可满足性问题求解器 2 3 】的符号化模型检测，即有界模型检测， 不使用状态空间搜索的方法，它把受验证系统和规范逻辑性质转换成命题公式， 利用可满足性问题求解器对这个命题公式进行求解，这种模型检测方法没有状态 空间爆炸的问题，然而显而易见这种模型检测方法的时间复杂度是指数级别的， 但可满足性问题求解器发展很快，已有很多好的算法能够在合理的时间内求解， 有界模型检测就有它存在的合理性了。然而如我们在前面提到的有界模型检测是 半决策化的检测过程，或者说它是不完备的模型检测技术。要使有界模型检测完 备化，我们就必须计算出完备性阈值c t ，用这个c t 值作为有界模型检测预设k 值的上界，当检测超过c t 时，没有发现系统有违法性质的反例存在，就说明系 统满足性质，这样在检测结束时就能给出系统满足性质的结果。可见，计算出完 备性阈值c t 对有界模型检测的完备化有重要意义。目前的一些计算方法大多计 算效率不高，而且计算出的完备性阈值过大而无实际意义，本文主要讨论如何提 高计算完备性阈值的效率，以及如何计算出较小的完备性阈值。 本文在已有 7 1 1 9 1 计算有界模型检测完备性阈值方法的基础上，提出了一 种简化的计算方法，这种方法能够缩减系统状态变量，从而使系统规模变小，得 到一个较之原模型相对简化的模型，在新的模型上计算完备性阈值不仅能够更容 易计算，而且计算出的完备性阈值更小，利用这个值作为有界模型检测k 值的上 界，我们就能够得到完备化的有界模型检测器。 1 4 论文组织结构 本文正文部分共分为六章，各章的主要内容为 第一章，引言。介绍论文的研究背景，提出本论文要研究的问题和研究本课 题的意义。 第二章，介绍与有界模型检测相关的基本概念，包括线性时态逻辑，有限状 态转移系统，有界模型检测的语义以及如何将有界模型检测转换成可满足性问 题，以及有界模型检测使用的s a t 求解器； 6 有界模型检测完备性阈值的优化计算 第1 章引言 第三章，在有界模型检测的完备性阂值形式化定义的基础上，讨论已有的计 算完备性阈值方法，并给出计算完备性阈值的优化计算方法，定义系统关键变量 和极小等价简化模型，给出三类非系统关键变量，并讨论如何得到等价简化模型。 第四章，讨论基于深度优先搜索的计算完备性阈值算法，对算法的实现及性 能进行详细分析。 第五章，用实验对本文介绍的模型简化策略和实现的算法进行测试 第六章，对本文介绍的方法和实验进行总结，并讨论进一步的研究工作。 7 有界模型检测完备性阈值的优化计算 第2 章有界模型检测 第2 章有界模型检测 有界模型检测 6 】是增加了边界限制的模型检测技术，它本质上是一个搜索 算法，这种算法在线性时态逻辑公式的约束下，在受验证系统模型中搜索一条长 度不超过预设的k 值的违反规范约束的反例路径。有界模型检测的主要过程【1 5 】 是：首先，把受验证的系统或模型构造为有限状态机f s m ( f i n i t es t a t em a c h i n e ) ， 通过f s m 状态间的转移来模拟受验证系统或模型的运行情况；然后，用线性时 态逻辑语言l 1 亿( 1 i n e a r - t i m et e m p o r a ll o g i c ) 描述要验证的规范性质；设定一个 自然数k 的上界值，比如6 0 、1 0 0 或更大的数；把f s m 状态间的转移关系和由 l t l 公式转化出的否定范式n n f ( n e g a t i o nn o r m a lf o r m ) 通过逻辑与运算构成有 界模型检测的逻辑转换公式；把有界模型检测的逻辑转换公式编码成可满足性问 题s a t 的实例，使用s a t 求解器求解；如果有解，就找到了一个反例；反之， 如果s a t 实例不可满足，则表明受验证的系统或模型运行到k 阶段时是安全的、 没有错误的。图2 1 描述了有界模型检测执行的流程。图中的符号c t 表示模型m 检验性质矽时的完备性阈值，根据完备性阈值的定义，在验证过程中，如果k 值 超过c t 值时仍然有ml - 。，我们就可以得出ml - 的结论，否则当k 为小于 c t 的某个自然数时有ml 。我们就找到了m 不满足性质的一个反例。 图2 - 1 有界模型检测的过程 8 m l f m l = f 有界模型检测完备性阈值的优化计算第2 章有畀模型检测 2 1 基本概念 给出一个系统或模型，一个规范性质，模型检测验证这条规范性质在这个系 统或模型上的满足情况。那么如何去表达系统，又如何去描述规范性质呢? 本节 分两个部分对规范性质的描述方法和系统的表示进行介绍，他们是模型检测，也 是有界模型检测的基础概念，最后给出一个例子来更好的表述这两个概念。 1 时态逻辑 用时态逻辑来描述要验证的规范性质，这也是有界模型检测过程中第一步要 做的事情。时态逻辑( t e m p o r a ll o g i c ) ，是对模态逻辑的扩展，它涉及含有时间 信息的状态、事件及其关系的谓词、命题和演算，这些时间信息包括：现在、过 去、将来、之前、之后等时间。 时态逻辑对谓词逻辑进行了扩充，增加了时序上的操作，这里的时序概念指 的是系统状态序列。线性时态逻辑把系统的状态序列处理成线性结构，它仅考虑 现在和将来的时间序列而不考虑过去的时间序列，比较适合于并发程序的描述与 验证。标准的命题线性时态逻辑( p l t l ，p r o p o s i t i o n a ll i n e a rt e m p o r a ll o g i c ) 是由原 子命题、布尔连接符和常用的线性操作符组成的，简称为线性时态逻辑l t l 。 定义2 - 1 ( 命题线性时态逻辑) 设原子命题的集合为彳尸，其中矽a p ，l t l 公式的语法定义如下：。 1 若矽a p ，则汐是l t l 公式 2 ，若缈和是l 1 几公式，则1 矽，矽人矽，矽v 妒，矽一，g 妒，却，蜘， 矽脚，嬲矿等都是l 1 凡公式 2 中的符号x ，g ，u ，r 分别表示下一个( n e x t ) ，全部( g l o b a l ) ，最终 ( e v e n t u a l l y ) ，直到都( u n t i l ) ，直到才( r e l e a s e ) 等模态词；1 ， ，v ，专 等符号为逻辑连接词。本文讨论的规范性质就是采用这种定义的命题线性时态逻 辑来表示的。在进行验证的时候要将l 1 吼公式转换成n n f 的形式。 2 有限状态转移系统 有界模型检测验证的系统都是有限状态系统，通常将有限状态系统表示成克 9 有界模型检测完备性阈值的优化计算第2 章有界模型检测 里普克( k r i p k e ) 结构。 定义2 2 ( k r i p k e 结构) 是一个四元组m = p ，i ，t ，三) ，其中s 表示状态 集，i s 表示初始状态集，t s x s 表示转移关系，l ：s + 专p ( a ) 是标签函数， 其中a 是原子命题的集合，p ( a ) 是彳的超集。标签函数是对系统状态的一种跟 踪观察机制：对一个状态s s ，三( j ) 表示那些在状态s 上为真的原子命题集合。 定义2 - 3 ( 路径) 有界模型检测的路径用符号万表示，万= g 。，s 2 ，s ，) ，其中s s ，f n 我们用万( f ) = s 表示路径中第f 个状态，用万= g ，s ，+ ，s m 。) 表示路径从状态 f 开始的后缀状态序列。 定义2 - 4 ( l t l 模型检测语义) 设m 为一k r i p k e 结构，万为m 的一条路 径，厂为l 1 几公式，则万| - 厂如下定义： 万| _ p i f f p e l ( z t ( o ) ) 万卜呻 i f f p 仨三( 万( o ) ) 石i _ 厂 g i f f 万i - 厂且万i - gn l = f vg i f f 万i - 厂或万i - g 万| _ 可 i f f v i ，万，l - 厂万i - j 歹 i f f 3 i ，万，i - 厂 万i _ 可 i f f万1 i - 厂 万l - 唿 i f f 3 i ，刀i _ g 且，_ ， f ，万7 i = s 万i - 歹醣 i f f v f ，万1 g 或影，j i ，万i _ 定义2 - 5 ( 有效性) 一个l t l 公式厂在一个k r i p k e 结构m 上全局有效 ( u n i v e r s a l l yv a l i d ) 表示成mi - ，当且仅当m 中的所有路径万使得万l - f 并 且万( 0 ) ，；一个l 1 l 公式厂在一个k r i p k e 结构m 上局部有效( e x i s t e n t i a l l y v a l i d ) 表示成mi - e f ，当且仅当m 中至少存在一条路径万使得7 h - f 并且 万( 0 ) ， 从定义2 - 5 可以看出一个l t l 公式厂在一个k r i p k e 结构m 上全局有效当且 l o 有界模型检测完备性阈值的优化计算第2 章有界模型检测 仅当1 厂在m 上不是局部有效的。通常，我们取公式厂的否定式，通过验证了在 m 上不是局部有效的来求解全局性问题。直观上说，我们在m 中找的反例， 如果没有找到公式的反例这就说明厂在m 上是全局有效的。在模型检测中， 我们通常只考虑局部性问题。 3 两位计数器的例子 考虑两位计数器的例子，它的模型代码如下： 这个有限状态转移系统的状态由变量b o 和b 1 表示，b o 和b 1 都是布尔类型， 它们的值可以用0 表示假，1 表示真。这样两位计数器的状态空间就是4 ，表示 成状态集s = o o ，0 1 ，1 0 , 11 ) 。状态转移关系表示成比特串的形式如下： 0 0 0 1 ，0 1 1 0 ，1 0 1 1 ，1 1 0 0 用k r i p k e 结构的形式表示成图，如图2 2 所示。初始状态0 有一条无源的入 边，其他的箭头表示上面的四个转移关系。 图2 2 两位计数器状态转移图 有界模型检测完备性阈值的优化计算第2 章有界模型检测 在这个例子中，状态集s = s 0 ，s l ，s 2 ，s 3 ，初始状态集i - s 0 ，转移关系 t = ( s 0 ，s 1 ) ，( s l ，s 2 ) ，( s 2 ，s 3 ) ，( s 3 ，s o ) ) ，设原子命题集a 只含有一个原子命 题p ：b 0 = l & b l = l ，设线性时态逻辑性质厂为印，则模型中路径 万：0j1 专2 专3 就是满足性质厂的路径，因为在状态3 上b o 和b 1 都为1 。 有了本节的基本概念，后面的几节对有界模型检测的基本原理进行介绍，包 括有界模型检测的语义、如何转换成可满足性问题以及可满足性问题求解器，本 节重点介绍两种有界模型检测的转换方法：基于句法的转换方法和基于语义的转 换方法，他们是有界模型检测的重点，对计算完备性阈值同样有重要意义。 2 2 有界模型检测的语义 有界模型检n 5 1 是把可满足性问题求解器s a t e 2 3 应用于模型检测的一种 新的模型检测技术。s a t 求解器在求解布尔函数方面有很高的效率，近年来s a t 求解器有很大的发展，目前它已经可以解决含有数十万个变量和百万条子句的实 例( 在本节第三部分我们将详细介绍s a r ) ，这大大超过了基于b d d 结构的模 型检测的可检测系统规模，而且用s a t 求解省去了用以表示b d d 结构的存储空 间，没有了状态空间爆炸的问题。 有界模型检测的主要思想我们在第一章已经提到，就是在模型m 中搜索一 条状态数量受限的前缀路径7 使得规范性质厂的否定式无效。虽然我们搜索的是 一条状态有限的前缀路径，考虑到含回路的路径，它仍可以表示无限长的路径。 图2 3 和图2 4 分别描述了一条无回路和有回路的状态路径。无回路的有限路径 无法说明任何无限长路径的性质，如图2 3 所示的路径无法说明状态之后的性 质，图2 4 在状态& 之后有一条指向的回路，它可以表示如6 汐这样具有无限 特点的性质。 1 2 有界模型检测完备性阈值的优化计算第2 章有界模型检测 图2 3 无环路径 图2 4 带环路径 定义2 - 6 ( 环路) 对于自然数，和后，如果，七，称路径万是一个( 忌，) 环路， 仅当丁仂( 后) ，万( 功并且万= u ，口，其中1 4 = ( 刀( o ) ，万( ，一1 ) ) 且v = 仞( 班一，万( 后) ) 。 ，口表示对v 的无限循环。称刀是一个七环路，仅当存在k ，艺0 使得万是一个( j j ，) 环路。 我们使用k 环路这个概念来定义有界模型检测的语义，在有界模型检测中， 我们只考虑路径的有限前缀，因此我们只使用路径的前k + 1 个状态( ，s k ) 来 验证m 性质的有效性。如果路径刀是一个后环路，有界模型检测的语义同一般 m 模型检测的语义一样，这是因为这条路径的前缀状态已经包含这条路径所有 的信息。 定义2 7 ( 含环路的有界模型检测语义) 令自然数七0 并且万是一个k 环 路，一个m 公式厂在界值为七的路径x _ t z 有效( 记作z r l = 。f ) ，当且仅当y l _ f 。 下面我们考虑石不含环路的情况。u l 公式厂= f p 在路径万上有效，仅当我 们能够找到某个数，0 使得在路径万的后缀万上有效。在有界模型检测中的 状态后+ 1 是最后一个状态，我们无法递归的定义路径万的后缀万，为了解决这 个问题我们引入万l _ ：f 的表示方法，其中f 表示当前状态的序号，它表示在路 径万的后缀万上有效。下面给出不含环路的情况下有界模型检测的语义。 定义2 8 ( 不含环路的有界模型检测语义) 令自然数k o 并且万不是一个 后环路，一个l 1 凡公式在界值为七的路径万上有效( 记作万l - 。f ) ，当且仅当 1 3 有界模型检测完备性阈值的优化计算 第2 章有界模型检测 万| = ：f ，其中： 万i - ：p i f f p l q r ( i ) )叫= ：叩i f f p 叠三( 万( f ) ) 万| ：厂 g i f f 万i ：且万i _ ：g 万j _ ：v g i f f 叫= ：或石l - ：g叫= ：何 总为假 万| - ：矽 i f f 可，f 歹j j 刀i _ ：厂 万| ：矽 i f f i k 且万一- - “k1 厂 万| _ ：他 i f f 玑i j k a r l ： g 且v 刀，f 刀 _ ，刀l _ ：厂 万i - 傀 i f f 影，f ，j i 叫= f 厂且v 刀，f 珂 弦| ：g 注意定义2 - 8 中，如果刀不是一个k 环路，定义够恒为假，因为厂可能在路 径万川上无效。这意味着，在有界模型检测中等价式1 方羞g 可不再成立。 引理2 - 1 令厂是一个l t l 公式，万是一条任意路径，则万i _ 。厂j 万l - f 引理2 - 2 令厂是一个m 公式，m 是一个k r i p k e 结构。如果ml - e f ，那么 存在某个数k o 使得ml - 。e f 定理2 - 1 令是一个l t l 公式，m 是一个k r i p k e 结构。mi - e f 当且仅 当存在某个数k o 使得mi _ 。e f 定理2 】是我们从模型检测发展出有界模型检测技术的原理依据所在。 2 3 转换成可满足性问题 上一节中我们定义了有界模型检测的语义和重要的定理2 1 。现在我们介绍 如何将有界模型检测问题转化成可满足性问题，以使用高效的s a t 求解器来进 行模型检测。这里我们介绍两种转换方法：基于句法的转换方法和基于语义的转 换方法。 1 ) 基于句法的转换方法 1 4 有界模型检测完备性阈值的优化计算 第2 章有界模型检测 给定一个克里普克结构m 、一个l 1 l 公式和一个整数界后，我们可以构 造出命题公式0 m ，卅l 。命题公式中的变量，s 。表示路径万上的一个有限的状 态的序列，每一个变量一是由状态变量表示成的向量赋值。命题公式0 m ，刀l 实 际上是对状态的一个约束，公式0 m ，卅l 是可满足的，当且仅当时态性质在路 径7 上有效。 共享公共子公式后，公式0 m ，州l 的规模与厂的规模呈正线性关系，与k 呈 平方关系，与转移关系r ，初始状态集，以及原子命题的大小呈线性关系，如此， 有界模型检测问题可以在线性时间内转化成命题的可满足性问题。 下面来构造公式0 m ，卅l ，首先定义由模型m 约束的有效路径石的公式 0 m m ，然后再给出由l t l 公式约束的能够满足性质f 的路径刀的命题公式。 定义2 - 9 ( 展开转移关系) 对于一个克里普克结构m ，k n 0 m i l 每i ( s o ) 入k - i r ( i = 0 根据一条路径在长度k 内有无环路，有两种对应的时态公式的转换方法。 下面的定义2 1 0 给出无环的转换方式，0 1 蔓表示无环路的情况。定义2 1 2 给出 有环的转换方式，0 i 蔓表示有环路的情况。 定义2 1 0 ( 无环的l t l 转换公式) 对于一个m 公式厂和整数界后，f n 且i k 呲：一p o ，) 0 厂 g 吸# 0 9 i 翼 0 酬丘净总为假 0 -