（计算机应用技术专业论文）基于vhdl的模型检查应用与实现.pdf

上海大学硕1 ：学位论文 摘要 随着计算机软硬件系统规模的日益复杂化、重要化，如何保证计算机 系统的正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问 题。长期以来，常用的系统设计检验方法是以经验为基础的测试方法。但 是，测试方法只能证明错误的存在，但不能证明错误的不存在，所以，对 于高可靠性系统来说，测试方法有明显的局限性。 在过去二十多年间，各国研究人员为解决这个问题付出了巨大的努 力，取得了重要的进展。在为此提出的诸多理论和方法中，模型检查( m o d e l c h e c k i n g ) 以其简洁明了和自动化程度高而引人注目。 本文旨先介绍了模型检查技术的基本思想、研究方向和最新研究进展 以及相关背景工具和v h d l 语言，然后介绍了模型检查技术的理论基础， 并研究和设计了一个针对时序电路v h d l 设计的模型检查系统的解决方 案。本文的丰要工作有： 1 研究模型检查相关理论和算法，包括k r i p k e 结构、时序逻辑c t l 、 不动点计算、反例路径生成等。并在此基础上实现了一个基于i q i p k e 结构、 不动点计算和o b d d 动态排序的模型检查器，可验证v h d l 设计的正确性。 2 提出了一个针对时序电路v h d l 设计的模型检查系统的解决方案。 包括了实现方案选择、系统主要内容( 包括v h d l 建模，给出规格说明， 进行模型检查) 以及系统总体框架； 3 实现将v h d l 设计转换成有限状态机，并使之能同时适用于异步 时序电路和同步时序电路，这包括建模算法、子模型的建立，子模型的合 并等：另外对上述建模算法进行优化，对于同步时序电路能有效化简，减 少系统状态空间。 4 研究和实现o b d d 相关技术，将v h d l 数据类型用o b d d 表示， 并采用动态变量排序的筛选算法，使o b d d 变量序得到优化，减少o b d d 的规模。 5 最后对一个锁存器v h d l 设计进行模型检查以检验所做工作。 关键词：模型检查，硬件描述语言，有限状态机，- - 3 l 决策图 上海大学硕+ 学位论文 a b s t r a c t a s 0 1 1 1 c o m p u t e rs o f t w a r ea n dh a r d w a r es y s t e m sh a v eb e c o m e i n c r e a s i n g l yi m p o r t a n ta n dc o m p l e x ，h o wt oe n s u r et h ec o i t e c t n e s sa n d r e l i a b i l i t yo fs u c hs y s t e m sh a sb e c o m eav i t a lp r o b l e mi nb o t ht h e o r e t i c a la n d i n d u s t r i a lc i r c l e s t h ec o m m o n l yu s e dm e t h o df o rd e s i g nv a l i d a t i o ni st h e v e t e r a nt e c h n i q u eo ft e s t i n g ，w h i c hc a no n l yp r o v et h ee x i s t e n c eo fb u g s ，b u t c a n n o tp r o v et h ei n e x i s t e n c eo f b u g s t e s t i n gi sb yn a t u r en o tag o o dm e t h o df o r h i 曲r e l i a b i l i t ys y s t e m s i nt h el a s tc o u p l eo fd e c a d e s ，r e s e a r c h e r sf r o mm a n yc o u n t r i e sh a v eb e e n p u t t i n gg r e a te f f o r tt or e s o l v et h i sp r o b l e ma n dh a v em a d eg r e a ta c h i e v e m e n t sa s w e l l a m o n gt h er e l a t e dt h e o r i e sa n dm e t h o d s ，m o d e lc h e c k i n gh a sc o m et o f r o n tb e c a u s eo fi t sc o n c i s e n e s sa n dh i g hd e g r e eo fa u t o m a t i o n i nt h i sp a p e r , i tf i r s t l yg i v e sa no v e r v i e wo fm o d e lc h e c k i n g ，i n c l u d i n gi t s b a s i cm e t h o d o l o g y , d e v e l o p i n gd i r e c t i o n sa n du p - t o d a t er e s e a r c ha d v a n c e m e n t t h e n ，t h et h e o r e t i c a lf u n d a m e n t a lo fm o d e lc h e c k i n g ，t e m p o r a ll o g i c ，a n d s o m er e l a t e dt o o la n dl a n g u a g ea r ei n t r o d u c e d a f t e rt h a t ，as o l u t i o nt om o d e l c h e c k i n gs y s t e mi sp r o p o s e dt ov e r i f yg e n e r a lv h d ld e s i g n t h em a i nc o n t r i b u t i o n so ft h i sp a p e ra r es h o w na sf o l l o w s ： 1 r e s e a r c h i n gm o d e lc h e c k i n ga l g o r i t h m si n c l u d i n gk r i p k es t r u c t u r e ， c t l , f i x e d - p o i n t ，c o u n t e r - e x a m p l e a m o d e lc h e c k e rb a s e do nt h o s e t e c h n o l o g i e sa n do b d dd y n a m i cr e o r d e r i n g i s i m p l e m e n t e dt ov e r i f yt h e c o r r e c t n e s so f av h d l d e s i g n 2 as o l u t i o nt om o d e lc h e c k i n gb a s e do nv h d ld e s i g ni sg i v e ni n t h i s p a p e r i td e s c r i b e st h es y s t e ma r c h i t e c t u r eo ft h es o l u t i o ni n c l u d i n gm o d e l i n g ， s p e c i f i c a t i o n ，a n dm o d e lc h e c k i n g 3 am o d e l i n ga l g o r i t h mi sg i v e nw h i c ht r a n s l a t e sv h d ld e s i g ni n t of s m a n ds i m p l i f y i n gf s mo fs y n c h r o n o u sv h d l d e s i g n 4 c o m p u t i n go b d df o rv h d ld a t at y p ea n da p p l y i n gs i f t i n g a l g o r i t h mt or e d u c et h es t a t es p a c eo ft h eo b d d 5 f i n a l l y , 粕e x a m p l eo fm o d e lc h e c k i n gl a t c h - v h d l d e s i g ni sg i v e nt ov e g f y w o r k sa b o v e k e y w o r d s ：m o d e lc h e c k i n g ，v h d l ，f s m ，b d d 上海大学硕士学位论文 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同_ 工作的其他同志对本研究所做的 任何贡献均己在论文中作了明确的说明并表示了谢意。 签名：丝皇耋丝日期：竺生! ：，f 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即： 学校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学 校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：莒傩鸟导师签名：逛丕! 型日 i i 期：乏! ! 篓：至型 i ：海大学硕l 学位论文 1 1 引言 第一章绪论 随着计算机软硬件系统规模的日益复杂化、重要化，如何保证计算机系统 的正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。今天 我们已经很难承受计算机系统发生故障所带来的损失，尤其是对于航天、金融、 交通等行业的计算机系统，其安全性与可靠性的要求更是特别严格，系统中的 任何小问题都有可能带来灾难性的后果。在计算机技术日新月异的今天，限制 计算机实际广泛应用的因素已经不再是机器硬件“缓慢 的速度和“低下 的 计算能力，而更多的是在设计和实现正确可靠的复杂系统时，我们本身的设计 和保障能力还比较有限，无法保证所设计系统的安全性、正确性和可靠性。 但是，由于现在的系统复杂度很高，系统的设计和分析是相当困难的，尤 其对于并发系统，由于其内在的非确定性因素很大，难度就更大。这就需要一 种可靠并且可行的系统验证方法( v a l i d a t i o nm e t h o d ) 川。 目前针对复杂系统的丰要的验证方法有测试( t e s t i n g ) 、仿真( s i m u l a t i o n ) 、 演绎推理( d e d u c t i v er e a s o n i n g ) 、模型检查( m o d e lc h e c k i n g ) 等。 测试( t e s t i n g ) 和仿真( s i m u l a t i o n ) 是两种比较传统的系统验证方法。实 践证明这两种方法在系统调试的早期是非常有效的。在方法上，它们大体上都 是在系统的某些节点注入信号，然后在其他节点观察结果信号，以此验证系统； 对于软件系统，则通常包括提供某些输入并观察相应的输出来验证。测试和仿 真通常能有效地发现许多错误，但是其不足也是很明显的，即：对给定数据集 通过了测试但并不能保证在实际运行中对其它输入不发生错误。即测试用例不 可能涵盖所有实际输入，所以无法回答系统内没有错误这样一类问题。 演绎推理验证方法( d e d u c t i v er e a s o n i n gv e r i f i c a t i o n ) 的重要性在计算机领 域已经被广泛认识到，并深刻影响了软件开发。但其不足是：演绎推理是一个 相当耗时费力的过程，并且只有那些对逻辑推理有很高造诣并具有丰富实践经 验的专家才能很好的执行。因此这种方法实践上很少使用，主要应用于一些高 j ：海大学硕士学位论文 度敏感的系统，比如安全协议等。 模型检查( m o d e lc h e c k i n g ) 是一种新的验证有穷状态并发系统的技术，并 以其简洁明了和自动化程度高而引人注目。本文研究的对象就是模型检查，这 是一种形式化验证方法。形式化方法( f o r m a lm e t h o d s ) 【2 】是基于数学方法来描 述目标系统性质的一门技术，用严格的数学符号和数学法则对目标系统的结构 与行为进行有效的综合，分析和推理，它为系统的说明、开发和验证提供了一 个框架，以便于发现目标系统中的不致性，不完整性，以及设计与要求相违 背等情况。形式化方法用数学方法描述系统的规格说明，并且根据数学理论来 检查所设计的系统是否满足所期望的性质。实践证明，形式化方法可通过自动 验证发现用其他方法不能发现的设计错误。 模型检查技术有2 个显著的优点：一是自动化验证，不需要人工干预就可 以完成整个检查过程；二是如果验证结果表明系统不满足规格说明，则模型检 查能够给出反例( c o u n t e r e x a m p l e ) 指出为什么不满足。 1 2 。当前研究概况 1 2 1 模型检查研究概况 模型检查的研究始于八十年代初，当时e m c l a r k ，e a e m e r s o n 【3 】等人 提出了用于描述并发系统性质的c t l ( 计算树时序逻辑) 逻辑，设计了测试有 穷状态系统是否满足给定c t l 公式( 即规格说明) 的算法，并实现了一个原型 系统。这一工作为对并发系统的性质自动进行验证开辟了一条新的途径。 随后不久出现的符号模型检查( s y m b o l i cm o d e lc h e c k i n g ) 【4 】技术使这一方 法向实际应用迈出了关键的一步。模型检查己被应用于计算机硬件、通信协议、 控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩e i 的成功，并 在实际中得到广泛应用。 模型检查已经从学术界辐射到了产业界，许多大公司，如i n t e r , h e , p h i l l i p s 等成立了专门的小组负责将该技术应用于生产过程中。c l a r k e ，e m e r s o n ，b r y a n t 和m c m i l l o n 因模型检查的创始性工作获得了1 9 9 8 年a c mp a r i sk a n e l l a k i s 2 上海大学硕上学位论文 a w a r df o rt h e o r ya n dp r a c t i c e 。 模型检查的研究大致涵盖以下内容：模态时序逻辑、模型检查算法及其 时空效率( 特别是空间效率) 的改进以及支撑工具的研制等。 模型检查方法面临的主要挑战就是“状态爆炸 问题。因为该方法基于对 系统状态空间的穷举搜索。当系统的规模越来越大时，需要的空间和时间的开 销将呈指数级增加，也就是系统的状态数目会急速增加，在这种情况下直接对 其状态空间进行搜索在实际上是不可行的。 为了能够有效地应用模型检查方法，需要研究减少和压缩状态空间的方法。 文献上关于这方面的文章很多，其中很多方法已经实现在不同的模型检查工具 中。 符号模型检查【4 1 的基本原理是将系统的状态转换关系用逻辑公式表示。在 这种方法中，二叉决策图( b i n a r yd e c i s i o nd i a g r a m ，简写b d d ) 【5 】是用以表示 逻辑公式的重要手段。它能较为紧凑地表示状态转换关系，以降低系统模型所 需的内存空间。另外，状态转换的计算可以以集合为单位，以提高搜索的效率。 该技术使模型检查方法向实际应用迈出了关键的一步。 o n t h e n y 【6 1 技术的基本原理是根据需要展开系统路径所包含的状态，避免 预先生成系统中所包含的所有状态。 一个系统可以由多个进程组成，并发执行使得不同进程的动作可以有许多 不同的次序。基于对这一问题的认识，我们可以将某些状态的次序固定，以减 少重复验证本质上相同的路径，这种方法称为偏序规约7 1 。 由多进程组成的系统中某些进程可能完全类似，并发执行的结果可能产生 许多许多相同或相似的路径。基于对这一问题的认识和研究，我们可以只搜索 在对称关系中等价的一种情形，以避免重复搜索对称或相同的系统状态，这种 方法称为对称模型检查【8 】。 一般来讲能够减少搜索空间的方法能同时节省时间和内存空间的需求。由 于内存空间在某些情况下比时间更为重要，有些方法的目标是以时间换空间。 例如在s p i n 9 1 中实现的压缩方法和用自动机表示可达状态的方法就是这样的方 法。 i ：海大学硕上学位论文 除了在模型检查的过程中应用不同方法以增加效率和减少内存空间的需求 外，还有许多研究的目标是减少模型本身或验证性质的复杂性。这方面的方法 有不同类型的抽象【1 0 1 1 1 、程序切片【1 2 13 1 、模型分解1 4 1 、验证性质的分解【1 5 】。抽 象的基本想法是抽掉系统中的细节，用尽可能少的状态来刻画系统的运作过程。 程序切片的基本想法是将程序中不影响所要验证的性质的语句去掉以减少模型 复杂性。模型分解的想法是将一个模型分解成若干部分，或者分别验证，或者 提供一个较好的组合方法以降低验证的复杂性。同样，一个需要验证的性质也 有可能分解成若干部分，然后分别验证。 1 2 2 模型检查工具及应用进展 模型检查的优点在于可以完全自动地进行验证，这一方法的成功在很大程 度上应归功于有效的软件工具的支持。以下介绍几个验证不同类型逻辑公式的 软件工具： s m v t 4 】是美国卡耐基梅隆大学开发的模型检查工具，用以检查一个有限状 态系统是否满足c t l 公式。它的建模方式是以模块为单位，模块可以同步或异 步组合。模块描述的基本要素包括非确定性选择，状态转换和并行赋值语句。 其模型检查的基本方法是以二又图表示状态转换关系，以计算不动点的方法检 查状态的可达性和其所满足的性质。 s p i n 9 1 是美国贝尔实验室开发的模型检查工具，用以检查一个有限状态系 统是否满足p l t l 公式及其他一些性质，包括可达性和循环。它的建模方式是 以进程为单位，进程异步组合。进程描述的基本要素包括赋值语句，条件语句， 通讯语句，非确定性选择和循环语句。其模型检查的基本方法是以自动机表示 各进程和p l t l 公式，以计算这些自动机的组合可接受的语言是否为空的方法 检查进程模型是否满足给定的性质。 c v t l 6 1 是美国卡耐基梅隆大学开发的模型检查工具。该工具使用符号模型检 查技术，可以验证v h d l 设计，但是c v 目前只能在s u ns p a r c 机器上使用， 因此其适用性要差一些，影响了其实际应用。 v e d s o t t t l 7 1 是贝尔实验室开发的又一个模型检查工具，是一个大的工业化软 4 f ：海大学硕士学位论文 件产品，集成朗讯公司的c d m ac a l l p r o c e s s i n g 软件库，每天通过无线网络处 理百万级的移动设备通信。 随着模型检查技术的迸一步发展，其应用范围逐步扩大，涵盖了硬件设计、 通讯协议、安全协议、控制系统和一部分软件。电子线路设计验证的例子包括 先进先出存储器的验证，验证的性质包括输入和输出的关系18 1 。浮点运算部件 的验证，验证的性质包括计算过程所需满足的不变式【1 9 】。 对于复杂的协议和软件，模型检查的验证基于抽象和简化的模型。协议验 证的例子包括认证协议的验证，验证的性质包括对通话双方的确认 2 0 】；合同协 议的验证，验证的性质包括公平和滥用的可能性2 1 】；缓存协议的验证，验证的 性质包括数据的一致性和读写的活性【2 2 1 。 对于软件，由于软件的复杂和软件运行中可能到达的状态个数通常没有实 质上的限制，验证通常局限于软件的某些重要组成部分。软件验证的例子包括 飞行系统软件的验证，验证的性质包括系统所处的状态和可执行动作之间的关 裂2 3 】；铁路信号系统软件的验证，验证的性质包括控制信号与控制装置状态的 关系【2 4 】。 随着软件建模工具的发展，现在通过u m l 实现系统的建模，然后对相应 的u m l 模型进行模型检查的相关研究也逐步发展【2 5 1 。对于u m l 不同类型的图 也出现不同的转换方式，如：从顺序图【2 6 】、活动副2 7 1 、类图【2 8 】，状态图等到 状态迁移系统的转换。对u m l 状态切片【3 0 】与z 语言【3 1 】到状态迁移系统的转换 研究也是对模型检查技术的扩展。利用u m l 不但可以为系统建模，而且还可 以自动生成相关的程序代码片断，这也是u m l 应用于模型检查技术的一大优 势。 模型检查还可以应用于其他方面，其基本思想是将一个过程或系统抽象成 一个有穷状态模型，加以分析验证。这方面的例子包括化学过程验证，验证的 性质包括阀门、管道和容器的状况【3 2 】；公司操作过程分析，分析的内容包括操 作过程是否具有所需的功能 3 3 】；机床操作程序的验证，验证的性质包括操作程 序的动作前后关系和操作是否安全可靠【3 4 1 。 测试是保证软件产品可靠性和正确性的传统手段。与测试不同，模型检查 j ：海大学硕：l 学位论文 不是针对某组输入，而是面向某类性质来检查系统是否合乎规约。在系统不满 足所要求的性质时，模型检查算法会产生一个反例( 一般是一条执行路径) 来 说明不满足的原因。这一功能与测试有异曲同工之处，是一个十分值得注意的 研究方向，文酬3 5 】提出了基于模型检查的测试用例自动生成的初步方法。 另外，需要一提的是模型检查工具与大型软件开发工具的结合。比如，瑞 典t e l e l o g i c 公司的软件开发工具( t a u ) 包含系统建模，系统测试以及模型检 查工具，这个软件开发工具主要面向通讯、实时系统，其基木原理与s p i n 相 同。文献【3 6 1 提出了在广泛运用的开发用具e c l i p s e 中实现的一个初步的模型检查 插件。这些都是当前比较热门的研究方向。本文提出的有关基于v h d l 的模型 检查的解决方案也可进一步集成到相关e d a 工具中，也可以与仿真、测试相结 合，具有广泛的应用前景。 1 3 论文的课题来源、研究内容和意义 本文课题来源于8 6 3 项目：基于模型的w e b 应用测试方法、测试用例牛成 技术与工具的研究( 课题编号：2 0 0 7 a a 0 1 2 1 4 4 ) 。 目前普遍认为，硬件模型检查技术在工业界的应用前景是十分乐观的，基 于v h d l 的模型检查技术的推广应用也正在迅速展开。 事实上，近几年来，模型检查技术已经引起了e d a 产业的轰动和商业界的 投资热潮。据统计，近几年在全世界的主要e d a 公司都相继研制和推出了模型 检查软件。人们预计这项技术将在电子设计领域得到更加广泛的应用。 本文首先讨论了模型检查技术的基本思想、研究方向和最新研究进展以及 相关背景工具和v h d l 语言，然后讨论了模型检查技术的理论基础，并研究和 设计了一个针对时序电路v h d l 设计的模型检查系统的解决方案。 本文主要研究对于用硬件描述语言v h d l 所设计和描述的系统，用模型检 查进行验证，从而保证系统正确性和可靠性，实现自动化的模型检查。 主要研究内容包括以下几部分： 首先研究模型检查相关理论和算法，包括k r i p k e 结构、时序逻辑c t l 、不 动点计算，反例路径生成等。 6 ：海大学硕 ：学位论文 然后在此基础上提出了一个针对时序电路v h d l 设计的模型检查系统的解 决方案。包括了实现方案选择、系统主要内容以及系统总体框架；将v h d l 设 计转换成有限状态机，并使之能同时适用于异步时序电路和同步时序电路，包 括建模算法、子模型的建立，子模型的合并等；另外对上述建模算法进行优化， 对于同步时序电路能有效减少系统状态空间。 最后研究o b d d 相关实现技术，并针对上述模型检查系统，将v h d l 数据 类型用o b d d 表示，并采用动态变量排序的筛选算法，使o b d d 变量序得到 优化，减少o b d d 的规模。 本文的章节安排如下： 第一章，序言，介绍了模型检查研究概况，模型检查工具和应用进展，以 及论文研究内容 第二章，模型检查技术，首先概述了模型检查技术的主要思想，介绍了 k r i p k e 结构、时序逻辑c t l 公式，不动点计算，最后介绍了一种实用的反例生 成策略。 第三章，基于v h d l 的模型检查系统的设计，提出了一个针对时序电路 v h d l 设计的模型检查系统的解决方案。包括方案选择，系统的主要内容和系 统的总体框架。 第四章，基于模型检查的v h d l 到f s m 的转换，首先介绍了基于模型检 查的v h d l 子集，有限状态机的定义，然后将v h d l 设计转换成有限状态机， 能同时适用于异步时序电路和同步时序电路，同时对上述建模算法进行优化， 对于同步时序电路能有效减少系统状态空间。 第五章，v h d l 数据类型的o b d d 表示，首先介绍了o b d d 的基本概念 和基本算法i t e ，然后提出o b d d 实现的数据结构和基本算法，最后将v h d l 数据类型用o b d d 表示，并采用动态变量排序算法。最后对一个锁存器v h d l 设计进行模型检查以检验所做工作。 第六章，总结与展望。 7 e 海大学硕。 = 学位论文 第二章模型检查技术 随着计算机软硬件系统规模的日益复杂化、重要化，如何保证计算机系统 的正确性和可靠性成为紧迫需要解决的问题，由此提出的诸多理论和方法中， 模型检查以其简洁明了和自动化程度高引人注目。模型检查的研究范围大致涵 盖以下内容：时序逻辑，模型检查算法及其时空效率的改进，以及支持工具的 研制。这几个方面之间有着密切的内在联系，一般来说不同时序逻辑的模型检 查算法的复杂性不一样，针对的问题不一样。本章主要介绍模型检查基本原理， 计算树逻辑( c t l ，c o m p u t e r t r e el o g i c a l ) ，模型检查基木算法。 2 1 模型检查基本原理 模型检查是一种针对有限状态并发系统( f i n i t e s t a t ec o n c u r r e n ts y s t e m ) 的 形式化自动验证技术，它通过穷尽搜索系统的整个状态空间( s t a t es p a c e ) 来检 查系统模型是否满足给定的性质。 模型检查的研究始于上世纪八十年代初，当时e m c l a r k ，e a e m e r s o n 等人提出了用于描述并发系统性质的c t l ( 计算树时序逻辑) 逻辑，设计了测 试有穷状态系统是否满足给定c t l 公式( 即规格说明) 的算法，并实现了一个 原型系统。这一工作为对并发系统的性质自动进行验证开辟了条新的途径。 模型检查的基本思想是用状态迁移系统( m ) 表示系统的行为，用时序逻 辑公式( f ) 描述系统的性质。这样“系统是否具有所期望的性质”就转化为数 学问题：“状态迁移系统m 是否是公式f 的一个模型? ，可用公式表示为： mi f ? 这个问题在有穷状态系统中，是可判定的，可以对状态空间进行遍历搜索 即可确定公式是否成立。而对于些具有无限状态的系统，可以通过抽象和归 约，使之映射为有穷状态系统。 模型检查的基本过程可简要描述为：( 如图2 1 所示) 1 建模：把需要设计分析的系统转化为种模型检查接受的可形式化的模 8 l 二海大学硕j ：学位论文 型，即状态迁移系统。 2 给出规格说明：把系统的属性及对系统的要求，作为规格说明以时序逻 辑( c t l 、l t l 或u 演算) 的形式给出，以进行验证。 进行验证：根据模型检查算法，在模型的状态空间内对规格说明进行搜索。 不符合规格说明的可以给出反例，指出其错误所在。 图2 1 模型检查过程示意图 基于状态迁移系统的模型检查有两个重要的优点：一是建立在状态迁移系 统之上的模型检查是全自动的，并且不需要用户掌握很深的数学方面的专业知 识，就可以完成验证过程。这为模型检查的广泛应用提供了方便之门；二是如 果系统模型不能满足某一规格说明，模型检查算法会自动给出反例，也就是错 误路径，标识何处出现了错误，而这样的反例将会对查找错误原因和修正错误 提供重要的帮助。 而模型检查最大的局限性就是系统“状态空间爆炸 问题。当系统规模庞 大和复杂时，系统的状态空间急剧增大，对时间和空间的要求使得在实际工作 中模型检查运算无法完成。针对这一问题有很多研究工作已经进行，并取得了 相应的成果。一方面，从扩充计算机处理能力入手，用尽量少的资源处理尽可 能多的状态。如：0 1 1 。t h e f l y 技术，o b d d 的采用等等。另一方面，从限制系统 9 i ：海大学硕：l 学位论文 模型的规模入手，尽量减少系统模型的状态，使系统模型的状态空间缩小到可 以实际运算。如：归约、抽象、切片、局部状态空间等。这样从一定程度上缓 解了状态爆炸问题。 随着研究的深入，模型检查的应用越来越广泛，涵盖了通讯协议、安全协 议、控制系统、电子线路和软件系统等诸多领域。模型检查技术的应用，也标 示着人们对系统的安全性和正确性的关注和认识又进一步，同时对系统安全性 越来越重视，这也促进了模型检查技术本身的发展。 2 2 k r i p k e 结构 对系统进行验证的首要工作就是构建系统的形式化模型，使计算机程序可 以方便地处理验证过程。，模型检查用到的数据结构就是k r i p k e 结构，用状态 迁移系统来描述系统的形式化模型。k r i p k e 结构是一种基于状态迁移关系的结 构，便于模型检查运算，对系统的验证就是在k r i p k e 结构上，按照状态转移关 系寻找满足条件的路径。 k r i p k e 结构定义如下： 一个原子命题集( a p ，a t o m i cp r o p o s i t i o n ) 上的k r i p l e 结构是个四元组 m = s ，s o ，r ，l ，表示一个有限状态并发系统模型。其中： a p 是原子命题集，表示系统具有的基本性质。 s 是系统的状态集，也就是状态空间，是模型检查的基础。 瓯s 是系统的初始状态集。 r s s 是系统状态间的转换关系集。 l ：s 一2 a p 是标号函数，标识在每个状态上为真的命题。对于任意状态s ， 如果一个命题f 出现在状态s 上，即：f l ( s ) ，则说明命题f 在状态s 上满足 的。 由此可知，一个系统模型就是一个k r i p k e 结构。系统的运行过程，可以表 示为一条路径，就是一个状态的无限序列= s 。s ，s ：。表示从初始状态s 。开始 的系统运行轨迹。有时，在不考虑初始状态时s o 可以省略。如图2 2 所示是一 1 0 f ：海大学硕士学位论文 个k r i p k e 结构示意图。 图2 2 一个k r i p k e 结构的状态迁移图 其中： s = 1 ，2 ，3 ) ；r = ( 1 ，2 ) ，( 1 ，3 ) ，( 2 ，1 ) ，( 2 ，3 ) ，( 3 ，3 ) ) ； l = ( 1 ，a ，b ) ，( 2 ，b ，c ) ，( 3 ，c ) ) 。图中标出来的字母代表在此状态上为 真的命题。 2 3 时序逻辑 时序逻辑( t e m p o r a ll o g i c ) 是模型检查的理论基础，是一种命题逻辑，是 研究问题的必然性、可能性及其相关概念的一个逻辑学分支，在描述并发系统 中是非常有效的。 时序逻辑并不直接需要时间向量就可以描述出事件间的先后顺序，表示事 件的发牛序列。时序逻辑应用原子命题和布尔运算符，如：与、或、非等，可 以组成复杂表达式，来表示系统的某一属性。时序逻辑通过时序逻辑算子表达 事件的发牛顺序。时序逻辑算子也可以和布尔运算符进行联合或嵌套，组成更 复杂的时序逻辑公式。 一个时序逻辑公式表示系统的某一属性，也可以说是系统的一条路径，可 以描述系统中某一状态是可能到达的，或者某一状态是永远也无法到达的。 常用的时序逻辑有三种，计算树逻辑c t l 、命题线性时序逻辑l t l 和命题 _ l ：海大学硕上学位论文 u 演算。本节主要介绍c t l 。 2 3 1 计算树逻辑c t l 从概念上讲，计算树逻辑就是一种用计算树描述系统的形式化方法。在 k r i p k e 结构表示的状态空间中，以初始状态为根，每个状态可能有多个后续状 态，而后续状态又可能有多个后续状态，以此类推可以形成一个状态树。将图 2 2 的k r i p k e 结构按所有可能的路径扩展，就形成一个计算树( 如图2 3 所示) 。 图2 3 图2 2k r i p k e 结构展开的计算树 这棵计算树表现了从根节点开始的所有可能路径，是一种展开的系统状态 图。 c t l 是一种分叉时序逻辑，可以描述状态的前后关系和分叉情况。用c t l 描述的状态或性质就是c t l 公式。 c t l 公式由原子命题、逻辑连接符、路径算子( p a t hq u a n t i f i e r s ) 和时序 算子( t e m p o r a lo p e r a t o r s ) 组成。 c t l 逻辑连接符最基本的是：- i ( 非) ，八( 与) ，v ( 或) 路径算子用来描述计算树上的分叉情况。表示在从某状态开始的所有路 径上或某一路径上满足的性质。路径算子包括： e ( e x i s t s )表示对于某一分支。 1 2 卜海大学硕 = 学位论文 a ( a l w a y s ) 表示对于所有分支。 时序算子用来描述贯穿计算树的路径的性质。共有五个基本时序算子： x ( n e x tt i m e ) 表示路径上当前状态的下一个状态。 f ( i nt h ef u t u r e ) 表示路径上以后的某个状态。 g ( g l o b a l l y ) 表示路径经上的所有状态。 u ( u n t i l ) 表示直到某一状态。 r ( r e l a t i v e ) u 的对偶。 2 3 2c t l 公式 c t l 公式有两种类型：种是状态公式( s t a t ef o r m u l a s ) ，表示在某一状态 上为“真；另一种是路径公式( p a t hf o r m u l a s ) ，表示在某条路径上为“真”。 状态公式的合式公式定义如下： ( 1 ) 如果p a p ，那么p 是状态公式。 ( 2 ) 如果f 和g 是状态公式，那么 f ，f v g 和f a g 都是状态公式。 ( 3 ) 如果f 是路径公式，那么e f 和a f 都是状态公式。 路径公式的合式公式定义如下： ( 1 ) 如果f 是状态公式，那么f 也是路径公式。 ( 2 ) 如果f 和g 是路径公式，那么1f ，g ，f 入g ，x f ，f f ，g f ，f u g 和 f r g 都是路径公式。 定义1 是路径丌从状态s 1 开始的后缀。如果f 是状态公式，那么表达式 m ，si = f 就是说在k r i p k e 结构m 中，f 在状态s 上为真。如果f 是路径公式， 那么表达式m ，兀i = f 表示在k r i p k e 结构m 中，沿着路径兀，f 为真。 下面是l = 的一些常见表达式：( f l 和f 2 是状态公式，9 1 和9 2 是路径公式) 1 m ，s | = pp l ( s ) 2 m ，sl _ - if l营m ，sf f i 3 m ，sl = f lv f 2m ，s | = f l 或m ，s | ：f 2 4 m ，si _ f l 八f 2营m ，s - n 且m ，s | - f 2 5 m ，sj = e g l铮存在一条从s 开始的路径，满足m ，丌l = g l 1 3 6 m ，s | 一a g l营所有从8 开始的路径，都满足m ，兀j = g l 7 m ，nl = f ls 是路径兀的第一个状态，并且m ，si = f l 8 m ，了【l = 1g lc ，m ，了【l 9 1 9 m ，丌l = g lv 9 2c ，m ，i = g l 或m ，i = 9 2 1 0 m ，l - g la 9 2m ，| _ g l 且m ，l 9 2 1 1 m ，i x g l铮m ，1l _ g l 1 2 m ，i _ f g l存在k o ，满足m ，“| _ g l 1 3 m ，f = g g l对于所有i o ，满足m ，1 | - g l 1 4 m ，i _ g lu9 2存在k o ，满足m ，。i - 9 2 ，且对于所有的o j k ，有m ，兀。l - g l 1 5 m ，兀 g lr9 2营对于所有的j 0 ，如果对于每个i j ， m ，1 9 1 ，那么m ，丌f = 9 2 c t l 有2 个路径算子和5 个时序算子，因此总共有1 0 种组合： a x 和e x a f 和e f a g 和e g a u 和e u a r 和e r 注：a u 和e u 指形如a ( f ug ) 、e ( f ug ) 的公式。 通过一些简单的等价变换，所有以上运算最后都可以归结为e x ，e g 和e u 三种基本运算，因此，任何c t l 公式都可表示为用a 、e x 、e g 、e u 组合 起来的表达式【l 3 1 ： a xf三1e x ( 7f ) e ff三e t r u eu f 】 a gf三1e f ( 7f ) a ff兰7e g ( 7f ) a fug 三7e 1 7g1 j ( 7f a 7g ) 八1e g ( 1g ) a f v 朗 三1e 1 7fu7g 1 4 e 海大学硕士学位论文 e l frg 兰7a 7fu1g 下图是常见的c t l 算子： m ，s o i - e f g m ，s o i _ e g g 2 4 模型检查算法 g m ，s o i = a f g m ，s o i a gg 图2 4 四种基本c t l 算子 模型检查的算法过程就是：对于给定的用k r i p k e 结构表示的系统模型 m = s ，s o ，r ，l ) ，以及用时序逻辑公式( c t l 等) 表示的系统属性( 规格说 明) f ，寻找s 中所有的满足f 的状态，即t = s e esm ，si = f ) 。当初始状态s o 包含在t 中时，即& 丁时，系统模型m 满足规格说明f 的要求，系统得到验 证。 符号模型检查算法把用k r i p k e 结构表示的状态迁移系统看成带标号的有向 图。有向图中的节点代表系统的状态，图中的弧表示状态间的转换关系，状态 上的标号就是标号函数l ：s 一2 a p 对应的内容。标号完成后，检查初始状态的 标号即可判断系统是否满足规格说明。前- d , 节说过所有的c t l 公式都可以归 上海大学硕士学位论文 结到 、 、e x 、e g 、e u 五个算子，下面给出模型检查基本算法。 态s s tittt 图2 5c t l 基本公式生成路径示意图 标号算法： l a b e l g r a h p ( f ) s w i t c h ( ft y p e ) c a s e 原子命题p ： 标记所有满足p 的状态) ； c a s e1 ： 标记所有不满足f 的状态) ； c a s e 八： f = f l a l 2 标记同时满足f 1 和也的状态) ； c a s ev ： 类似“八 ； c a s ee x ： f = e xf l 标记所有后继状态满足f 1 的状态) ； c a s ee g ： f = e gf l 调用c h e c k e g ( f 1 ) ) ； c a s ee u ： 仁e ( f l u f 2 ) 调用c h e c k e u ( f l ，纪) ) ； ) 其中，对于公式e ( f uf ) ，假定公式f 和g 都已经标号完成。即对于任意状 f l a b e l ( s ) i f f s i = f 1 6 三 上海大学硕士学位论文 f l a b e l ( s ) i f f s i - f 从当前状态s 出发，直到某一后继状态t ，形成一条路径，满足t l = g ，状 态t 前的所有状态均满足公式f o 如图2 5 所示。 c h e c k e u ( f l ，f 2 ) t = si 也l a b e l ( s ) ) ； f o r a l ls td ol a b e l ( s ) = l a b e l ( s ) u ee f l u f 2 ： w h i l et d o c h o o s es t ： t = t s ) ： f o ra l lts u c h t h a tr ( t ，s ) d o i fe f l u f 2 岳l a b e l ( t ) a n df l l a b e l ( t ) t h e n l a b e l ( t ) = l a b e l ( t ) u ee f l u f 2 ) ： t = tu t ) ： e n d i f ： e n df o r ： e n dw h i l e ： ) e gf 的检查算法比较复杂，要把系统状态迁