中文模板

Size: px

Start display at page:

Download "中文模板"

懿赵
1 years ago
Views:

1 ISSN -9825, CODEN RUXUEW E-ma: Journa of Software, Vo.2, No.8, August 29, pp do:.3724/sp.j Te/Fax: by Insttute of Software, the Chnese Academy of Scences. A rghts reserved. 有界模型检测的优化杨晋吉,2+, 苏开乐 3, 骆翔宇 4, 林瀚 2 2, 肖茵茵 ( 华南师范大学计算机学院, 广东广州 563) 2 ( 中山大学信息科学与技术学院, 广东广州 5275) 3 ( 北京大学信息科学技术学院, 北京 87) 4 ( 桂林电子科技大学计算机与控制学院, 广西桂林 544) Optmzaton of Bounded Mode Checng YANG Jn-J,2+, SU Ka-Le 3, LUO Xang-Yu 4, LIN Han 2, XIAO Yn-Yn 2 (Schoo of Computer, South Chna Norma Unversty, Guangzhou 563, Chna) 2 (Schoo of Informaton Scence and Technoogy, Sun Yat-Sen Unversty, Guangzhou 5275, Chna) 3 (Schoo of Eectroncs Engneerng and Computer Scence, Peng Unversty, Beng 87, Chna) 4 (Coege of Computer and Contro, Gun Unversty of Eectronc Technoogy, Gun 544, Chna) + Correspondng author: E-ma: yang@scnu.edu.cn Yang JJ, Su KL, Luo XY, Ln H, Xao YY. Optmzaton of bounded mode checng. Journa of Software, 29,2(8): Abstract: Ths paper optmzes the encodng of verfyng G(p) and G(p F(q)) whch are two mportant and frequenty used moda operators n optmzaton of encodng for bounded mode checng (BMC). Through anayss of the propertes of fnte state machne (FSM) and LTL (near-tme tempora ogc) when verfyng these moda operators, t presents a concse recursve formua, whch can effcenty transate BMC nstances nto SAT (satsfabty) nstances. The ogca propertes of these recurson formuas are verfed. The expermenta comparson between the optmzaton of BMC and the other two mportant methods AA_BMC and Tmo_BMC for sovng these moda operators n BMC shows that the former s superor to the atter n both the scae of nstances and the dffcuty to sove the probem. Research of ths paper s aso benefca to encodng optmzaton of verfyng other moda operators n BMC. Key words: mode checng; bounded mode checng; SAT (satsfabty); moda operator; recurson formua 摘要 : G(p) 和 G(p F(q)) 是有界模型检测 (bounded mode checng, 简称 BMC) 中的两个重要的常用模态算子. 对验证 G(p) 和 G(p F(q)) 编码转换公式进行优化. 通过分析当验证这些模态算子时 FSM(fnte state machne) 的状态转移和线性时序逻辑 (near-tme tempora ogc, 简称 LTL) 的语义特征. 在现有的编码公式的基础上, 给出了简 Supported by the Outstandng Young Research Fund of Chna under Grant No ( 国家杰出青年基金 ); the Natona Natura Scence Foundaton of Chna under Grant Nos.64734, ( 国家自然科学基金 ); the Guangdong Provnca Natura Scence Foundaton of Chna under Grant No ( 广东省自然科学基金 ), the Guangdong Provnca Research Foundaton of Scence and Technoogy of Chna under Grant No.27B468 ( 广东省科技攻关项目 ) Receved ; Revsed 28-2-; Accepted

