（计算机软件与理论专业论文）基于cerl程序的软件模型检测及基工具.pdf

基于c e r l 程序的软件模型检测及其工具 专业：计算机软件与理论 硕士生：林强 指导老师：苏开乐教授 摘要 本文旨在研究软件模型检测及其工具实现，包括模型的表示、检测的算法、 实现方案、案例分析和如何与软件开发过程相结合等问题。本文从模型检测、软 件模型检测的基本理论讲起，深入论述了软件模型检测的重要技术，系统地介绍 了数个对当前软件模型检测影响比较大的检测工具及其技术。 在总结前人的成果后，本文提出了基于c e r l 语言的表达方法，提出了用c e r l 作为中间层的转化式模型检测方案并以从c e r l 到s m v 的转化为例子总结了该方 案的主要问题并给出相应解决策略，提出基于路径谓词的检测方案、算法并给出 优化方法。作者在系统分析s m v 模型检测工具的基础上实现了自己的方案，这里 我们实现如何用s m v 语言来模拟c e r l 语义的算法并把转化式方案和基于路径的 检测方案有机统一起来。在讨论如何使软件模型检测和实际软件开发相结合的问 题时候，我们引入了使用断言机制的方法。 在实验方面，本文对三个比较有代表性的程序作了分析，说明本文工具的实 用性。最后本文对自己的方案的进一步完善和研究进行了简单探讨。 关键词：模型检测，软件模型检测，s m v ，s p m ，布尔程序，c e r l 程序 s o f t w a r em o d eic h e c kin ga n dt o oisb a s e do nc e r l p r o g r a m l i n q i 粕g m 句o r ：c o m p u t e rs o f t w a r ea 1 1 dt h e o r y s u p e n 嚏s o r ：s uk a i l ep r o f b s s o r a b s t r a c t i t lt h i sp a p e rw ef o c u so nt h es t u d yo ft h es o m 矿a r em o d e lc h e c k i n ga 1 1 di t st 0 0 1 s 中山大学硕士研究生毕业论文 基于c e r l 程序的软件模型检测及其工具 i n c l u d m gm o d e lr e p r e s e n t a t i o n ，c h e c 妯n ga l g o t m ，i m p l e m e n t a t i o n ，c a s es t u d ya l l d t h ec o m b i n a t i o no fm o d e lc h e c k i n ga n ds o 胁盯ed e v e l o p m e n tp r o c e s s t h i sp 印e r s t a r t sw i t ht h ee s s e n t i a lm e o r yo fm o d e lc h e c l 【i n ga 1 1 ds o f t 、v a r cm o d e lc h e c k i n g ，t a l k s a b o u tt l l ei m p o r t a n tt e c l l n i q u e si ns o n w a r ei n o d e lc h e c l 【i n g ，a i l dt h e ni t g i v e sa s y s t e m i ci m m d u c t i o no f s e v e r a lf h m o u sm o d e lc h e c k i n gt o o l sa l l dt l l e i rt c c h n i q u e s a f t e rs 眦m 撕z i n gt h ef u l 丘l l m e n t s0 fo t h 盯p e o p l e ，m i s 枷c i ep u t sf o 刑a r dt h e s o f h a r er n o d e l d e s c 啦) t i o n m e m o db a s e do nc 腿l( c o 眦o ne l e m e n t r 印r c s e n t a t i o nl a l l g i l a g e ) l a l l g i l a g e ，t h ec o n v e r s i o nm o d e lc h e c k i n gs c h e m eu s e d c e r la sm ei n t e m e d i a t el a l l g i l a g e w 色u s et h ec e r lt os m vt m s l a t i o na sa n e x a n 叩1 et oe x p l a i nm em a i np r o b l 锄si n “ss c h e m ea 1 1 dt h e i rs 0 1 u t i o n s w ea l s o d i s p l a yt l l em o d e lc h c c k i n gs c h e m eb a s e do np a t hp r e d i c a t e s ，c h e c k i n ga l g o r i m ma 1 1 d o p t i m i z e dm e t h o d w ei m p l e m e n to l l rs c h e m eo nt 1 1 eb 踮i so ft h ew o r ko fs m v m o d e lc h e c k e lw ei r n p l e m e n th o wt ou s es m v l a n g u a g et os i m u l a t em es c m a l l t i co f c e r l1 a 1 1 9 l l a g e w h e nt a l k i n ga b o u tm ep r o b l e mo ft h cc o i n b i n 撕o n0 fs o f t w a r e m o d e lc h e c k i n ga n ds 0 脚a r ed e v e l o p m e n tw ei m p o r tt h ep r o p o s a lu s i n ga s s e r t i o n w eh a v eac a s es t i l d yo nt h e r ec l a s s i cp m g m m si no r d e rt od e m o n s t r a t et l l e p r a c t i c a b i l i t yo fo l l rt 0 0 1 _ f i n a l l yw ed i s c u s sm ep r o b l e mo fc o n s 眦吼a t t i n ga i l d e x t e n d i n go u r r e s e a r c h k e y w o r d ：m o d e lc h e c k i n g ，s o f t v r a r em o d e lc h e c k i n g ，s p n ，s m v b o o l e a np r 0 蹦u n ， c e r lp r o 伊柚 i i 中山大学硕士研究生毕业论文 基于c b r l 程序的软件模型检测及其工具 引言 模型检测u 作为一种自动化验证方法，在硬件检测和协议验证等领域得到了 广泛的应用。模型检测需要两个输入：一是系统，我们需要验证其正确性的一个 系统；二是规范，该系统应具有的性质。模型检测中最大的挑战就是状态空间的 爆炸问题。这个问题源于系统中有许多相互作用的部件，或者系统中有复杂的数 据结构，而且这些数据结构可以有许多不同的取值。在这种情况下系统状态的数 目将变得十分巨大。模型检测的实质就是检测系统和规范两者的一致性。 模型检测技术的一大优点就是我们可以利用它进行自动化的验证。模型检测 工具通常使用一种对系统的状态空间穷举搜索的过程决定某些规范是否为真。给 予足够的资源，模型检测工具总是以y c s ，n o 作为回答而终结。这种方法已经成功 应用于许多复杂的电路设计和通信协议验证工作，目前主要用来检测使用时态逻 辑描述的规范。模型检测工具主要有s m v 【”，s p 玳【2 纠等。 当前，软件质量跟不上实际的需求给社会经济带来很大的损失，2 0 0 2 年美 国国家标准与技术研究所( n a t i o n a lm s t i t u t co fs t a n d a r d & t e c l u l o l o g y ) 发表了一个 调查报告一t l l ee c o n o m i ci m p a c t so fi n a d e q u a t eh l 丘a s t m c t u r ef o rs o f t w a r et e s t i n g ， 该报告翔实地论述了软件质量保证手段不足对经济的影响。软件模型检测则是有 效提高软件质量的技术，因此它成为了模型检测研究中的一个热点问题，欧美各 大高校、研究机构及软件公司都有从事这个方面的研发。本文就是我们在总结当 前软件模型检测领域有影响的理论和技术的基础上，对自己的所做的一些研究工 作的总结。 本文在总结程序设计语言的基本特征后定义了一套语言一c e r l ( c o m m o n e l e m e n tr 印r e s e t l t a t i o nl 脚罂l a g e ) ，使用该语言作为软件模型检测输入的系统描 述语言，对软件模型检测问题进行研究。我们提出了基于c e r l 的软件模型检测 方案和从c e i u 到s m v 的转化方案，并对该方案加以实现，通过实验来验证我 们的结论。 本文的结构如下：在第1 章中介绍了模型检测，软件模型检测的有关概念和 基本问题。在第2 章中介绍了数个当前比较流行的( 软件) 模型检测工具并总结 了它们的关键技术。第3 章中我们提出了自己的c e r l 程序模型检测方案，我们 以c e r l 到s m v 的转化为例说明转化式检测方案的主要问题及对策。第4 章对 我们的方案的系统实现做了详细介绍，我们的实现方案体现了两个方案的内在统 一。第5 章中我对三个实例程序作了分析，给出了实验的结果。第6 章我们对我 们的方案的进一步研究做了简单探讨，提出了一些研究设想。 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 第1 章软件模型检测技术概述 l1 模型检测 模型检测【1 作为一种自动化验证方法，在工业界已经得到广泛的应用。模型 检测需要两个输入：一一是系统，需要我们验证其正确性的一个系统；二是规范， 该系统应具有的性质。模型检测中最大的挑战就是状态空间的爆炸问题。这个问 题源于系统中有许多不同部件的交互，或者系统中有取值范围很大的复杂数据结 构，在这种情况下系统状态的规模将变得非常庞大。 模型检测技术的一大优点就是我们可以利用它进行自动化的验证。模型检测 工具通常使用种对系统的状态空间穷举搜索的过程决定某些规范是否为真。给 予足够的资源，模型检测工具总是以y e s n o 作为回答而终结。这种方法已经成功 应用于许多复杂的电路设计、通信协议和软件验证工作，目前检测的规范主要是 用时态逻辑( 或其扩展逻辑) 来描述的。 1 1 1 模型检测的过程 模型检测一般由以下几项任务组成。 第一项任务是建模，即把一个设计转化成模型检测工具能够接受的形式。在 许多情况下这仅仅是一项编译工作。由于时间和内存的局限，一个设计的建模可 能必须用抽象的方法减少不相关或不重要的细节。 第二项任务是给定规范，即在验证之前，要说明设计必须满足的性质。这个 规范通常以逻辑的形式给出。对硬件或软件系统，通常使用时序逻辑，这种逻辑 能够断言系统随着时间演变的行为变化。对本文的软件模型检测也是如此。 对于规范的一个重要的问题是完备性。模型检测提供了一种方法检测一个设 计模型是否满足一定的设计规范，但不可能确定给定的规范涵盖了系统应满足的 所有的性质。 最后是验证实施过程。在理想情况下验证是完全自动化的。但是，在实际应 用中常常需要人的参与。最常见的人工活动是验证结果的分析。为了证实否定的 结果，常常需要把出错的路径呈现给用户。否定结果可以做为测试属性的反例， 并能帮助设计者跟踪到出错的地方。在这种情况下，通过分析错误路径可能要求 对系统修改或重写模型检测的算法。 产生错误的路径也可能是因为不正确的系统建模或是不正确的规范要求。错 误路径也可用于发现和修补这两类问题。最后一种可能是验证任务可能会不能正 常终止，因为模型规模太大以致于不能装进计算机内存。在这种情况下，可能需 要更改模型检测工具的参数或调整模型后重新验证。 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 1 1 2 系统建模 我们说一个状态是系统在一个特定时间点的一个快照或是当前的系统描述， 我们还需要知道系统状态的值如何随着系统的动作而变化。这可以通过刻画系统 在动作发生前和动作发生后的状态来描述系统的改变，这样的状态对决定了系统 状态的迁移。我们使用状态转换图k r i p k e 结构来描述系统的行为。 个硒p k e 结构1 ，1 0 1 包含以下几个部分：一个状态集，一个状态之间的迁 移集，一个标记函数，利用在某个状态下为真的属性来标记该状态。k r i p k c 结构 中的路径用来模拟系统的计算。虽然这些模型非常简单，但在对系统进行推理时 它们有足够的表达能力。以下我们给出用来建模系统的k f i p k e 结构的形式化定 义。 定义：设a p 为个原子命题集，一个在a p 上的k p k e 结构m 是一个四元组 m = ( s ，s 。，r ，l ) ： 1 s 是有限状态集 2 s 。是s 的一个子集 3 r s s 是一个传递关系，且必须是完全的，即，对于每一个s s 都存在一 个状态s s 满足r ( s ，s ) 4 l ：s 斗2 ”是一个函数，该函数对每一个状态用在该状态成立的原子命题集 进行标记。 如果对初始状态没有特殊的要求，可以省略s 。，这样k r i p k e 结构m = ( s ，r ，l ) 将是一个三元组。 1 1 3 二叉决定图 二叉决定图【2 1 可以符号化表示有限状态系统，这为我们在计算机上模拟有限 状态系统提供了一种方法。在这一节里，我们首先讨论如何用二叉决定图表示布 尔函数。布尔函数定义在o 和1 上，0 代表f a l s e ，l 代表t m e 。我们将看到二叉 决定图可以直观有效的表示布尔函数。然后我们讨论如何用二叉决定图编码 k r i p k e 结构，这样我们就可以在计算机上表示我们的系统，进行计算机辅助验证。 我们将看到利用二叉决定图进行符号化模型检测可以处理规模巨大的系统。 有序二叉决定图( 以下简称0 b d d ) 是布尔公式的一种规范形式表示1 2 】。这 种表示通常比传统的合取范式或析取范式更紧凑，而且对o b d d 的操作也非常 有效率。因此0 b d d 广泛应用在计算机辅助设计中，包括信号模拟，组合逻辑 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 验证，最近也开始用于有限状态并发系统的验证。 为了讨论二叉决定图，我们首先考虑如何生成一棵二叉决定树。二叉决定树 是一个有根的有向树，它由两类结点组成，终结点和非终结点组成。每一个非终 结点v 由一个变量v 缸( v ) 标识，它有两个后继结点：l o w ( v ) 对应变量v 被赋值成 为。的情况，h i 曲( v ) 对应变量v 被赋值为1 的情况。每一个终端结点v 被表示为 v a l u e ( v ) ，v a l u e ( v ) 要么是o 要么是l 。 考虑布尔函数f ( a 】，a 2 ，b l ，b2 ) = ( a l b 1 ) ( a2h b 2 ) 表示的二位比较器，该 比较器由布尔公式( a 1hb 。) ( a ：hb ：) 定义，其二叉决定树表示如下图： 图1 1 ：( a l 付b 1 ) ( a 2hb 2 ) 的二义决定树 从树的根结点出发到终端结点，我们可以确定该路径上对变量的真值赋值是 否使该二叉决定图表示的布尔公式为真。如果变量v 被赋值为o ，那么从根结点 到终端结点的路径上的下一个结点将是l o w ( v ) 。如果v 被赋值为1 那么路径上的 下一个结点将是l l i 曲( v ) 。标识终端结点的值是该布尔函数在此路径赋值下的值。 例如，赋值 通向标号为o 的叶子结点；因此布尔公式 ( a ，b ，) ( a ，b ，) 在这个赋值下为假。 二叉决定树并没有为布尔函数提供简明的表示，实际上，二叉决定图跟真值 表的规模大小相同。同时，我们看到在二叉决定树中通常有许多冗余。例如，图 1 1 所示的二叉决定树中，有八棵根结点标识为b 2 的予树，但只有三棵子树是不 相同的。因此，合并同态的子树可以得到布尔公式的更简练的表示。合并的结果 是一个有向无环图，我们称之为二叉决定图。更准确的说，一个二叉决定图是一 个有根的有向无环图，它有两种结点，终端结点和非终端结点。与二叉决定树相 似，每一个非终端结点v 由一个变量v a r ( v ) 标记，有两个后继结点，i o w ( v ) 和 h i 曲( v ) 。每一个终端结点标记为0 或l 。每个以v 为根的二叉决定图b 确定一个 布尔函数l ( x ，x 。) ，方法如下【2 】 d 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 1 如果v 是一个终端结点 2 如果v a l u e ( v ) = l 那么f v ( x ”，x 。) = 1 。 3 如果v a l u e ( v ) = 0 那么f v ( x ”，x 。) = 0 。 4 如果v 是一个非终端结点，v a r ( v ) = 】【。，那么0 是一个函数 f v ( x ”，x 。) = ( 1 x i f k v ) ( x l ，x 。) ) v ( x f h 讪 ，) ( x 1 ，x 。) ) 。 上述方法得到的二叉决定图，对一个布尔公式的表示并不唯一。我们引入两 个约束可以得到布尔公式的标准表示。第一，对于每一条从根结点到终端结点的 路径变量都以相同的次序出现。第二，在图中没有同态和冗余的结点存在。引入 这两个约束得到的二又决定图，我们称之为有序二叉决定图( o b d d ) 。b r y a n t 【2 】 讨论了获得o b d d 的方法，并给出了一个以自底向上方式工作的称为“归约” 的程序实现，该程序运行时间与二叉决定图大小成线性关系。对图1 1 所示的二 叉决定树，如果我们使用顺序a l b l a 2 l 。 为了用o b d d 表示q ，我们对d 中的元素进行编码，使用一个双射妒：( o ，1 ) 1 寸d ， 把每个长度为m 的布尔向量映射到d 中的一个元素使用编码矿，我们根据以 e 中山大学硕士研究生毕业论文 基于c e r l 程序的软件模型检测及其工具 下的规则建立m n 元的布尔关系0 ： q ( x 。，x 。) = q ( 妒( x ，) ，( x 。) ) 其中，x ；是由m 个布尔变量构成的向量，用于对在d 上取值的变量x 。进行 l 编码。现在可以用o b d d 表示q ，因为该o b d d 由q 的特征函数f 0 确定。这 一技术可以方便的扩展到不同的域d ，d 。上。而且，由于集合可以看成是一个 一元关系，该技术也可以用来表示集合。 现在考虑k r i p k e 结构m = ( s ，r ，l ) 。为了表示这个结构，我们必须描述状态 集s ，迁移关系r 和映射l 。对于状态集s ，我们首先需要对这些状态编码，为 了简单起见，我们假设这里恰好有2 ”个状态。和上述讨论一样，我们假设 ：( o ，1 ) ”寸s 为把布尔向量映射到状态的函数。由于每个赋值都是s 中一个状态的编码， 表示s 的特征函数就是取值为1 的o b d d 。对于迁移关系r ，我们使用与状态同 样的编码。我们需要两个布尔变量集，一个表示开始状态，另一个表示迁移的最 终状态。如果迁移函数编码成布尔关系食( i ，_ ) ，那么r 由特征函数k 表示。最 后，我们考虑映射l ，尽管l 定义为从状态到原子命题子集的映射，把它看成从 原子命题到状态子集的映射将更方便。原子命题p 被映射到状态集 slp l ( s ) ) 。 我们称这些状态集为l 。，该状态集可以用上述编码庐表示。我们用这种方式分 别表示每个原子命题。 1 1 4 不动点及其计算 我们知道，在c t l 模型检测过程中，不动点( f i x p o i n t ) 【1 1 的计算是十分重要 的。设m = ( s ，r ，三) 为一个任意的k p k e 结构，集合p ( s ) 为s 的幂集，同时它 也代表该集合所根据集合的包含关系形成的格。任何j p ( s ) 的元素s 可以认为是 s 上面的一个谓词，即对所有s 包含的状态谓词取真，其它状态则取假。任何把 p ( s ) 映射到尸( s ) 的函数被称为谓词转换器。设f ：p ( s ) 呻p ( s ) 为一个谓词转换 器，则 ( 1 ) f 称为单调的，则若尸立q 则有f ( 尸) f ( q ) 。 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 ( 2 ) f 称为u 连续的，则如果b b 则有f ( u ，异) = u ，f ( 卑) ； ( 3 ) f 称为n 连续的，则如果e 芝i 则有r ( n ，只) = n f f ( 鼻) ； 对于k r i p k e 结构m = ( 只月，工) ，我们有下面的定理，这些为最小不动点 ( 胆f ( z ) ) 和最大不动点( u z r ( z ) ) 的计算奠定了理论基础。 定理1 1 1 】：假如k p k e 结构中的s 是有限的而且f 是单调的，则同时r 也是u 连 续和n 连续的。 证明：略。 定理1 2 【1 】：如果f 是单调的，则对每个整数i ，有f ( 凡b p ) f “1 ( 而厶g ) 和 f ( z h p ) jr “1 ( z h p ) 。 证明：略。 定理1 3 ：如果f 是单调而且s 是有限的，则存在一个整数f 0 对所有f 0 有 f 。( 心厶p ) = f ( 凡括0 。类似地，也存在一个整数。对所有，。有 f ( z 地e ) = f “( 丁h p ) 。 证明：略。 定理1 4 【1 ：如果f 是单调而且s 是有限的，则存在一个整数乇有 ，层r ( z ) = f ( ，h b p ) 。类似地，也存在一个整数五有u z f ( z ) = f ( 7 h p ) 。 证明：略。 对于c t l 公式f 的模型检测，公式f 也对应了尸( j ) 上的一个谓词 川m ，s 净n ，则c t l 中每个操作符都可以表示为某些谓词转换器的不动点运 算。下面给出这些结果，有兴趣的读者请参考原文献 ”。 彳巧= 肜z v 臌吲= 肛工v 脚 a 研= 泌 a 磁 4 l 兀 = 肛 v ( 工n a 踢) 4 尽厂2 】- u z n ( v 丘核) e 姒= 泌 脚 研工【犯】= 胆以v ( l 漓z ) 研z 班】= 泌以 ( _ v z 渊z ) 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 另外，为了应用上述定理，有关的谓词转换的迭代过程需要满足单调性的要 求，关于这些运算单调性的证明本文不列出。请感兴趣的读者参考文献【”。 1 2 软件的验证理论基础 讨。 为了研究软件模型检测的问题，我们有必要先在理论上对此问题做一些探 1 2 1 串行与并行程序 软件的验证包括串行( s e q u e m i a l ) 程序验证和并行( c o n c u r r e n t ) 程序验证两大部 分，先说明它们两者的一些特点。 串行程序的特点是： ( 1 ) 通常运行会终止而得到最后的结果。 ( 2 ) 可以理解为一个黑盒子，如下图 x z 。 l l y 图1 3 ：串行程序的黑盒模型 ( 3 ) 可以通过输入输出的关系来说明，记输入输出关系函数为r ( x ，z ) 。例如z = 1 + 3 + + ( 2 x 1 ) ，则这个函数的关系可以写成r ( x ，z ) ：z = x 2 。 并行程序的基本特点是： ( 1 ) 并行程序通常不是获得一个最终的结果，而是维持与它所在的环境的持续的 交互。 ( 2 ) 一般情况下不会终止。 ( 3 ) 与环境的交互是并行程序最重要的功能。 ( 4 ) 并行程序的行为是我们所关注和要验证的。 一般地，串行和并行程序都可能是有有限或者无限状态的，当前流行的一种 研究方法就是用d e d u c t i v em c t h o d s 方法来验证无限状态程序，用基于算法的方法 验证有限的程序。 1 2 2 软件验证的基础概念 历史上，对串行程序的研究是从形式化验证f o n n a lv e r i f i c a t i o n 技术开始的， f 1 0 y d 在1 9 6 7 年的文章定义了串行程序验证的主要问题和概括了该方法的主要 原理： ( 1 ) 使用不变式( i n v a r i a n t s ) 来证明程序的部分正确性( p a r t i a lc o r r e c t n e s s ) 。 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 ( 2 ) 利用良构序函数( w e l l 一f o u n d e dr a n k i n gf u n c t i o n s ) 来确定程序的终止性 ( t e r m i n a t i o n ) 。 为了进行软件的验证检测，我们的理论应该包括以下的一些要素。 ( 1 ) 编程语言( p r 0 铲蛐i i l i n gl a l l g u a g e ) ，它用来描述待验证的系统。 ( 2 ) 规范描述语言( s p e c i f i c a t i o nl 姐g u a g c ) ，用来指明待验证的属性。 ( 3 ) 验证的方法学( v c r i f i c a t i o nm e t h o d o l o g y ) ，即对给定一个系统s 和属性i ，证 明s 户i 。对于任何验证的方法学，我们必须考虑其中的两个重要问题，也就是： 1 ) 可靠性( s o u n d n e s s ) 问题。 2 ) 完备性( c o m p l e t e n e s s ) 问题。 1 2 3 几种类型正确性的概念 对于同一软件模型，我们在不同的基础和假设上对其正确性验证，因此正确 性也有不问的概念。假定b 是一个谓词逻辑的基( b 勰i s ) ，占为该基上的一个解释 函数，为相应的状态集合。s 为程序，m 。( s ) 为程序s 的语义函数，妒：_ b d o f 和沙：斗b d d f 为分别称为前提条件和后置条件的两个谓词。则： ( 1 ) 对于谓词p 和y ( 在| 9 的解释下) s 称为部分正确的( 5 】，则对所有状态仃： 若妒( 盯) = 丁h e 和m 。( s ) ( 盯) 有定义则妒( m 。( s ) ( 盯) ) = m e 。 ( 2 ) 对于谓词妒和y ( 在| 9 的解释下) s 称为终止的 5 】，则对所有状态盯： 若p ( 仃) = 丁h e 则m 。( j ) ( 盯) 有定义。 ( 3 ) 对于谓词p 和y ( 在| 9 的解释下) s 称为完全正确的【5 】则对所有状态盯： 若妒( 盯) = z h e 则m j ( s ) ( 盯) 有定义和y ( m 口( s ) ( 仃) ) = z h p 。 上述3 个概念把程序验证的最主要问题定义出来了，从定义中可以看出：部 分正确性+ 终止性= 完全正确性。另外，对于“终止性”，它实质等价于图灵机 的停机问题，也就是说它本身是“半可判”的问题。因此完全正确性也是不可算 的问题。本文在此不对这些问题展开，有兴趣的读者请参考支献 翻。 1 2 4 用不变式证明部分正确性 证明部分正确性的经典方法是f l o y d 的归纳断言( i n d u c t i v ；a s s e n i o n s ) 方法f 5 】o 该方法要求用户找出程序位置标签的一个集合，然后让每个位置标签跟一个断言 关联起来，这个集合称为割点( c u t p o i n t s ) 集，割点集必须包含程序中所有的循环。 通常每个割点关联的断言是表明程序执行到该割点的时候的特征。 中山大学硕士研究生毕业论文 基于c e r l 程序的软件模型检羽l 及其工具 假定b 为谓词逻辑的基，p ，g 峨为两个公式，s 为一程序，1 9 为b 上的 一个解释。则证明s 相对于p ，g 的部分正确性( 在0 的解释下) 的归纳断言方法如 下【5 ： ( 1 ) 选择所有出现在s 的语句标签1 a b e l 的一个子集c ，使得首尾两个标签厶， 都在c 中并且s 中的每个循环至少包含c 中的一个元素，我们称c 中的 元素为割点( c u t p o i n t s ) 。c 中的元素可以理解为s 的一个抽象的轮廓。 ( 2 ) 对c 中每个元素，把一个公式g ，阡下瓦与它关联起来，也就是p 和割点，。 关联，g 和割点关联，其它割点则是另外合适的公式，只要步骤( 3 ) 可 以顺利执行，这些公式可以是任意的。如果一个割点，包含在一个循环里 面，则其关联的公式称为不变式( i n v 撕a m ) 。 ( 3 ) 对s 中每条路径口= ( f 。，z 。) ，| 1 ，其中，0 ，c ，。萑c ，验证 从如开始由条件乱经过口的执行后，吼是成立的( 在| 9 的解释下) 。 1 2 5 用序函数( r a n k i gf u b c t i o n ) 证明终止性。 证明终止性的常用方法是w e l l f o u l l d e d 集方法【5 】，它的主要思想是“单调有 界必有极限”的思想。由亍w e l l 一f o l l i l d e d 集的存在，我们可以得到与每个位置标 签相关的公式不会存在一个无穷递降的循环，从而表明程序的执行最终是会停止 的，所以证明了终止性。 假定b 为谓词逻辑的基，p ，g 呱为两个公式，s 为一程序，1 9 为b 上的 一个解释。则证朗s 相对于办g 的终止性( 在口的解释下) 的w e l l - f o u n d e d 集方法 如下 5 】： ( 1 ) 选择所有出现在s 的语句标签l a b e l 的一个子集c ，使得首标签，0 在c 中 并且s 中的每个循环至少包含c 中的一个元素。 ( 2 ) 对c 中每个元素，把一个公式g ，峨与它关联起来，也就是p 和割点f o 关联，其它割点则是另外“适当”的公式。 ( 3 ) 对s 中每条路径口= ( f o ，i ) ，七l ，其中毛，c ，t 一仨c ，验证 从f o 开始由条件“经过口的执行后，吼是成立的( 在口的解释下) a ( 4 ) 选择c 的一个子集c 1 ，使s 的每个循环中至少包含c 1 的一个元素。 ( 5 ) 选择一个合适的w e l l f o l l l l d e d 集( w ，) 。 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 ( 6 ) 给c 1 的每个元素，关联一个函数晶：斗矽，该函数把所有的状态都映射 到w e l l f o l l l l d e d 集上。 ( 7 ) 对s 中每条路径口= ( z 。，) ，尼1 ，其中f 0 ，c 1 ，崔c 1 ，证明 对所有状态盯寸有：若| 9 ( 吼) ( = t n l e 和m 8 ) ( 盯) 是有定义则 g ( 目( j ) ( 盯) ) 亡g ( 盯) 。 证明终止性的w e l l f o l h l d e d 集方法的前3 个步骤除了割点的集合c 不包括最 后一个标签l 外，是与归纳断言方法一样的。由于w e l l 一f o u n d e d 集上无非构造无 穷的下降序列，所有该方法能证明执行的路径不能是无限长的( 即类似单调下降 而且有下界，则必有极限的情形1 。 1 3 模型检测中的流行技术 1 3 1 偏序归约 偏序归约是模型检测中非常有效和最常用的压缩状态空间技术，在此我们有 必要做一些简单介绍。 偏序归约就是把完全的状态图映射到一个归约过的同时又保留在完全图中 状态的有关属性的状态图。如果归约过的图耗费更少的内存空间或者能被更快的 遍历，则这样的方法值得一试。 考虑如下的例子： 图l 一4 ：可被归约的一个例子 这个状态图由4 个状态和4 个迁移关系组成。迁移上的标识表明该迁移对应 的过程。该图有两个完全路径( 从初始状态出发并且不能在扩展的路径) ： s o ，s 1 ，s 3 和【s o ，s 2 ，s 3 】。假如中间状态是与待检测的属性无关的，我们只需跟踪 这两个路径中的一个即可。假如这里迁移a 和是可以交换的。他们可以按任何 顺序执行并且与他们的遍历顺序是无关的。因此完全的状态图可以被归约为一个 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 仅包含一条路径的归约图。 如果在构造归约图的时候，我们需要构造个完全的状态图，这样我们并不 能够减少内存的消耗，因此本文将介绍一种方法，它不需要构造完全状态图就能 构造归约图。 使能( e n a b l e d n e s s ) ，可交换性( c o 咖u t a t i v i t y ) 和独立性( i n d 印e n d e n c e ) 是偏序归约中的重要概念【”，使能，可交换性和独立性是识别哪一个迁移可以在 归约图上省略，哪一个迁移必须保留的准则。我们这里给出它们的基本定义。 定义：迁移过程 和f ，是可交换的谁对所有状态s 满足： ，f 2 ) 互p n 6 姒s ) ，r 1 ( 2 ( s ) ) 2f 2 ( f 1 ( s ) ) 在图l 一4 中口和卢是可交换的。这个定义意味着对任意状态s 如果，f ：不 是同时都是“使能”的，则它们不是可交换的。 定义：迁移过程 和“是独立的i f r 它们是可交换的并且它们不会互相影响而使 对方不处于“使能”状态。 由此有迁移进程 和f ，是独立的证对所有状态s 满足： ，f 2 ) 互鲫口6 z b 烈s ) ， p 玎口6 如战f 2 ( s ) ) a n df 2 e 胛6 2 8 d ( f l ( s ) ) a i l df 1 ( f 2 ( s ) ) ：f 2 ( ( s ) ) 。 在图1 4 中a 和口是独立的。 定义：迁移过程和f ：是依赖的i 疗它们是非独立的。 定义：进程p l 与p 2 是独立的i f r 所有p l 的迁移和所有p 2 的迁移是独立的。 可见性是偏序归约中，用于定义迁移对命题的作用的概念。它反映了迁移簇 ( 迁移的一个集合) 对命题c 的影响。 定义：一个迁移簇t 对命题c 是可见的i f r 出现c p 陀咕妇缸t ) ) 君p f - 眦l f b ( t ) ) 定义：一个迁移簇t 对命题c 是不可见的濉它对c 是非可见的。 在图1 5 的例子中，假定我们检测某个仅在j 。为真的命题。迁移( s 0 ，s 1 ) ，( s o ， s 2 ) ，( s 1 ，s 3 ) ，( s 2 ，s 3 ) 都是对该命题不可见，而迁移( s 1 ，s 4 ) 则是可见的。 中山大学硕士研究生毕业论文 基于c e r l 程序的软件模型检测及其工具 图1 5一个对s 4 可见的迁移图 i n v i s i b l en a n s i t i o n v i s i b l en l m s i t i o n 归约其实是一种抽象技术，因此对同一原始的图，归约后的图不是唯一的， 我们把归约后的图称为归约图。同时我们称所有从初始节点出发到没有出度的节 点为止的路径为完全路径。则所有图1 5 中的完全路径总共有如下两种情况： ( 1 ) 初始时候不出现s 4 后来出现s 4 。 ( 2 ) 从来就不出现s 4 。 所有完全路径遍历的个别状态会有不同，但是都表达了上面的某一种模式。 由于命题在非s 4 的状态下没有差别，这就不能区别路径【s o ，s 1 ，s 3 和 s o ，s 2 ，s 3 。 这个完全状态图就可以被归约为一个省略了某些不能被区别的路径的归约图。下 图是一个归约图的一种可能的情形。 图1 6 ：图l 一5 的可能的一种归约图 另一种可能的归约图如下： 图1 7 ：图l 一5 的可能的另一种归约图 相对而言，图1 6 会更加优越些，因为它拥有更少的迁移和更少的状态节 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 点数。但是在实际的情况下，我们不能总是可以获得最优的归约图结构。我们反 而对获得较大( 非最大) 的归约程度( 即次优类结构) 比较感兴趣。 a l p l e ( s ) 集合的计算是确定模型检测过程中系统扩展路径的重要步骤，也是 影响归约效果的重要步骤。即产生一个归约图时候，我们用可达状态集合 彻担触域s ) 的一个子集来代替它，也就是我们所说的锄p l e ( s ) 集合。因此有： 锄1 p l e ( s ) 冬e n a b l e d ( s ) 定义：状态s 是被完全扩展讧r 它的a i l l p l e ( s ) = c i l a b l e d ( s ) 。 我们用一套规则来决定e n a b l e d ( s ) 中的元素在锄p 1 s ) 集合中的去留问题。在 决定a n l p l e ( s ) 是否应该包含一个迁移的时候，我们应该以“迁移的去除不丢失与 属性相关的行为”为依据。 在c 1 a r k e ，g r 哪b e r ga i l dp e l e d 的 南比，国e 战垤的1 4 7 页中有一个关于获 得锄p l e 集合的方法的介绍，具体如下： m l ec o ：a m p l e ( s ) = ai f r e l l 西l e d ( s ) = 0 n l l e c l ：从状态s 出发的完全状态图中的每条路径，如下条件必须满足：一个依 赖于a 坼，蜮s ) 中的某个迁移的迁移不能在口，即何s ) 的迁移没有执行前执行。 m l ec 2 ：假如状态s 没有完全扩展，则每个迁移a 锄p l e ( s ) 是不可见的。 m l e c 3 ：个循环路径中如果包含一个有某些迁移a 处于“使能”的状态，但是 “从来没有被包含到循环上某些状态的姗p 1 “s ) 集合中，这样的循环是不允许的。 从这条规则可以获得的一个重要结论是铋a b l e d ( s ) 一锄p l e ( s ) 中的所有元素 独立于a n l p l e ( s ) 中的所有元素。 证明：假定存在一个迁移t 1 e n a b l e d ( s ) ，它依赖于迁移t 2 锄p l e ( s ) 。 t 1 因此不能在a i l l p l s ) 的某一迁移执行前被执行。反之，假如t l 是先执行的，则 它必然被包含在锄p l e ( s ) 中。 r u l ec o 防止归约图在完全状态图中没有终止状态的情况下出现终止状态。 r u l ec 1 是目前最复杂的规则，它应用到完全状态图的每条路径。c 1 a r k e ， ( 删m b e r ga i l dp e l e d 川提供了仅仅考虑同一进程( 被检测对象中的进程) 的不同 迁移对之间的依赖关系和不同进程之间共享同一变量的进程之间的迁移的依赖 关系而不是所有进程之间的所有迁移的关系。因此可以避免在完全构造状态的后 构造锄p i e ( s ) ，从而具育较低的计算复杂度。 最后，我们可以对偏序归约中的技术进行概括性的理解。进行归约时候，那 些前集和后集对的命题的真假有不同影响的迁移( 即上述可见迁移) 的前集和后 集肯定会处于在归约后的路径不同的“片断”中( 即它们的差异不能忽略) 。由 于模型检测是基于状态片断的访问序列的，如果归约过程满足所有访问的片断序 列被保留的前提，则这个归约是正确的。因此为了说明一个归约方法的正确性， 只需说明完全状态图中的任何的“片断”序列都在归约图中存在。这个是我们构 中山大学硕士研究生毕业论文基于c e r l 程序的软件模型检测及其工具 造归约方法时候必须遵守的原则。 1 - 3 2 o n t h e n y 验证技术 可达性分析是对一个系统中所有可能达到的状态和迁移进行穷举遍历的验 证技术。o n t h c - n y 技术基于这样考虑的可达性分析技术：进行可达性分析，不 需要存储全局系统所有的状态。事实上，对于多数实际问题的规模的系统状态爆 炸问题都已经使构造完全的状态图变得近乎不可能。因此我们更倾向于模拟所有 系统能够执行的迁移序列就足够了。一个经典的深度优先搜索就可以o n t 1 1 e n y 地遍历该系统，也就是不存储在遍历过程中所发生的迁移。这大大减少了对内存 的需求 1 5 对于图的深度优先搜索，最小的存储需求就是遍历的当前路径，这样的搜索 算法大大减少了内存空间的需求但是还能保证对整个状态空间的遍历，然而所需 要的时间将会大大增加，因为我们需要重新生成那些已经访问过的节点。深度优 先搜索的另一极端，在遍历时候一个访问到新的节点就把它存储起来，这样会把 需要的时间减到最少，但是需要存储所有的可达状态。然而对大规模的可达图而 言，存储所有的状态是不太可能的。因此尝试在这两种策略之间取得折中的各种 方法都被提出来了