（计算机软件与理论专业论文）弱公平条件下模型检验状态空间的对称化简.pdf

弱公平条件下模型检验状态空间的对称化简 论文题目： 专业： 硕十生： 指导老师： 弱公平条件下模型检验状态空间的对称化简 计算机软件与理论 周文 张治国副教授 摘要 形式化验证已经成为对系统设计和协议设计进行确认的重要手段，其方法分 为两类1 4 ”，一类是以逻辑推理为基础，另一类则以穷尽搜索为基础，穷尽搜索方 法统称为模型检验。逻辑推理的不足之处在于推理的难度。对于稍微复杂的系统， 自动化的推理就难以胜任。模型检验的好处在于它有全自动化的检验过程，并且 如果一个性质不满足，它能给出这个性质不满足的理由，可据此对系统设计进行 改进。 状态爆炸l6 1 是模型检验中的一个重要难题。实际系统中的状态数目可能很 大，以至无法在有限的时间和内存空间下进行完整的检验。 对称归约是处理状态爆炸问题的有效技术之一。但是在实际系统验证时，如 果是处于公平条件下，已有的对称归约算法很难有有效的作用。而在实际应用中， 公平性足验证一些性质的先决条件。 本文给出了一个模型检验的算法，在公平条件下利用对称归约化简状态空 间，以改善状态爆炸问题。 这个算法基于嵌套深度优先搜索( n d f s ) 算法。它假定要检验的性质用b t l c h i 自动机1 1 9 i 给定，因此，检验系统是否支持某个给定性质的问题，就归结为在图 中寻找接受回路的问题1 7 , 6 1 。 本文首先叙述并分析了标准的n d f s 算法1 7 17 】和带对称归约的n d f s 算法 1 3 1 ：然后通过对模型检验器s p i n 中的弱公平性算法( 由h o l z m a n n 实现) 进行扩 展，提出了一个在弱公平条件下、未使用对称归约的、基于嵌套深度优先搜 ( n d f s ) 的模型检验策略，最后在此基础上提出基于n d f s 的融合弱公平性和 对称归约的算法。 相对于基于寻找最大强连通分支( m s c c ) 的类似算法i l l ，“l ，本算法具有基 于n d f s 的优势，每个状态的空间开销也要少，而且，虽然与它们有相同的最坏 时间复杂度o ( n l h ( t ) i ) ，但是在检测到性质的一个反例时，本算法需要遍历 的状态要少得多，因此具有更好的时间和空间复杂性，同时也兼容于近似验证技 术。 本文还把这个算法的原型运用在通用的模型检验器s p i n 之上，对p e t e r s o n 互斥协议等例子的进行验证实验。实验的结果显示，本文的算法使对称归约在弱 公平条件下的化简效果接近于它不在弱公平条件约束下的化简效果。 关键词：模型检验，状态爆炸，嵌套深度优先搜索，对称归约，公平性 弱公平条件下模型梭骢状态空间的对称化简 t i t l e ：s y m m e t r yr e d u c t i o ni ns t a t es p a c ef o rm o d e lc h e c k i n g u n d e rw e a kf a i r n e s s m a j o r ：s o f t w a r e a n dt h e o r e t i c a lc o m p u t e rs c i e n e e n a m e ：z h o uw e n s u p e r v i s o r ：v i c e p r o f e s s o rz h a n gz h i - g u o a b s t r a c t f o r m a lv e r i f i c a t i o nh a sb e e na ni m p o r t a n tm e t h o dt oc o n f i mt h ed e s i g no f s y s t e m sa n dp r o t o c o l s i t st e c h n i q t i e sc a n b ed i v i d e di n t ot w oc l a s s e s ：o n ei sb a s e do n l o g i cr e a s o n i n g ；o n ei sc a l l e dm o d e lc h e c k i n g 弧es h o r t c o m i n go fl o g i cr e a s o n i n gi s t h ed i f f i c u k yo fr e a s o n i n g ，a n di ti sh a r dt ob ea u t o m a t e df o rs l i g h t l yc o m p l i c a t e d s y s t e m s t h em o d e lc h e c k i n gi sb a s e do n e n u m e r a t i o ns e a r c h i ti sak i n do f a u t o m a t i c f o r m a lv e r i f i c a t i o nt e c h n i q u e , a n de a ng i v et h e x t & s o nw h e nas y s t e ms p e c i f i c a t i o n c a nn o tf i ts o l n eo fi t sp r o p e r t i e s , s ot h es y s t e mm o d e lc a r lb em o d i f i e da c c o r d i n gt o t h a tr e a s o nd u r i n gs y 髓e m d e s i g n t “i t h em a i np r o b l e mi nm o d e l c h e c k i n gi st h a tt h es i z eo f t h es t a t es p a c em a yg r o w v e r yr a p i d l yw i t ht h es i z eo f t h es y r s t e mm o d e l 柏i ss i t u a t i o ni sk n o w na st h es t a t e e x p l o s i o n 1 6 l 。 s y m m e t r yr e d u c t i o ni sa n e f 嚣c 沁n tm e t h o dt oa l l e v i a t et h e 髓a t ee x p l o s i o n 。 s u r p r i s i n g l y , t h em e t h o d s a r en o te 饪h t i r et oa d m i t a l l ya m e l i o r a t i o no f s t a t e r e d u c t i o ni nt h ec a s eo f f a i r n e s sa s s u m p t i o n b u tt h ef a i m e s si sa p r e r e q u i s i t ef o rt h e v e r i f i c a t i o no f m a n y i n t e r e s t i n gs y s t e mp r o p e r t i e si np r a c t i c e 弧i st h e s i sp r e s e n t sa l la l g o r i t h mf o rm o d e lc h e c k i n gu n d e rw e a kf a i r n e s st h a t e x p l o i t ss y m m e t r y t or e d u c et h es t a t es p a c e t h e a l g o r i t h mi sb a s e do n t h en e s t e dd e p t hf i r s ts e a r c h ( n d f s la l g o r i t h m t “1 i ti sa s s u m e dt h a tt h ep r o p e r t i e st ob ec h e c k e da r eg i v e na sb t l c h ia u t o m a t a i s ot h e p r o b l e mo f c h e c k i n g w h e t h e rt h es y s t e mh o l ds o m eg i v e np r o p e r t yc a l lb er e d u c e dt o t h ep r o b l e m o f f i n d i n ga c c e p t a n c ec y c l e si nt h eg r a p hr e p r e s e n t i n go f t h es y s t e m s t a t e s p a c eo f t h ep r o p e r t ya u t o m a t o n l 7 “if i r s td e s c r i b ea na l g o r i t h mb a s e do nn d f sf o r m o d e lc h e c k i n gu n d e rw e a kf a i m e s sw i t h o u ts y m m e t r yr e d u c t i o 轧t h e np r e s e n tt h e a l g o r i t h m w h i c h m e r g e s f a i r n e s sa n ds y m m e t r yr e d u c t i o n i nt h i st h e s i s , t h ep r o t o t y p eo ft h ep r e s e n t e da l g o r i t h mi sa p p l i e do nt h em o d e l c h e c k e rs d 逸。稚l er e s u k so ft h ee x p e r i m e n t ss h o wt h a tt h ea l g o r i t h mc a n l e t s y m m e t r y r e d u c t i o nb ee f f e c t i v ei nc o n d i t i o no f w e a k f a i m e s s k e y w o r d s ：m o d e lc h e c k i n g ，s t a t ee x p l o s i o n , n d f s ，s y m m e t r yr e d u c t i o n , f a i r n e s s 弱公平条件下模型检验状态空间的对称化简 1 1 问题的提出 第1 章背景与现状 通常，软件系统或协议可以通过对原型的测试来不断地改进。而对于复杂且 对安全性要求很高的系统或协议，如果要等到建立系统才能进行质量评估，代价 可能非常昂贵。在设计过程的早期，如果能对系统的说明进行验证的话，将会大 大地减少以后的修改工作。 形式化方法原则上就是用数学与逻辑来描述和验证软件系统或协议的方法。 从描述上讲，一方面是系统或协议的描述，另一方面是性质的描述。这些可 以用一种或多种语言来描述。这些语言包括命题逻辑，线性时序逻辑，进程代数 等等。基于时态逻辑的说明语言理论上能说明任何软件系统或协议1 4 j ，这方面的 描述语言有，兀，a + ，p r o m e l a 等。 从验证来讲，主要有两类方法1 4 2 l ，一类是以逻辑推理为基础，另一类则以穷 尽搜索为基础。穷尽搜索方法统称为模型检验( m o d e lc h e c k i n g ) 。 逻辑推理的不足之处在于推理的难度。对于稍微复杂的系统，自动化的推理 就难以胜任。模型检验的好处在于它有全自动化的检验过程，并且如果一个性质 不满足，它能给出这个性质不满足的理由，可据此对系统设计进行改进。 形式化验证的应用在集成电路设计和协议设计上都取得了很大的成绩。但是 对软件系统的验证要复杂得多，因为软件的描述要比电路和协议复杂，状态空间 大得多。 模型检验的方法通常需要对系统的所有可达状态进行系统化的检验，因此常 常需要很多的时间和内存空间。随着系统的增大，系统所包含的状态空间会迅速 增长，实际系统中的状态数目可能非常庞大，以至无法在有限的时间和内存空间 下进行有效的检验，使得常规的搜索算法无能为力，这种现象称为状态爆炸问题 1 6 1 。因此，改善状态爆炸成为了模型检验的一个研究重点。任何新的模型检验方 法需要满足以下目标p ： 尽可能地大幅度减少需要检验的状态； 新的算法应该尽可能地使用较少的内存和时间； 新的算法应该能容易使用并且能高度自动化。 在执行时态逻辑模型检验时，利用对称归约是解决状态爆炸问题的有效手段 0 0 , 6 。 许多系统，如互斥算法、缓冲一致协议、或者总线通信协议，都显示了对称 的巨大程度。我们来看一个典型的互斥协议。无论怎么调整进程标记的秩序，进 程同时进入它们的临界区( c r i t i c a ls e c t i o n s ) 的可能( 或不可能) 性是保持不变 的。因此，在遍历状态空间时，如果一个正在被访问的状态等于对已经访问过的 状态进行一次p i d ( 进程i d ) 次序交换，那么这个搜索就可以删去。更形式化地 讲，系统的对称性表示为系统全局的状态上的一个给定的置换群g 。对其中任意 两个状态s 和s ，如果存在一个置换ne g ，使得s 能通过对s 进行n 置换得到， 则s 和s ，是行为等价的。这样，系统状态空间t 就被分为等价类。我们定义一个 选择函数h ，从每个等价类中唯一选择一个代表，然后，这个被构造的商状态空 间h ( t ) 就只包含代表元素，只需要在h ( t ) 上检验性质是否满足，而不用在 弱公平条件下模型检验状态空间的对称化简 t 上去检验了。通常来说h ( t ) 比t 小得多，因此对验证算法在内存和时间方 面的改善可能是巨大的。 然而，令人奇怪的是，尽管公平性很容易用时态逻辑表达，但是一旦把公平 性考虑进去时，这些对称归约的方法对状态爆炸问题改善的效果就很小了1 1 1 , 1 4 i 。 但是，由于公平性对证明活性( 1 i v e n e s s ) 和推进性( p r o g r e s s ) 非常重要，因此， 在对通常交错语义的并发性进行建模的时候，公平是非常必要的。 公平分为强公平和弱公平两种i s , l i j 。强公平是指如果某个进程无限次地被激 活( e n a b l e d ) ，那么这个进程将被无限次地执行( e x e c u t e d ) ，形式地表示为： 。( g f e n , 一g f e x , ) ，其中命题e n ，表示进程i 在状态s 上是活动的，c ) 【i 表示由 进程i 的单步的执行而得到的转换产生了状态s 。强公平通常用于对同步交互建 模，但它会使模型检验更加困难，因此尽量避免使用。 本文主要关注弱公平性。弱公平性的含义是：对系统的每个执行序列，如果 某个进程从某个时间点开始被持续地激活，那么这个进程中至少有一条指令将最 终被执行，简而言之就是“如果进程能够推进那么它就不会永远等待”。可形式 地表示为： 。( f g e n ，- - ) g f e x i ) 。弱公平对于异步模型是充分的。它经常与互 斥算法、繁忙等待、单个的调度执行队列、资源分配等联系在一起，将保证这些 属性的正确性，例如，在互斥条件下持续试图进入临界区的进程最终能进入临界 区，或者在调度中已经进入等待队列的每个进程将最终离开等待队列。因此，把 弱公平性下的模型检验算法与对称归约技术结合到一起，实际是验证许多性质的 先决条件。 本文试图提出一个模型检验的算法，实现在弱公平条件下利用对称性化简状 态空间。 弱公平条件下横蛩稔验状态空简的对称化衙 1 2 当前国内外的研究状况 一般认为，形式化方法始于2 0 世纪6 0 年代末的f l o y d ，h o a l e 和m a n n a 等 在程序规格和验证方面的研究1 4 ”，人们试图用数举方法证明程序的正确性而发展 成为各种程序验证方法。 对势发帮分蠢式疆彦戆形式纯验涯随即发袋起来，势扩麓烈验证靖态露舞。 时态逻辑作为形式纯验证中的一种形式描述方法是由p h u e l i 簸早提出麓，并得到 了他本人和m a m a 、o w i c k i 、l a m p o r t 等人的发展。这种新的方法使用时惑逻辑 来描谶动态行为，即程序在时间上的效果。 2 0 世纪8 0 年代e c l a r k e 与e a e m e r s o n 掇嬲模型检验方法1 1 1 ，其基本愿想 藏楚状态穷举，这瓣浚态空蔫，疆梵验涯系统瓣辩态经囊( t e m p o r a lp r o p e r t i e s ) 。 模型梭验把状态国的可达性用作一个k r i p k e 结构，k r i p k e 缭构对对系统的所有 可能的状态序列进杼了编码。由于这方法简便易行，近年在世界上受到工业界与 理论界的广泛注意。先后出现了报多状态空间遍历和模型检验的工具，如s p h l 、 c o s p a n 、s m v 、m u 犟h i 等等。因为趣们是凳众鸯动纯的，因j 逝对用户憋形式 健验谣知误要求磁较低。 状态遍历和模趔检验方法的效率很大程度上依赖可达性状态图的大小，状态 爆炸娥模型检验的主要难题。为了弱化状态爆炸问题，很多人先后提出了许多方 法，主要有o n t h e - 埘方法、对称归约方法、偏序归约方法、b i t - s t a t eh a s h i n g 方 法等镣。 1 9 9 3 年，i 乱d i l l 、c l a r k e 、e m e r s o n 帮s i s t t a 等入先后拯掇了利露系绫状态 空间的对称性化简状态空间的算法。其中，f p 和d i l l 主要集中对基本类型的正 确性( c o r r e c t n e s s ) 进行推理，即，用时态逻辑c t l 表达的、形式为a g - e r r o r 的安全特性( s a f e t y p r o p e r t i e s ) 。c l a r k e 等人以及随后的e m e r s o n 和s i s t l a 提燃， 逶芰瘫爨群理论酶麓零撬念，霹黻涮爱黠穗魏对覆c t l 交逡瓣掰毒正确戆验涯 进行状态空闻纯简。研究表明，对称归约方法怒模型检验中解决状态空间璨炸的 最有效的武器之一。 然而，在实际的验证中发现，一旦把公平性考虑进去时，这些利用了澍称归 约豹方法对状态爆炸海题改善的教果势不明驻。蔼在爰交镄语义( i n t e r l e a v i n g s e m a n t i c s ) 对并发靛进行建模辩，公平( f a i r n e s s ) 是必要静。这是困秀，多令 顺序谶程( s e q u e n t i a lp r o c e s s ) 的并发执行被处理为单个进稷的充分小的原子步 的非确定的交错执行。为了反应燃个基本要求，每个进程必须以正的但不确定的 速度远行最简单形式的公平可以表达为每个遴程被无限次( i n f i n i t e l yo f t e n ) 地 谖震，在 l 芷窝活戆( l i v e n e s s ) 秘攘进瞧( p r o g r e s s ) 辩，公带蛙是 常墼黎懿。 1 9 9 5 年e m e r s o n 和s i s t l a 掇掇了个公警条件下的对称癌约算法驻“，简称 e s 9 5 。并把公平憾分为两种：强公平性( s t r o n gf a i r n e s s ) 、弱公平性( w e a k f a i r n e s s ) 。这个算法的特点是基于寻找所有最大强连通分支( m s c c ) 的图算法1 2 ”。 1 9 9 7 年g y u r i s 翱s i s t l a 在e s 9 5 算法的基础上进行了改进1 1 4 1 ，这个新的箨法 藏称为g s 9 7 。这个浚送静算法爨然是基于寻掇瞬有最大强逡遥分支( m s c c ) 的图簿法瑚l ，最大的改进是g s 9 7 是o n - t h e - f l y ( 即在需要时才生成状态窝间) 的。 与基于m s c c 的技术不同的另种搜索技术是基于嵌套深度优先搜索 ( n d f s ) 鲍技本。1 9 9 2 年c o u r c o u b e t i s 、v a r d i 、w o l p e r 等入提出了嵌套漾度佳 弱公平条件下模型检验状态空间的对称化简 先搜索算法( n e s t e dd e p t h f i r s ts e a r c ha l g o r i t h m ，简称n d f s 算法) ”j 来检验 状态空间中的接受回路。基于n d f s 的算法与与基于m s c c 的算法相比，它不 需要显式地构造乘积图的强连通分支。所谓乘积图是指表示模型与性质的乘积自 动机的图。1 9 9 6 年，h o l z m a n 等人对n d f s 算法提出进一步的改进1 1 7 l ，以节约 内存空间。随后，h o l z m a n 在模型验证器s p i n 中实现了n d f s 算法，但到目前 为止，在s p i n 中还没有实现对称归约算法。 2 0 0 2 年，b o s n a c k i 提出了一个带对称归约( s y m m e t r yr e d u c t i o n ) 的n d f s 算法1 3 1 ，但没有将公平性结合进去。到目前为止在文献中还没有发现基于n d f s 的结合对称归约和弱公平的模型检验算法。 4 弱公平条件下模型检验状态空间的对称化简 1 3 论文的主要结论和贡献 对系统进行模型检验时，系统中的状态数目通常很大，以至无法在有限的时 间和内存空间下进行完整的检验，这就是模型检验中的状态爆炸1 6 1 难题。 如前所述，对称归约是处理状态爆炸问题的有效技术之一，但是在实际系统 验证时，如果是处于公平条件下，己有的对称归约算法很难有有效的作用。 本文给出了一个基于嵌套深度优先搜索( n d f s ) 的模型检验算法，实现在弱 公平条件下利用对称性化简状态空间。 这个算法假定要检验的的性质用b t l c h i 自动机给定，因而，检验系统是否支 持某个给定性质的问题，就归结为在图( 这个图表示了系统状态空间与性质自动 机的乘积( p r o d u c t ) ) 中寻找接受回路的问题。 为了简化状态空间，本文使用了一个对称归约算法。在简化了的状态空间上 运用一个算法来检验弱公平性接受回路。沿着这些回路，每个进程必定要么挂起 ( d i s a b l e d ) 要么在回路中存在一个转化。其中的关键是怎样把对称性和弱公平 性有效地结合起来，让这两个算法同时运行而不是先后运行，而且用o n t h e - f l y 方式( 即只在需要时才生成状态空间) 。在模型检验中，o n - t h e - f l y 方式是非常重 要的，因为经常没有足够的内存空间和时间来处理整个状态空间。 本文在第二章介绍了形式化描述与验证相关知识，并对时态逻辑的有关符号 进行了规定。在第三章介绍了模型检验的基本思想以及状态空间化简的几个主要 算法。然后在第四章叙述并讨论了标准的n d f s 算法i7 n 和带对称归约的n d f s 算法【3 l ；再在第五章通过对模型检验器s p i n 中的公平性算法( 由h o l z m a n n 实现) 进行扩展，提出了一个在弱公平条件下基于嵌套深度优先搜( n d f s ) 的模型检 验策略，最后在这个策略的基础上提出基于n d f s 的融合弱公平性和对称归约的 算法。 相对于基于寻找最大强连通分支( m s c c ) 的类似算法【i l “l ，本算法具有基 于n d f s 的优势。由于基于m s c c 的算法必须让每个状态保留两个额外的长整 数作为标记，而本提出的算法不需要这些额外的信息，因此每个状态的空间开销 也要少，也能兼容于近似验证技术。而且，虽然与它们有相同的最坏时间复杂度 o ( n l h ( t ) i ) ，但是在检测到性质的一个反例时，本文提出的算法需要遍历的 状态要少得多，因此具有更好的时问和空间复杂性。 本文把这个算法的原型运用在通用的模型检验器s p i n 之上，对p e t e r s o n 互 斥协议等例子的用不同的方法进行验证实验，通过对比这些方法的实验结果，初 步显示本文提出的算法与典型的对称归约算法1 4 l 对状态空间的化简程度接近，表 明本文提出的算法良好地结合了弱公平性和对称归约。 弱公平条件下模型检验状态空间的对称化简 第2 章系统描述与验证 2 1 系统性质概述 系统的性质主要包括以下六个方面“i ：活性、安全性、完各性、可恢复性、 和有界性。 1 、活性( l i v e n e s s ) 活性又称为无死锁性。协议的活性指系统或协议运行时一些好的事情会发 生，这些好的事情包括：预定的事情会产生，指定的状态会达到，应该进行的协 议活动会进行等。协议的活性体现在终止性和进展性两个方面。或者说，如果协 议有终止性和进展性，它就有活性。终止性指系统或协议从任何一个状态开始运 行时，总能正确地到达指定状态。在某些情况下，协议的终止状态和初始状态是 同一个，这样，协议从初始状态开始运行时总能正确地回到初始状态，并反复运 行。这就是协议的可重复性。即，可重复性终止性+ 进展性= 活性 2 、安全性( s a f e t y ) 安全性是指系统或协议在运行时没有坏的事情出现。这些坏的事情包括不可 接受事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界等。 坏事情一般导致两种现象：死锁( d e a d l o c k ) 和活锁( l i v e l o e k ) 。最典型的死锁 是系统或协议各实体都处于这样一个等待状态，即只有在“某个事件”发生后才 能进行进行进一步的动作，但是在该状态下，这个“某个事件”却不会发生。活 锁是指系统或协议处于无限死循环中，系统的状态还是变化的，但不能脱离这种 死循环状态。例如，协议无限隹4 地执行超时重发操作，但是总是不能收到对方的 确认信息。 3 、一致性 协议一致性指协议服务行为和协议行为一致。包括两个方面：协议应该为用 户提供要求的业务；协议无须提供用户没有要求的业务。 4 、完备性 完备性指系统或协议性质完全符号环境的各种要求，即系统或协议的构造考 虑了用户的要求、用户特点、通道性质、工作模式等各种潜在因素的影响，考虑 了对各种错误事件，异常情况的处理。 5 、可恢复性 可恢复性指系统或协议出现差错后，系统或协议本身能否在有限步骤内返回 到正常状态( 包括初始状态) 下执行。可恢复性是和可重复性相关联的一个性质。 6 、有界性 有界性是与系统或协议中的变量和参数有关的一个性质，用来衡量变量和参 数是否超过其限定值。如：缓冲通道中允许驻留的报文数等。 弱公平条件下模型检验状态空间的对称化简 2 2 系统验诞概述 系统验证或协议验证就是确认系统或协议规格模型的有效性，即确认规格模 型是孬滚足蔫求静终东，兹是否一致、宠各、憋否无死镀灌鲅等i , t 1 1 。 形式化验证的鹜疆是系统或协议的行为朝瞧矮的形式馥：擒述。系统懿舒麓可 通过形式模型或者彤式描述语言谶行描述，而系统性质( 需求) 的描述方式是系 统断畜语言( 如c t l 等) 。事实上，各种实际系统模型可以肴成是断言语裔抽象 语义模型( 如时序终构或k r i p k e 缭构) 的一个实例。因此，系统验证就变成确 谈搂熬哥满是淫戆鹚蔻，帮系绫攘鎏是否瀵楚蓉绞錾言( 逻瓣公式) ，蒙嚣说系 统模掇是否是断言逻辑公式的一个模型。对于莉陋状态系统，往往存在一惑的算 法可自动地完成这种判断。 谯系统验证地黢展过程中，先后提出了多种特殊到比较一般地技术，主露有 程序藏确性证明技术、不变量分柝，证明技术、可达性分析技术、符号模型检验 技术等。 其中证明技术出于难以自动化寅现，应用逐非常困难。 潦于可达空间分析的技术容甥实现自动化。宦试图产生和检查系统或协议所 有或部分的可达状淼，进而检验熬于状态或者繁于状态序列的系统性质可达性 分辑嚣法是曩亲生簸舞检验一个特定的初始状态霹达匏蜃霄状态的箕法，烹燮包 括：穷尽搜索( 可麓于达餮1 妒个状态鹃系统) 、受控部分疆索( 可用于这飘l o ” 个状杰的系统) 和随机搜索( 更大的系统) 。由于“状态爆炸”问题，目前旗于 可达激间分析的技术还只能应用予小系统的分析。 符号模型检验技术也有“状i 熬爆炸”问题，瞧由于使用断言语言的不动点理 论，骧及褥号凭翡敬态窝聚言袭瑟装寒( 热o b d d ) ，整它霹潋处理戆状泰室闽 显著掇商，目前己张中型复杂的系统中得到应翊。 7 弱公甲条件下模型检验状态空间的对称化简 2 3 线性时态逻辑( l t l ) 时态逻辑或时序逻辑( t l ，t e m p o r a ll o g i c ) 是模态逻辑的扩展，它涉及含 时间信息( 现在、过去、将来、之前、之后) 的事件、状态及其关系的命题、谓 词和演算。 下面对常用逻辑术语进行简要的介绍，并对一些逻辑符号进行规定： ( 1 ) 命题命题为非真即假的陈述句。 ( 2 ) 个体常量系统中可以识别的独立存在的事物，简称常量。 ( 3 ) 个体变量表示不确定个体常量的符号，简称为变量。 ( 4 ) 量词对个体变量施加限制和约束的词。旖加了量词的变量叫约束变 量，未施加量词的变量叫自由变量。 ( 5 ) 谓词表示个体变量性质或属性的词。其值非真即假。 ( 6 ) 函数多个变量之间的映象关系。函数不能单独出现在逻辑式中，它 必须嵌于谓词中。变量也不能单独出现在逻辑公式中，也必须嵌于谓词中。例如 s e q u e n c e ( m ) = s e q 这个谓词可出现在逻辑式中。 ( 7 ) 项由数学运算符( 十，) 和关系符( ， ，= ) 联 系起来的常量函数称为项。两个项用关系符联系之后，所得复合项的值非真即假。 ( 8 ) 公理作为推理出发点的公式。 ( 9 ) 定理根据推理规则由公理推导( 或证明) 的公式。公理都是定理。 ( 1 0 ) 永真式其值永远为真的公式，又称重言式。 ( 11 ) 原子命题不含任何逻辑操作符的命题。 ( 1 2 ) 原子谓词不含任何逻辑操作符的谓词。 ( 1 3 ) 逻辑操作符对逻辑公式进行操作，或连接，或演算的符号。它分 为一元操作符：一( 非) ；二元操作符： ( 与) 、v ( 或) 、一( 蕴涵) 、一( 等 价) 。 ( 1 4 ) 合式公式按下述生成规则构成的逻辑符号称为合式公式，简称公 式： 1 、值为逻辑值的项，原子命题、原子谓词为合式公式； 2 、如果a 为合式公式，1 a 为合式公式； 3 、如果a 和b 为合式公式，那么a 八b ，a v b ，a b ，a b 也为合式 公式； 4 、如果a 是合式公式，并且x 为自由变量，那么( v x ) a ，( ：i x ) a 是合式 公式； 5 、反复使用以上规则构成的表达式为合式公式。 ( 1 5 ) 一阶谓词逻辑量词只施加于个体变量的逻辑。量词可施加于谓词 名本身的逻辑为高阶逻辑。 时态逻辑对谓词逻辑进行了扩充，增加了时态或时序操作等。这里的时序指 系统状态序列。 1 、时态词( 时态操作) g ( 或口) ：“总是”( a l w a y s ) 或者“今后”( h e n c e f o r t h ) 操作。口a 表 翁公平条件下模型检验状态空同奇臼对称他简 示“a 总是为真”。 f ( 或) ：“菜时”( s o m e t i m e ) 操终。矗表示“蠢融a 为囊”。 x ( 或n ，0 ) ；“下次”( n e x t ) 操捧。o a 表示“a 在系统的下一个状 态( 时刻) 为真”。 u ：“直到”( u n t i l ) 操作。aub 表示“a 一直为舆，直到出现b 为真 为l ”。 常用的复合操作： 口a ：从当前状态开始，系统存在多个状态，a 为真。 口a ：系统存在个状态，从那个状态开始，a 总为真。 o 口a ：扶下令状态开始，a 总是为囊。 ，s 2 ，s o ) ，( s o ，s 1 ) ，s l ， s 2 ) ) ，l ( s 0 ) = a ，b ，l ( s 1 ) = a ，c ) ，l ( s 2 ) = b ，一c ) 。 1 0 弱公平条件下模型撩验状态空间的对称化筒 图加1 一个k r i p k e 结构 3 、计算树逻辑c 俄 c t l 由一系列c t l 公式组成，一个c t l 公式由路径量词和时态算子两部分 组残。踌径基运蠢a ( 对于蘑鸯路径) 窝e ( 存在菜个路聚) ；时态舅予鸯g ( a l w a y s ) 、f ( s o m e t i m e ) 、x ( n e x tt h n e ) 、u ( u n t i l ) 。爨径蕉弱帮嚣于杰葬子 统称为时序逻辑符母，具体含义如下。 a ：对从当前状态出发的所有路； e ：存在从当前状态出发的菜条路径： f ：在指定鼹径上豹将来黧令获态； g ：在指定路径上的所有状态 n ( 或x ) ：襁指定路径上的下一个状态； u ：在指定路径上直到某个谓词成立为止。 状态公式帮爨缀公式壶热下鬏剩生藏： s l ：每个原子命题p 都怒状态公式； s 2 ：若p ，q 是状态公式，则 p 、p a q 、p v q 都是状态公式； s 3 ：若p 燃路径公式，则a p 和e p 都怒路径公式； p l ：每个状态公式p 都怒路径公式； p 2 ：若p ，q 是路径公式，刘强p a q 、p v q 都楚鼹径公式； p 3 ：若p ，q 是路径公式，则f p ，g p ，n p 和p u q 都是路径公式； p 3 ：若p ，q 是状态公戏，则f p ，g p ，n p 和p u q 都是路径公式。 状态公式s l ，s 2 ，s 3 和路强公式p 1 ，p 2 ，p 3 称为双时序语言c t l 。盼溪法 公式； 状态公式s 1 ，s 2 ，s 3 和路径公式p 3 称为分支对序逻辑c t l 的语法公式； 状态公式s 1 和路径公式p 1 ，p 2 ，p 3 称为线性时序逻辑语畜p l t l 的语法公 式。 出上可知，c t l 释p l t l 都怒c t l * 的子谖畜。 下面给出用c t l 公戏描述的一魑常用的系统或协议性质： ( 1 ) a g p ：袭示系统的不变性，该公式可用来说明两个进程不可能同时访 问个资源或系统不会达到死锁状态，通常表承“坏事情永邋不会发生”； ( 2 ) a f a g p ：凌示系绞最终箨整在p 必嶷豹捩态，弱蛮诞明系统失效的次 弱公平条件下模型梭验状态空间的对称化简 数是有限的特性； ( 3 ) a g ( p a f p ) ：表示麸黪窝p 为真熬状态。最终惑缝翻这q 为囊的捩 态，它穗可以表示程经侮状态下只骚由请求，潮系统最终能瓣应请求； ( 4 ) a g a f p ：袭示从任何一个可达状态，熊无限多次进 使得p 为真的状 态。町用来描述从任何状态都能进入到复位状态的系统特性； ( 5 ) a f p ：表示从镪始状态最终总能进入到使p 为真的状态，即表示“好 靛事骛慧会发生” ( 6 ) a g e f p ：袭示p 总是有可能发生的，例如可以表示系统总是可能谶入 剑研；死锁状态。 弱公平条件下模型检验状态空间的对称化简 第3 章模型检验及其状态空间化简 3 1 可达性分析技术 可达性分析是试图产生和检查系统或协议所有或部分的可达状态，进而检验 基于状态或者基于状态序列的系统性质。所谓可达状态是指系统从初始状态开始 经历有限次转化之后可达到的状态，所有可达状态构成了系统可达状态空间。可 达性分析算法是用来生成并检验一个特定的初始状态可达的所有状态的算法，主 要包括：穷尽搜索( 可用于达到1 0 7 个状态的系统) 、受控部分搜索( 可用于达 到1 0 个状态的系统) 和随机搜索( 更大的系统) 。 穷尽搜索是最简单的算法。它分析最为细致，但它只能分析小规模的协议或 系统。如果穷尽搜索算法超过它的极限，会蜕变为受控部分搜索方法，且分析的 质量会显著下降。 受控部分搜索算法可提高穷尽搜索算法所不适用的情况下的搜索质量。它通 过在限定的内存及时间下对所能搜索到的完全状态中的最优部分来实现这项功 能。 随机搜索技术适用于受控部分搜索算法不能应用的系统中。在这些系统中， 系统状态空间的估计值很大，以至于部分搜索技术也不能进行可靠的选择。在这 些情况下，最可能的搜索是在状态空间中进行随机或者是有所侧重的随机搜索。 有两种度量可达性性分析能力的指标：覆盖性和查错质量。覆盖性可由系统 测试的状态数与全部状态空间的状态数之比来进行量化。查错质量可以用所查找 到的不同错误类型在所有错误数中所占的比例来衡量。 1 穷尽搜索 穷尽搜索算法是对系统状态中的所有状态进行遍历。给定系统中的状态可分 为两类：可达状态和不可达状态，一般要求系统中不含有任何不可达状态，不可 达状态应包含所有错误状态。 图3 - 1 为穷尽搜索算法的基本结构。 s t a r t ( ) 过程初始化两组状态集：一组是名为w 的要被分析的一组系统工 作状态集；一组是名为a 的已被分析过的状态集。状态集a 也被称为系统状态 空间，当算法结束时，a 应包含系统所有可达状态。 s t a r t o ( w = i n i t i a l _ s t a t e ；产工作集：还未分析的 a = ( ) ； + 己分析过的状态+ a n a l y z e o ； ) a n a l y z e o ，穷尽或完全搜索+ i f ( w i se m p t y ) r e t u r n ； 弱公平条件下模型检验状态空间的对称化简 q 2 l a s te l e m e n tf r o mw ； a d d q t o a ； i 袖一e r r o rs t a t e ) r e p o r te r r o r 0 ； e l s e t b re a c hs u c c e s s o rs t a t es o f q i f ( 5 i sn o t i n a o r 、价 a d ds t o w ! a n a l y s e ( ) ； ， d e l e t e q f r o mw ： ) 图3 - 1 穷尽搜索算法的基本结构 依据跌集台w 申获褥状态的顺序不同，穷尽搜索算法分为深度优先遍历翱 宽瘦绽凳遗历。翔鬃怒浚先进先逡灏净存取凝悫，舞法葵法藏嶷为宽度谯竞邃掰。 宽度优先遍历其有最先发现最缀错误序捌的优点。深度优先算法其有占用小 的w 空间的优点。对于这一点，一个直观的解释摄：深度优先遍历时，w 的大 小则是搜索树深度的函数，而在宽度优先遍历时，w 的大小则是搜索树宽度的 露数。援索树的最大深度取决予一个单独执行缪列的最大长发，但是越的宽发取 决予肇獭撬 子；亭爰瀚菠太数器，麓赣通常是一个较大戆蓬。 穷尽搜索方法的难要问题是玄的适用性有一定局限。需要耩重指出的楚，完 全状态空间搜索技术的覆盖度并不一定是1 0 0 ，它取决于状恣空间的大小和用 于搜索的存储空间的数量。 当状态空闼令数超遘1 0 8 辩，完全攫索方法会不霹避受悠发生囊渍。下露鼹 一个籁革的计算来说明。 如果是以s 个字节来存储系统状态，并且我们的机器可用内存是m 个字节， 那么能产生并分析的状态数不超过m s 个。m 照一个取决于机器的常量，