2 26 Journa of Software 软件学报 Vo.2, No.8, August 29 洁高效的递推公式, 该公式有利于高效编码成 SAT(satsfabty) 实例 ; 证明了递推公式和原转换公式的逻辑关系. 通过实验比较分析, 在生成 SAT 实例规模和易求解方面都优于 BMC 中求解这些模态算子的现有的两种重要方法 AA_BMC 和 Tmo_BMC. 所给出的方法和思想对于 BMC 中验证其他模态算子时的编码优化也有参考价值. 关键词 : 模型检测 ; 有界模型检测 ; 可满足性问题 ; 模态算子 ; 递推公式中图法分类号 : TP3 文献标识码 : A 模型检测 (mode checng) [] 是一种以形式化方式构造系统的模拟运行过程, 自动检测是否满足某些期望规范的一种新兴技术. 随着计算机系统越来越复杂, 网络应用越来越普及和重要, 通过模型检测技术来验证系统和网络的安全性和正确性的应用也逐渐增多. 有界模型检测 (bounded mode checng, 简称 BMC) [2,3] 是针对前期的 OBDD(ordered bnary decson dagram) 技术的模型检测的不足, 如状态空间爆炸需要人工设定逻辑公式中的变量顺序才可有效减少逻辑公式相对应的 BDD(bnary decson dagram) 结构的存储空间检测变量少等问题而产生的一种新的模型检测技术. 其优势之一是把 BMC 问题编码成 SAT(satsfabty) 实例, 充分利用 SAT 工具进行求解, 较好地弥补了上述的不足, 使可以验证的变量数提升一个数量级以上 ; 另一优势是由于采用宽度优先搜索, 所获得的反例是长度最短最简明的反例, 有利于设计者理解问题, 找出原因. 当实验验证边界上界小于 6 时,BMC 要优于传统的模型检测 [4]. 近年来, 已出现一些有界模型检测的实际应用 [5,6]. 有界模型检测的主要过程是 : 先把要验证的系统或模型构造为有限状态自动机 (fnte state machne, 简称 FSM), 通过 FSM 状态间的转移来模拟系统或模型运行 ; 要验证的规范说明用时序逻辑 LTL(near-tme tempora ogc) 进行说明 ( 如 G(p),F(p)); 设定边界上界 K;FSM 状态间的转移关系和 LTL 逻辑规范否定的 NNF(negaton norma form) 公式通过逻辑与构成 BMC 转换公式 ; 把 BMC 转换公式编码成 SAT 实例, 通过 SAT 工具求解. 若有解, 则找到反例 ; 反之, 若不可满足, 则表明要验证的系统或模型运行到 K 阶段时, 是安全的没有错误的. 近年来, 有界模型检测成为一个研究热点, 围绕 BMC 的许多问题, 每年有专门的 BMC 国际会议. 目前, 主要在 3 个方面提高 BMC 性能. 其一在于对 BMC 的转换公式优化 [7 9] ; 其二是编码成 SAT 实例时, 对其变量和子句的优化 [,] ; 其三是针对 BMC 问题映射成 SAT 实例后, 针对 SAT 子句的特点, 优化 SAT 工具, 提高 SAT 求解效率 [2]. 前两种方法都是生成尽可能少的变量和子句, 句子结构尽可能地简单, 方便求解 ; 第 2 种方法在优化时破坏了 BMC 问题的特征, 若再用第 3 种方法中针对 BMC 优化的 SAT 工具, 就无法取得较好的效果, 并且有界模型检测中仅有 2%~3% 的时间用于产生 SAT 实例和求解. 第种方法是采用把 BMC 转换公式转换为逻辑等价但结构简单易于实现的 BMC 公式. 这样的公式在以后进行编码时, 可直接产生变量和子句都较少且易解的 SAT 实例, 从而提高 BMC 的效率. 本文的工作属于第种方法, 在 BMC 的 LTL 规范说明中,G(p),G(p F(q)) 是协议验证中非常重要的 LTL 的模态描述词, 如 G(p) 验证协议的保密性, 验证智能体的认知算子 [5] ;G(p F(q)) 验证协议的认证性等. 本文根据 FSM 状态间的转移关系和 G(p),G(p F(q)) 公式的语义结构, 得到与其 BMC 转换公式逻辑等价和蕴含关系的简洁高效的递推公式, 证明了递推公式和原 BMC 转换公式的逻辑关系, 分析了其相应的复杂性变化. 最后通过实验验证了本文工作的有效性. 本文第节介绍 BMC 原理及相关公式和定理. 第 2 节介绍验证 G(p),G(p Fq) 等 LTL 模态词的转换公式及其优化方法. 第 3 节介绍与本文相关的其他工作. 第 4 节通过实验与两种已有的优化方法进行比较分析. BMC 原理及相关公式和定理 BMC 要验证的规范是用线性时序逻辑 LTL 进行描述的. 本节首先介绍 LTL 逻辑的语法和语义, 其次介绍 FSM 和 LTL 规范描述构成的 BMC 转换公式及原理, 最后介绍已有的一些优化方法.. LTL 的语法及语义定义 (LTL 语法 ). 设原子命题的集合为 A,LTL 公式的语法如下定义 :

3 杨晋吉等 : 有界模型检测的优化 27. 若 ϕ A, 则 ϕ 是 LTL 公式. 2. 若 ϕ 和 φ 是 LTL 公式, 则 ϕ,ϕφ,ϕφ,ϕ φ,gϕ,fϕ,xϕ,ϕuφ,ϕrφ 等是 LTL 公式. X,G,F,U,R 分别表示下一个 (next), 全部 (goba), 最终 (eventuay), 直到全 (unt), 直到有 (reease) 等模态词 ;,,, 等符号称为连接词. 因为主要是通过 BMC 找反例, 因此 BMC 实际处理的是 LTL 规范的否定形式.LTL 规范的否定形式要表示为 NNF(negatve norma form) 形式的 LTL 公式 ( 简称 NNF 公式 ).NNF 公式是不包含连接词, 且否定词只能出现在原子命题前的 LTL 公式. 若 f 为 LTL 公式, 则 depth(f) 为 f 的深度, 即 f 中模态词的嵌套层数. 定义 2. BMC 的克里普克结构 (Krpe structure) 为一四元组 M=(S,I,T,), 其中,S 为 BMC 中 FSM 产生的所有状态集合 ;I S,I 为初时状态的集合 ;T S S,T 为状态间转移关系的集合 ;:S P(A), 为标注状态的函数. 定义 3. BMC 的路径 π=(s,s 2,s 3, ), 其中,s S, N;π()=s ;π =(s,s +,s +2, ). 定义 4 (LTL 语义 ). 设 M 为一克里普克结构,π 为 M 的一路径,f 为 LTL 公式, 则 π f 如下定义 : π p ff p (π()) π p ff p (π()) π f g ff π f 且 π g π f g ff π f 或 π g π Gf ff,π f π Ff ff,π f π Xf ff π f π f Ug ff,π g 且,<,π f π f Rg ff,π g 或,<,π f 定义 5. 布尔公式是各原子命题只通过,,, 等连接词连接, 而没有使用模态词的公式..2 BMC 转换公式及原理根据 LTL 语义, 若 M 为克里普克结构,f 为 BMC 要验证的 LTL 规范说明否定形式的 NNF 公式, 为整数边界, 则可以创建命题公式 [[ M, f ]] ( 下文称为 BMC 转换公式 ), 路径 π=(s,s,s 2,,s ) 为 [[ M, f ]] 的有限状态序列.BMC 的转换公式 [[ M, f ]] 就是对有限状态序列 s,s,s 2,,s 的约束, 使得 [[ M, f ]] 是可满足的当且仅当 f 在路径 π 中是有效的 (vad). 定义 6(BMC 转换公式 ). 设 M 为克里普克结构,f 为 BMC 要验证的 LTL 规范说明否定形式的 NNF 公式, 为整数, 则 BMC 转换公式为 [[ M, f]] = [[ M]] [[ f]] () + 和 = = = 其中 : [[ M ]] = I( s ) T( s, s ),[[ f]] = ( L [[ f]] ) ( L [[ f]] ), L = T( s, s ), L = L,[[ f]] [[ f]] 的递归定义见表的描述 ; 若 f 为布尔公式, 则 [[ f ]] 和 [[ f ]] 简写为 f 和 f. [[ M, f ]] 是初时状态为 s, 路径长度为, 且满足 f 的所有路径. 在实际中, 因为边界被提前准确计算出来难度很大 [3], 所以一般依次取, +, +2, +3,, +MAX 进行试探 ; 称为边界下界, 大多数情况下取 =; ( +MAX) 为边界上界, 一般由用户设定. 对 [[ M, f ]] 依次求解, 若找到反例或到了设定时间 ( +MAX), 则停止增加, 算法结束 ; 否则一直加取下去. 当每取一个整数时, 把 [[ M, f ]] 转换为 SAT 实例, 通过 SAT 工具对此 SAT 实例求解, 若有解, 则算法结束 ; 否则, 取 + 继续前述算法. 因为 LTL 规范 f 否定形式的 NNF 公式被编码成布尔公式 [[ M, f ]] [] 的一部分, 所以与 BDD 方法不同, 公式 f 的规模决定 [[ M, f ]] 编码成 SAT 实例的规模. 同时, 该 SAT 实例的规模与边界有关, 边界越大, 其 SAT 实例规模越大. 前述的第种方法就是对 [[ M, f ]] 的优化, 尽可能找到等价或者是可满足性等价的简化的 [[ M, f ]]

4 28 Journa of Software 软件学报 Vo.2, No.8, August 29 公式, 从而生成较小的 SAT 实例, 提高求解的效率. 如果能够确定一个理想的边界的下界值, 就可以减少调用 SAT 工具来求解的次数. Tabe Recursve defnton of [[ f ]] and 表 [[ f ]] 和 [[ f ]] 的递归定义 [[ f ]] f [[ ]] f [[ f ]] p p p p p p hg [[ h]] [[g]] [[ h]] [[ g]] hg Xg [[ h]] [[g]] + [[ g]], f <, otherwse [[ h]] [[ g]] +! [[ g]], f < [[ g]], otherwse h Gg mn(, ) [[ ]] g Fg hug hrg [[ ]] ( [[ ]] g ( [[ h]] g mn(, ) n= [[ ]] n h ) ( [[ ]] g ) n= [[ ]] n n= [[ ]] n g ) mn(, ) [[ ]] g ( [[ ]] h n= [[ ]] n [[ g ]] ( [[ g]] n= [[ ]] n h ) n= [[ ]] n h g ) ( [[ ]] h [[ g]] n [[ g ]] n ) n= n=.3 BMC 转换公式已有的一些优化这里主要介绍与本文相关的优化方法, 其他一些方法将在后文加以介绍. 文献 [7] 给出主要针对 [[ M, f ]] 式中 [[ f ]] 的一些特性, 经过逻辑推导, 得出简化的 [[ f ]] 公式的表示. 与本文相关的主要有以下几个定理 : 定理. 对于任意的 LTL 公式 f, 任意的,,, 且和, [[ f ]] [[ f ]]. 定理 2. 公式 [[ f ]] 逻辑等价于 [[ f]] ( L [[ f]] ). = f ]] = 定理 3. 如果 depth(f), 则 [[ 与无关, [[ f]] [[ f]] ( L [[ f]] ). 特殊情况下, 当 [[ f ]] = [[ f ]] 时, [[ f ]] = [[ f ]]. 上述 3 个定理的证明详见文献 [7]. 2 验证 G(p),G(p Fq) 的编码优化公 2. 已有的相关的转换公式 G(p) 和 G(p Fq) 是 BMC 的 LTL 规范公式中, 在协议验证中非常重要用得最多的模态词.G(p) 验证协议的机密性,G(p Fq) 验证协议的认证性等 ; 它们用来验证智能体系统的多种属性 [5]. 一般 p,q 为布尔公式,G(p) 和 G(p Fq) 的否定形式的 NNF 公式为 F( p) 和 F(pG( q)). depth(f( p))=, 由表可知, [[F( p)]] = [[F( p)]], 由公式 () 和定理 3 可推出 G(p) 的 BMC 转换公式为 [[ M,F( p)]] = [[ M]] [[F( p)]] (2) depth(f(pg( q)))>, 只能由公式 () 和定理 2 得到 G(p Fq) 的 BMC 转换公式 : [[ M,F( p G( p))]] = [[ M]] [[F( p G( p))]] ( L [[F( p G( p))]] ) (3) = 尽管公式 (2) 公式(3) 这些经过文献 [7] 优化过的公式, 与原公式相比, 求解效率有一定的提高, 但这些优化方法并未考虑 [[ M ]]. 如果同时考虑 [[M ]], 那么根据这些公式明显的递增特性, 可推出逻辑等价或至少是有蕴含关系的简洁递推公式. 在目前已知的 BMC 工具 (NuSMV,VIS 等 ) 的各较新版本中也均未见讨论此类问题的递推公式的实现. 本文定理 4 给出了公式 [[ M,F( p)]] 简洁的逻辑等价的递推公式的证明, 定理 6 给出了公式 [[ M,F( p G( q))]] 的蕴含公式的递推公式的证明. 通过定理 4 和定理 6 的递推公式编码出的 SAT 实例远远小于公式 (2) 和公式 (3) 编码成的 SAT 实例, 通过用 SAT 公式求解验证, 求解效率明显提高, 从而提高 BMC 的效率.

5 杨晋吉等 : 有界模型检测的优化转换公式优化方法和效率分析 + 定理 4. 如果 [[ M,F( p)]] 是不可满足的, 则 [[ M,F( p )]] + 逻辑等价于 [[ M ]] + ( p + ). 证明 : [[ M,F( p)]] = [[ M]] [[F( p)]] = Is ( ) Ts (, s+ ) p+ = = + = Is ( ) Ts (, s+ ) p p+ ( 由表可知, p = p+ ) = = + = Is ( ) Tss (, + ) p Ts (, s+ ) Is ( ) Tss (, + ) p+ = = = + = ([[ M,F( p)]] T( s, s+ )) ([[ M]] + p+ ) 由前提可知, [[ M,F( p)]] 是不可满足的, 则 [[ M,F( p)]] T( s, s + ) 是不可满足的. 因为 [[ M,F( p)]] + T( s, s + ) 是不可满足的, 若 [[ M,F( p )]] + 是可满足的, 则可由逻辑或关系的性质得出 [[ M ]] + ( p + ) 也是可满 + + 足的 ; 反过来, 若 [[ M ]] + ( p + ) 是可满足的, 则 [[ M,F( p )]] + 是可满足的, 这也证明了 [[ M ]] + p + 逻辑等价于 [[ M,F( p )]] +. + 由定理 4 可知, 在 [[ M,F( p)]] 编码的 SAT 实例无解的前提下, [[ M ]] + p + 逻辑等价于 [[ M,F( p )]] +. 由此 + 得出,[[ M,F( p )]] + 编码的 SAT 实例的解就是 [[ M ]] + p + 编码的 SAT 实例的解 ; 反之也成立. 若 [[ M ]] + 编码的 SAT 实例无解, 则 [[ M,F( p )]] + 编码的 SAT 实例也无解. 而 [[ M ]] + p + 编码的 SAT 实例的规模小于 + [[ M,F( p )]] + 编码的 SAT 实例规模, 因此, 本文用求解 [[ M ]] + p + 的 SAT 实例来代替求解 [[ M,F( p )]] + 的 SAT 实例, 从而提高了求解效率. 下面比较分析编码成的 SAT 子句的效率提高问题.SAT 实例的子句内部是各原子变量逻辑或的关系, 子句 p 间是逻辑与的关系. 在 LTL 公式中,G,F,X,U 等模态词和蕴含词可转换为只包含,, 等连接词的公式.BMC 转化公式 φ 编码成的 SAT 实例的子句数量为 n(φ), 其递归求解过程见表 2. Tabe 2 由表 2 得到公式 (2) 的子句数量公式为 Recursve defnton of cause number of φ 表 2 φ 子句数量的递归定义 φ n(φ) n(φ) φ n(φ ) n(φ ) φ φ 2 n(φ )+n(φ 2 ) n(φ )n(φ 2 ) φ φ 2 n(φ )n(φ 2 ) n(φ )+n(φ 2 ) n([[m]] )+n( [[F( p)]] )=n([[m]] )+n p =n([[m]] )+ n ( p ) (4) = = 由表 2 和定理 4 得到 [[ M,F( p)]] 的子句数量公式为 n([[m]] )+ n ( p ) (5) n( p 公式 (4) 和公式 (5) 的 n([[m]] ) 部分相同, 只比较两公式的第 2 部分. 由表可知, n ( p ) = ). 设 n ( p ) = m,m 为一个整数常数, 公式 (4) 的第 2 部分的复杂性为指数次,O(m ). 文献 [] 通过增加原变量近 4 倍的新变量和重命名 (renamng) 的方式把原公式转换为可满足性等价的公式, 使子句数降为线性 tm 级, 其中 t>, 其复杂性降为线性复杂性 O(t). 公式 (5) 的第 2 部分为常数阶复杂性 O(m), 通过比较可看出, 公式 (4) 和公式 (5) 的第 2 部分的规模由线性阶复杂性降为常数阶复杂性, 且没有增加新变量. 本文对 G(p Fq) 进行优化时, 充分考虑在协议验证时 G(p Fq) 的语义. 若验证规范是 G(p Fq), 其示意图为图. 若 p 在状态 s 为真, 则至少存在个, 使 q 在状态 s 为真. G(p Fq) 否定形式的 NNF 公式是 F(pG( q)), 其示意图为图 2. 若 p 在状态 s 为真, 则从状态 s 开始的后续

6 2 Journa of Software 软件学报 Vo.2, No.8, August 29 所有状态中,q 都为假. p q s s s + s s + Fg. A representaton satsfes G(p Fq) 图 G(p Fq) 为真 p, q q q q s s s + s s + Fg.2 A representaton satsfes F(pG( q)) 图 2 F(pG( q)) 为真 [[ M,F( p G( q))]] = [[ M]] [[F( p G( q))]] ( L [[ F( p G( q))]] ). = 由表可知, [[G( q)]] =, 所以 [[F( p G( q))]] = ( p [[G( q)]] ) =, 由此可以把公式 (3) 简化为 [[ M]] ( L [[F( p G( q))]] ), = 这其实还是一个非常复杂的公式, 因为公式 (3) 的一个蕴含公式 : L = 可能产生环, 很难直接得到递推公式. 根据图图 2 的思想, 可以得到 [[ M]] [[F( p G ( q))]] 其中, [[F( p G( q))]] = [[ p]] [[ q]]. 本蕴含式与图图 2 语义示意图相一致, 且较易得到递推公式. 定理 5. 如果 [[ M]] [[F( p G ( q))]] 不可满足, 则 [[ M ]] [[F( p G( q))]] ( L [[F( p = 不可满足. G( q))]] ) 证明 : 因为 [[ M]] [[F( p G( q))]] ( L [[F( p G( q))]] ) 蕴含公式 [[ M]] [[F( p G ( q))]], = 根据蕴含性质, 当 [[ M]] [[F( p G ( q))]] 不可满足时, [[ M ]] [[F( p G( q))]] ( L [[F( p = 不可满足, 证毕. G( q))]] ) 根据定理 5 可知, 当边界值为时, 若公式 (6) 不可满足时, 有公式 (3) 也不可满足, 则可验证 BMC 问题在边界内是正确的 ; 若公式 (6) 可满足, 则尽管公式 (3) 不一定满足, 但可以得到一个较为理想的 BMC 下界, 从下界开始再用公式 (3) 求解, 也一定比当下界 = 时就一直用公式 (3) 求解的效率要高. [[ M ]] 定理 6. 如果 [[ M]] [[F( p G ( q))]] 是不可满足的, 则 [[ M]] [[F( p G ( q))]] 逻辑等价于 ( p 证明 : q + + ). [[ M]] [[F( p G ( q))]] [[ M]] p q = = = [[ M]] + p+ q+ ( p+ q ) + = + + (6)

7 杨晋吉等 : 有界模型检测的优化 = [[ M]] + p q+ q+ ( p+ q+ ) = = [[ M]] + p q q+ ( p+ q+ ) = = [[ M]] p q T( s, s+ ) q+ ([[ M]] + ( p+ q+ )) = = ([[ M]] [[F( p G ( q))]] T( s, s ) q ) ([[ M]] ( q q + )) 由前提可知, [[ M]] [[F( p G ( q))]] 不可满足, 则 [[ M ]] [[F( p G ( q))]] T( s, s ) q + + 也不可满足 ; 若 [[ M]] [[F( p G ( q))]] 满足, 则 [[ M ]] ( p q ) 必满足, 反之, 若 [[ M ]] ( p q ) 满足, 则 [[ M]] [[F( p G ( q))]] 必满足. 由此得证. + + 定理 7. 如果当依次取,,2,,m 时,[[ M ]] ( p q) [[ M]] ( L [[F( p G( q))]] ) = 足, 则当依次取 m+,m+2,, max 时, m+ ( p [[G( q)]] ). 证明 : [[ M]] ( L [[F( p G( q))]] ) = [[ M]] L [[ p G( q))]] = = = 不可满足, 当取 m+ 时, [[ M ]] ( ) 可满 p q 逻辑等价于 [[ M ]] L = = [[ M]] L ( p [[ G( q)]] ) ( 由表可知, p = p) = = m =[[ M]] L ( p [[ G( q)]] ) ( p [ [ G( q)]] ) = m+ m = + = = [[ M]] L ( p [[G( q)]] ) = m+ ( 由表中 p p 和 Gp的性质以及本定理的前提可知,[[ M]] ( p [[ G( q)]] ) = ) 对 G(p Fq) 否定形式的 NNF 公式 F(pG( q)) 求解时, 用定理 6 和定理 7 的组合来代替转换公式 [[ M]] ( L [[F( p G( q))]] ) ( 文献 [7] 对公式 (3) 优化过的逻辑等价式 ). 由于公式 (6) 符合 F(pG( q)) 的语 = 义且是公式 (3) 的蕴含式 ; 一般情况下, 当取,,2,,n(n MAX) 时, 公式 (3) 是无解的, 这时一定有当取,,2,,m(m n) 时, 公式 (6) 是无解的, 根据定理 5, 我们先用公式 (6) 的逻辑等价式 [[ M ]] ( p q + + ) 来确定公式 (6) 无解时的 m 值. 基于前述相似的理由, 当 [[ M]] [[F( p G ( q))]] 不可满足时, 用求解公式 [[ M ]] ( p q + + ) 编码的 SAT 实例来代替求解公式 [[ M]] [[F( p G ( q))]] 编码的 SAT 实例, 由开始, 依次加进行循环迭代 ; 当取 m+ 时,[[ M ]] ( p q ) 编码的 SAT 实例有解, 则再根据定理 7, 使从 m+ 开始, 用公式 [[ M]] ( L [[F( p G( q))]] ) 的逻辑等价式 [[ M]] 来 L ( p [[G( q)]] ) = m+ = 进行编码求解, 若公式 [[ M]] ( [[G( )]] ) 编码的 SAT 实例有解, 此解就是公式 L p q = m+ [[ M,F( p G( q))]] 的 SAT 实例解. 下面我们再来分析编码成 SAT 实例子句的效率. 参照表 2, 公式 (3) 产生的子句数量公式为 n([[m]] )+ ( n( ) ( [[F( G( ))]] )) (7) L + n p q =

8 22 Journa of Software 软件学报 Vo.2, No.8, August 29 定理 6 的公式 [[ M]] [[F( p G ( q))]] 产生的子句数量公式为 n([[m]] )+n( p )+n( q ) (8) 公式 (7) 和公式 (8) 的第部分都为 n([[m]] ), 同理, 只比较第 2 部分. 由表 2, 设 n( ) =m,m 为一个整数常数, ;n( q )=r,r 为一个整数常数,. 公式 (7) 的第 2 部分非常复杂, 其复杂性不低于指数级 O((m+r) ), 同样, 通过文献 [] 增加变量和重命名的方式把原公式转换为可满足性等价的公式, 使子句数降为线性 t(am+br) 级, 其中 a,b 各为一个整数常量,t>, 使其复杂性降为线性复杂性 O(t); 而公式 (8) 的第 2 部分的复杂性为常数阶 O(m+r), 且未增加新变量. 3 相关的工作本文的工作是文献 [7] 的工作的继续. 文献 [7] 分析了原始的 BMC 的 SAT 编码问题, 主要针对 BMC 转换公式的 [[ f ]] 公式进行了多种优化工作, 也提出一些高效的存储结构等. 这些工作在 NuSMV2..2 中实现, 且在后 [9] 续版本中不断完善.Tmo 等人利用 asso-shaped Krpe Structure 的特点, 把求解 CTL(computaton tree ogc) 公式用到的固定点 (fxpont) 方法运用到 BMC 的转换公式中. 文献 [9] 中的很多实验结果表明, 此方法比文献 [7,8] [8] 中的方法更为有效.Frsch 等人采用固定点的方法, 分别把 BMC 转化公式用 SNF 和固定点的标准形式表示. 固定点的标准形式充分利用了标准形式的特点, 使用类似于 Tabeau_stye 的方法. 实验结果表明,SAT 编码规模小于文献 [7], 总体上也优于 SNF 的表示. [,] Sherdan 等人对 BMC 编码成的 SAT 实例进行优化, 为了降低编码成 SAT 实例的复杂性, 编码时通过增加新变量和重命名, 这样编码成的 SAT 实例有很大的冗余, 因此, 基于 Boy de a Rour 思想, 提出了一种紧缩的优化编码的方法, 使得产生的 SAT 实例的规模大幅度降低, 但 BMC 的一些特征在所产生的 SAT 实例中消失了. [2] Strchman 等人利用 BMC 产生的 SAT 实例的一些特性, 如变量的次序冲突子句的处理等, 对 SAT 工具 [4] 进行优化,Gupta 等人利用 BDD 模型检测运行使得 SAT 工具自动获取 SAT 实例的一些特征, 也取得了较好的效率. 4 实验结果比较本文是在 NuSMV2.3. 模型检测工具中完成相应的优化工作. 本文的工作主要与 NuSMV2.3. 原方法和另 [9] 一种较好的 BMC 方法进行比较. 其中,NuSMV2.3. 原方法是在文献 [2] 的基础上, 经过文献 [7] 优化的方法, 本文简称为 AA_BMC 方法 ; 另一种较好的方法是由 Tmo 等人提出, 且在 NuSMV2.4. 中实现的, 本文简称为 Tmo_BMC 方法. 因为 Tmo_BMC 方法总体上优于另外几种优化的方法 [7,8], 因此本文没有与其他方法进行比较. 本文给出的对 G(f ) 优化方法称为 G_BMC, 对 G(p F(q)) 优化方法称为 G_F_BMC. NuSMV. 实验的环境如下 : 硬件 :Inte Core 43 处理器,2G 内存 ; 软件 :Wndows XP 专业版,WnGW32 平台编译实验用的模型主要取自文献 [5], 和自编的 NSPK 协议模型.BMC 具有这样的特点 : 边界越小, 验证时间越短 ; 越大, 验证时间越长. 若模型的边界较小, 则算法的验证时间比其他算法要短 ; 当变大时, 算法的验证时间仍然比其他算法要短. 若模型较小, 则在同样的边界下, 算法的验证时间比其他算法要短 ; 若模型较大, 则在同样的边界下, 算法的验证时间仍然比其他算法要短. 基于这些特点, 为了缩短实验的时间, 本文采用的模型较小 ; 若比较费时, 就缩短边界上界 K. 模型中都包含有 G(p) 或 G(p F(q)) 验证规范的例子. 本实验所用的模型大部分是用 CTL 规范说明, 要改为等价的 LTL 规范说明, 若在 K 边界内有解, 则要对 LTL 规范作适当的修改, 使其不可满足, 这样更便于验证算法的有效性.NSPK 协议模型当边界 =4 时可满足属于例外. 每个模型测试的项目包括运行完边界后, 其编码生成的 SAT 实例的变量数子句数生成 SAT 实例和求解 SAT 实例的总的时间 ( 单位 :s). 求解用的 SAT 工具为 NuSMV 内置的 SAT 求解工具. 由表 3 表 4 的实验数据可知, 在验证模态词 G(p) 和 G(p F(q)) 时,Tmo_BMC 算法与 AA_BMC 算法相比, p

9 杨晋吉等 : 有界模型检测的优化 23 并没有明显的优势. 本文提出的 G_BMC 和 G_F_BMC 在验证这类模态词时比前两类算法优势明显, 通过观察所产生的 SAT 实例的变量数和子句数, 其效率提高的幅度因不同的模型而有差异, 如 BRP 模型提高幅度稍小,SEMAPHORE 模型则提高幅度很大. 如前所述, 提高的幅度与验证规范公式复杂性密切相关, 模态词 G(p) 和 G(p F(q)) 的表达式越复杂, 效率提高得越明显. Mode Mutex DME4 NSPK Mode DME2 BRP Semaphore satsfed Tabe 3 Comparson of encodng G(p) 表 3 各 G(p) 编码比较 AA_BMC Tmo_BMC G_BMC Varabes Causes Tme Varabes Causes Tme Varabes Causes Tme < < < Tabe 4 Comparson of encodng G(p F(q)) 表 4 各 G(p F(q)) 编码比较 AA_BMC Tmo_BMC G_F_BMC Varabes Causes Tme Varabes Causes Tme Varabes Causes Tme < G_BMC 算法是基于定理 4 的, 其递推公式与公式 (2) 是逻辑等价的, 因此, 当 G_BMC 算法不可满足时, 模态词 G(p) 在阶段成立 ; 当 G_BMC 算法有可满足解时, 此解就是 G(p) 不成立的反例.G_F_BMC 算法是基于定理 6 和定理 7 的, 其中定理 6 的前提条件公式 (6) 与公式 [[ M,F( p G( q))]] 不等价, 是蕴含关系 ( 公式 [[ M,F( p G( q))]] 蕴含公式 (6)), 这在验证模型的正确性上是一致的 ; 而当定理 7 使公式 (6) 可满足时, 则可获得正确的反例. 当 G_F_BMC 算法不可满足时, 公式 [[ M,F( p G( q))]] 一定不可满足, 模态词 G(p F(q)) 在阶段一定成立 ; 而当 G_F_BMC 算法中的定理 7 使得公式 (6) 可满足时, 则可正确求出公式 [[ M,F( p G( q))]] 的 SAT 解, 即 G(p F(q)) 性质不成立时的反例解. 由表 4 可以看出,G_F_BMC 算法比另两种方法的效率提高得较明显. 5 结束语本文对有界模型检测中比较重要且很常用的 LTL 的模态词 G(p) 和 G(p F(q)) 编码进行优化, 结合 FSM 的状态转移关系和这些模态词的语义, 推出简洁且高效的递推式, 证明了递推式和原公式的等价或蕴含关系, 分析了优化后的方法产生的 SAT 实例的复杂性, 最后通过实验, 用具体的模型验证了本方法的有效性. 根据本文优化所采用的递推思想, 应该可以对部分其他 LTL 模态词编码进行优化, 这是下一步的工作. 致谢衷心感谢论文评审专家中肯而有益的评审意见和相关编辑严谨热情的工作 ; 感谢 Bere,Cmatt 等人提供的 NuSMV 系统 ; 感谢田艳玲副教授和陈清亮同学的帮助和支持. References: [] Care EM, Grumberg O, Peed DA. Mode Checng. Cambrdge: The MIT Press, [2] Bere A, Cmatt A, Care EM, Zhu Y. Symboc mode checng wthout BDDs. In: Ceaveand R, ed. Proc. of the 5th Int Conf. on Toos and Agorthms for the Constructons and Anayss of Systems (TACAS 99). LNCS 579, Bern: Sprnger-Verag, [3] Cmatt A, Care EM, Gunchga E, Gunchga F, Pstore M, Rover M, Sebastan R, Tacchea A. NuSMV 2: An opensource too for symboc mode checng. In: Brnsma E, Larsen KG, eds. Proc. of the 4th Int Conf. on Computer Aded Verfcaton < 7

10 24 Journa of Software 软件学报 Vo.2, No.8, August 29 (CAV 22). LNCS 244, Bern: Sprnger-Verag, [4] Ama N, Kurshan R, McMan K, Mede R. Expermenta anayss of dfferent technques for bounded mode checng. In: Hubert G, Hatcff J, eds. Proc. of the 9th Int Conf. on Toos and Agorthms for the Constructons and Anayss of Systems (TACAS 23). LNCS 269, Bern: Sprnger-Verag, [5] Luo XY, Su KL, Yang JJ. Bounded mode checng for tempora epstemc ogc n synchronous mut-agent systems. Journa of Software, 26,7(2): (n Chnese wth Engsh abstract). [6] Dane G, Urch K, Rof D. HW/SW co-verfcaton of embedded systems usng bounded mode checng. In: Qu G, Isma YI, Vayrshnan N, Zhou H, eds. Proc. of the 6th ACM Great Laes Symp. on VLSI 26. Carns: ACM Press, [7] Cmatt A, Pstore M, Rover M, Sebastan R. Improvng the encodng of LTL mode checng nto SAT. In: Agostno C, ed. Proc. of the 3rd Int Worshop on Verfcaton, Mode Checng, and Abstract Interpretaton (VMCAI 22). LNCS 2294, Bern: Sprnger-Verag, [8] Frsch A, Sherdan D, Wash T. A fxpont encodng for bounded mode checng. In: Aagaard MD, OLeary JW, eds. Proc. of the 4th Int Conf. on Forma Methods n Computer-Aded Desgn (FMCAD 22). LNCS 257, Bern: Sprnger-Verag, [9] Latvaa T, Bere A, Heano K, Juntta T. Smpe bounded LTL mode checng. In: Hu AJ, Martn AK, eds. Proc. of the 5th Int Conf. on Forma Methods n Computer-Aded Desgn (FMCAD 24). LNCS 332, Bern: Sprnger-Verag, [] Jacson P, Sherdan D. Cause form conversons for booean crcuts. In: Hoos HH, Mtche DG, eds. Proc. of the 7th Int Conf. on Theory and Appcatons of Satsfabty Testng (SAT 24). LNCS 3542, Bern: Sprnger-Verag, [] Jacson P, Sherdan D. The optmaty of a fast CNF converson and ts use wth SAT. In: Hoos HH, Mtche DG, eds. Proc. of the 7th Int Conf. on Theory and Appcatons of Satsfabty Testng (SAT 24). LNCS 379, Bern: Sprnger-Verag, [2] Strchman O. Acceeratng bounded mode checng of safety propertes. Forma Methods n System Desgn, 24,24():5 24. [3] Care EM, Kroeng D, Ouanne J, Strchman O. Competeness and compexty of bounded mode checng. In: Steffen B, Lev G, eds. Proc. of the 5th Int Conf. on Verfcaton, Mode Checng, and Abstract Interpretaton (VMCAI 24). LNCS 2937, Bern: Sprnger-Verag, [4] Gupta A, Gana M, Wang C, Yang Z, Ashar P. Learnng from BDDs n SAT-based bounded mode checng. In: Proc. of the 4th Conf. on Desgn Automaton (DAC 23). Montrea: IEEE Computer Socety Press, [5] 附中文参考文献 : [5] 骆翔宇, 苏开乐. 杨晋吉. 有界模型检测同步多智体系统的时态认知逻辑. 软件学报,26,7(2): /7/2485.htm 杨晋吉 (968-), 男, 山西太原人, 博士, 副教授, 主要研究领域为模型检测, 协议验证. 林瀚 (979-), 男, 博士,CCF 会员, 主要研究领域为人工智能逻辑及其算法. 苏开乐 (964-), 男, 博士, 教授, 博士生导师,CCF 高级会员, 主要研究领域为模型检测, 智能体系统. 肖茵茵 (983-), 女, 博士生,CCF 学生会员, 主要研究领域为模型检测, 安全协议验证. 骆翔宇 (974-), 男, 博士, 副教授, 主要研究领域为模型检测, 多智体系统.

untitled

untitled ISS -985, CODE RUXUEW E-mal: jos@scas.ac.cn Journal of Software, Vol., o.6, June, pp.96 37 http://www.jos.org.cn do:.374/sp.j...359 Tel/Fax: +86--656563 by Insttute of Software, the Chnese Academy of Scences.