（计算机软件与理论专业论文）spin模型检测的研究与应用.pdf

摘要 软件是否可信赖己成为一个国家的经济、国防等系统能否正常运转的关键因素之一，尤 其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关( s a f 奶, - - - c d t i c a l ) 领域更是如 此。这类系统要求绝对安全可靠，不容半点疏漏，否则将导致灾难性后果。如1 8 6 1 年8 月英 国克莱顿隧道事故，就是由于协议的不完整性造成的，还有1 9 9 6 年6 月4 日，欧洲航天局阿丽 亚娜( a m - a n e ) 5 0 1 火箭因为其控制软件的规范和设计错误而导致发射3 7 秒后爆炸。类似的报 道屡见不鲜，如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点 问题。 据统计，在美国每年要花去3 0 0 0 亿美金用来雇佣程序员专门来解决程序的b u g ，而这 个工作就占据了整个产品开发周期4 0 , , 6 0 * o 的时间尽管花费了这么大量的人力和物力来 排除b u g ，他们还是不能保证软件没有错误。 为了从根本上保证软件系统的可靠安全包括图灵奖得主a p n d e l i 在内的许多计算机 科学家都认为，采用形式化方法( f o r m a l m e t h d s ) 对系统进行形式化验证和分析，是构造可靠 安全软件的一个重要途径。模型检测技术是形式验证方法中的一种。而获得a c m ( a s s o e i a t i o n f o rc o m p u t i n gm a c h i n e r y ) 软件系统奖( s o f t w a r es y s t e m sa w a r d ) 的s p i n 就是著名的模型检 测工具之一。 典型的s p i n 工作模式是首先对并发式系统或分布式算法的规范建立高标准的模型，在 确认没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为，然后 s p i n 7 z 生一个用c 语言描述的验证程序，经检验机编译后被执行，执行中如果发现了违背正 确性说明的任何反饲，则反馈给交互模拟机，通过重现细节剔除引起错误的原因。 本文首先详细介绍了著名的模型检测工具s p i n 的历史、发展与特点，讨论了使用s p i n 对网络通信协议分析的方法。本文所做的主要工作，技术难点与创新处如下： s p i n ( s i m p l ep r o m d ai n t e r p r e t e r ) 是适合于并行系统，尤其是协议一致性的辅助分析 验证工具，本文讨论了在w i n 3 2 下和c y g w i n l i n u x u m x 下对s p 烈的安装和使用。 使用s p i n 的最简单的方式是使用图形界面x s p i n ，图形界面独立于s p i n 运行， 辅助产生和选择相应的s p i n 命令，x s p 矾在后台运行s p i n 得到期望的输出值， x s p i n 知道什么时候怎么样去编译模型检测的代码，也知道什么时候如何去执行一 它，所以可以不用记住所有的参数。本文介绍了在c y g w i n 下安装和使用s p i n 的 图形界面工具x s p i n 。 p r o m e l a ( p r o t o c o l p r o c e s sm e t al a n g u a g e ) 是用来对有限状态系统进行建模的形式 描述语言，本文阐述了如何使用p r o m e l a 语言对协议进行描述。 a b 协议是最早的端到端的通信协议之一，用s p 矾对a b 协议进行分析从而得到协 议t i t 不容易发现的错误。 使用s p i n 的图形界面x s p i n 对上述协议进行分析得到直观的进程之间信息的交 互图。 s p i n 不仅可以用来验证协议的正确性，也可以对身份验证协议进行有效的攻击检 测。本文讨论了在网络保密通信中使用密钥分配中心k d c 系统时的攻击问题。用 p r o m e l a 语言建立了k d c 的模型，使用l 1 l 描述其性质，用s p 矾进行模型检测验 证，使用x s p i n 得到协议受攻击的轨迹图形。 对n s s k 协议进行建模和分析，得到协议受攻击的轨迹。对w o o _ l a i n 协议进行建 模和分析，得到协议中潜在的两个受攻击轨迹。 本论文所做工作为以后模型检测的研究提供了参考。 作者在校期间，在计算机科学核心期刊上发表论文一篇。 关键字：模型检测，s p i n ，p r o m e l a ，x s p i n ，c y g w l n ，通道，仿真，验证，密码协议 中图分类号：t p 3 1 1 5 2 4 l ； ； ，#t；tli a b s t r a c t m e t h e rt h es o f t w a r ei sc r e d t h l eh a sb e c o m eo n eo f t h ef f f a c l a lf a c t o r sf o r t h en a t i o n a l e c o n o m ya n dn a u o n a ld e f e n e ee t c e s p e c i a l l yi us o m es a f e t y - c r i t i c a lf i e l d ss u c ha st h ee o n t r o lo f n u c l e a rr e a c t o r ，a e r i a ln a w g a u o na n dr a d w a ya t t e m p t e r t h e s es y s t e m sr e q u i r ea b s o l u t es a f e t y a n dn oe l t o ri sp e r u n t t e d o re l s et e r r i b l er e s u l tm a yo c c u r f o re x a m p l e ，c l a y t o nt u n n e l a c c i d e n tm a u g u s t1 8 6 1i u s tr e s u l t e df r o mh a l f - b a k e dp r o t o c 0 1 a n do nj u n e1 9 9 6 ，e u r o p e s p a c e f h g h td e p a r l m e n t r o c k e ta n a n e5 0 1e x p l o d e d3 7s e c o n d sa f l c rb e m gf i r e d ，d u et ot h e b u 嚣i l li t ss p e c t f i c a t m na n dd e s t g no f t h ec o n t r 0 1 s t m i l a rr e p o r t sa r ec o n u n o no c c u r r c l l c e s h o w t oe n s u r et h ed e p e n d a b d i t yo ft h e s es y s t e m sh a sb e c o m eaf o c u sp r o b l e mi nc o m p u t e rs c i e n c e a n dc y b e r n e t i c sf i e l d a c c o r d i n gt os t a t i s t i c s i na m e r i c a $ 3 0 0 0h u n d r e dm i l l i o nw i l lb es p e n ti ne m p l o y i n g p r o g r a m m e rt od e a lw i t ht h eb u g , w h i c ht o o ku p4 0 - - 6 0 o ft h ew h o l ed e v e l o p m e n tp e r i o d a l t h o u g hs om u c ht i m ea n de n e r g yh a sb e e ne o n s m n e di nd e m o l i s h l n gb u g s t h e yc a r l te n s u r e b u g sa r er e m o v e df r o mt h es o f t w a r e w i t l lt h ea i mt of f l l s u r et h ee r e d i b t h t ya n ds a f e t yo f t h es o f t w a r es y s t e mr a d i c a l l y , m a n y c o m p u t e rs c i e n t i s t s ，i n c l u d i n ga p i l d e l i 。ag a m e l o f 仙i n ga w a r d ，b e h e v et h a ti t i sa n i m p o r t a n tw a yt oc o n s t r u c ts a f es o f t w a r et h r o u g hv a l i d a t i n ga n da n a l y t n n gt h es y s t e mb yf o r m a l m e t h o d s m e d e le h e c k i n gt e c h n o l o g yi so n eo ft h ev a h d a t l n gw a y s ，a n ds p i n ，w h i c hi sa g a i n e ro fa s s o c i a t i o nf o rc o m p u t m gm a c h i n e r ys o f t w a r es y s t e m sa w a r d i so n eo ft h em o s t f a m o u sm o d e lc h e c k i n gt o o l s s p i n st y p i c a lm o d eo f w o r k i n gi st os t a r tw i t ht h es p e c i f i c a t i o no f ah i g hl e v e lm o d e l o fac o n c u r r e n ts y s t e m ，o rd i s m b u t e da l g o r i t h m ，t y p i c a l l yu s i n gs p i n sg r a p h m a lf i o n t - e n d x s p i n a f t e rf i x i n gs y n t a xe r r o r s m t e r a c t i v es i m u l a t i o ni sp e r f o r m e du n t l lb a s i cc o n f i d e n c ei 8 g a i n e dt h a tt h ed e s l g nb e h a v e sa si n t e n d e d t h e n , s p i ni su s e dt og e n e r a t ea no p t i m t z e d o n - t h e - f l yv e r i f l e a t a o np r o g r a mf r o l nt h eh i g hl e v e ls p e c i f i c a t i o n t h i sv e n f i e ri sc o m p i l e d , w i t h p o s s t h l ec o m p i l e t i m ee h o i c e sf o rt h et y p e so f r e d u c t i o na l g o n t h m st ob eu s e d a n de x e c u t e di f a n yc o l m t e r e x a m p l e st ot h ec o r r e c t n e s sc l a i m sa r ed e t e c t e d ，t h e s ec a nb ef e db a c ki n t ot h e i n t e r a c t i v es i m u l a t o ra n di n s p e c t e di nd e t a i lt oe s t a b l i s h ，a n dr e r u o v e ，t h e i rc a u s e i nt h ef r o n to f t h i sp a p e r , t h eh i s t o r y , d e v e l o p m e n ta n dc h a r a c t e r i s t i c so f s p i n 。af a m o u s m o d e ld e t e c t i o nt 0 0 1 a r ei n t r o d u c e dp r o m e l a ，t h es p i nm o d e h n gl a n g u a g e ，i sf o l l o w e d m i r e t a l i a t i o no fu n e d t t i o ns p i np i ni nw i n d o w s2 0 0 0t h r o u 【g hc y g w mi sd i s c u s s e di nt h i s p a p e r a sf o l l o w s a b - p r o t o c o li sd e s c r i b e da n dw ef o u n dt h ef a l s ea n dt h el c a k f i n a l l y , t h e c o u a - o f a n a l y z i n ge r y p t op r o t o c o lb yp r o m e l ad e s i g n i n gi sp o i n t e do u t a n dt h ep o t e n t i a la t t a c k w a sf e o n d n l l sp a p e ri r i e l u d e st h em a i nd o i n gw o r k , t h ed e e pt e c h n i q u e , a n dt h ec r e a t i v ew o r k a sf o l l o w s ： s p i ni sam o d e lc h e c k e rf o rt h e v e r i f i c a t i o no fc o n c u r r e n ta l g o r i t h m ss y s t e m s ， e s p e c i a l l yi st h a ta u x i h a r yt o o l sf o ra n a l y z i n ga g r e e m e n tc o n s i s t e n c y i nt h i sp a p e rw e d i s c l l 瞄t h a th o wt os e t u pa n du s es p i ni nt h ew i n 3 2e n v i r o n m e n ta n di nt h e c y g w i n l i n u x u n i xe n v i r o n m e n t t h es i m p l e s tw a yt ou s es p i ni st ou s ex s p i n w h i c hh a sg r a p h i c a li n t e r r a c e s g r a p h i c a li n t e r f a c e sr u nw i t h o u tu s i n gs p i na n dc h o o s ec o r r e s p o n t h n go r d e r so fs p i n x s p n qg e t sa n t i e i p a n to u t p u t a n k w e f $ t h r o u g hr u n n i n gs p i ni nt h eb a c k g r o u n d x s p i n k n o w sw h e na n dh o wt oc o m p d et h ec o d ea n di ta l s ok n o w st h a th o wt oi u nt h ec o d e ，s o y o un d n tt or e m e m b e ra l lt h ep a r a m e t e r s t h ep a p e ri n t r o d u c e sh o wt oi n s t a l la n dm c x s p i n t h eg u io f s p i n o nc y g w i np l a t f o r m p r o m e l a ( p r o t o c o l p r o c e s sm e t al a n g u a g e ) i saf o r m a ld e s c r i p t i v el a n g n a g c w h i e hi s w r i t t e nt om a k em o d e lo f t h ef i n i t es t a t e ss y s t e m n ep a p e ri n t r o d u c e sh o wt od e s e r i b ea 5 p r o t o c o li np r o m e l a a b p r o t o c o li so n eo f t h ee a r l i e s te n d - t o - e n dc o m m m l l c a t l o np r o t o c o l s ，a n dt h ep o t e l 撕a l b u g sa r ef o u n db yu s i n gs p i n w ec a r lg e t t h e i n f o r r n a u o n a l t e r n a t m ng l a p ho f t h e i n t u i t i o n i s t t c p r o c e s s o f t h e p r o t o c o l b y u s i n gx s p i n s p i nc a l ln o to n l yb eu s e dt ov e r l 母t h ev a h d n e s so f t h ep r o t o c o l ，i tc a l la l s ob eu s e dt o f h l dt h ea t t a c k so f t h ep r o t o c 0 1 i nt l u sp a p e rw em a k eam o d e lo f t h ek d cp r o t o c o lb y u s m gp r o m e l a ，a n dd e s c r i b ei t sp r o p e r t yb y n g 巩w e l l a sg e tt h ea t t a c kt r a c kb y u s i n gs p i na n dx s p i n m a k m g m o d e lo f t h en s s ka n dt h ew o o _ l a mp r o t o c o l ，w ea l s oc a ng e tt h et r a c ko f t h e a r t a c k s k e y w o r d ：m o d e lc h e c l a n g , s p i n p r o m e l a , x s p i n ，l t l ，c h a n ，s n n u l a t e ，v e r i f i c a t i o nc r y p t o p r o t o c o l c l a s s i f i c a t i o nn o ：t p 3 1 1 5 2 6 1 1 模型检测 第一章模型检测和模型检测工具 1 1 1 概述 一个软件系统的开发设计并不需要很长时间，但后期的测试，维护却占了整个开发周期的 8 0 以上。对于安全性很关键的系统和大型的实时复杂软件系统而言，也许只是因为一二个小 小的错误，就可能造成重大影响。因此，在这些软件系统中，安全性、正确性就提高到了至关 重要的地位。程序完全正确在当前来说是不能保证的，但如果能在开发的早期发现错误，则可 以避免大量的重复性的劳动，减少导致严重后果的因素。基于模型的验证方法( m o d e l - b a s e d v e r i f i c a t i o n ) 致力于这方面的研究，并在某些方面取得了重大突破。 m b v 主要用于复杂软件系统的开发过程，作用是在开发早期发现和纠正错误。工作方式是： 对软件系统或系统的某一部分( 需求规约、设计说明等) 建模，用某种形式化方法说明系统应拥有 的性质和满足的属性，通过对模型进行检测，判断软件系统是否拥有了这些期望的属性。m b v 涉及到了大量的形式化工作。通常使用的形式化技术有：状态机模型：时序逻辑模型；集合关 系模型；并行处理模型；状态探测法。现在研究的重点技术是模型检测( m o d e lc h e c k i n g ) 和 定理证明( t h e o r e mp r o v i n g ) m c 主要支持自动化验证，而定理证明则是用数学证明的方法证明 模型应满足系统的某些属性。在这方面研究较早的是e m c l a r k e 等。 1 1 2 主要技术 m c 使用状态空间搜索的办法来全自动地检验一个有穷状态系统是否满足其设计规范。这 类方法的优点在于它有全自动化的检测过程且验证速度快、效率高，并且如果一个性质不满 足，它能给出这个性质不满足的理由，据此可对系统描述进行改进。该方法自提出以来，发 展非常迅速。其理论与技术得到了工业界和学术界的广泛关注。目前，许多世界著名大公司 如a t & t 、f u j i t s u 、i n t e r 、i b m 、m i c r o s o f t 、l u c e n t 、m o t o r o l a 、s i e m e n s 等纷纷在其产品设计 和开发过程中使用模型检测技术，并在许多复杂的实例研究中发挥了重要的作用。m c 一般工 作方式如图l 所示 图l - i m e 工作模式 现在研究的m c 方法中，按系统属性的表达方式。把m c 方法分为两类。第一种方法是时序 模型检测。这种技术是在2 0 世纪8 0 年代由c l a r k e 和e m e r s o n ，q u e i l l e 和s i f a k i s 独立开发的技术 在这种方法中，系统的规约表达成某种时序逻辑，系统建成有限状态转换系统一个有效的搜 索过程用于检测一个给定的有限转换系统模型是否满足规约的要求第二对方法中规约给定为 一个自动机，系统也建成一个自动机，通过比较系统和规约来确定系统的行为是否满足规约的 要求。这两种方法并不是孤立的，v a r d i 和v o l p e r 表n s j 了怎样把模型映射为自动机，因此产生了 7 二者之间的联系。总的看来，m c 相关的工具和技术有s m v ，s p i n 、s c r 、n l t p l c k 、m u r p h i 、 b d d s 等。 1 1 3 研究现状和发展趋势 不管是m c 还是定理证明，其中都涉及到了大量的形式化工作，特别是建模技术和形式化推 理方面。纵观软件验证工具和技术的发展，主要思想都采用- t - - 元p m l ) 的思想和手段对系统的 一致性、安全性，进展性等属性或对于特定系统应拥有的性质进行证明和推理。对系统建模， 事实上是对系统的行为规约即动态性质进行描述，用某种逻辑表示的属性则是对系统静态性质 的描述。二者相互对照，检查系统的动态行为是否满足系统的静态性质，从而发现系统行为与 要求的不一致性。对于安全性和进展性来说也是一样的：用某种逻辑表示系统的安全属性和进 展条件，再检测这些条件是古被满足。 从当前的研究情况来看，今后的发展主要在以下几个方面进行：( 1 ) 集成不同的建模技术或 研究新的建模技术( 2 ) 扩展推理系统，如时序扩展等。( 3 ) 集成不同的工具，扩展工具的应用范 围。( 4 ) 形成自动化验证的支撑环境。( 5 ) 研究一种新的技术，结合m c 和定理证明技术各自的优 势。 此外，由于m c 和定理证明都将向自动化方向发展，在状态压缩、数据结构，编码技术方而 将提出更高的要求，因此这力面的研究也是一个热点。 1 2 常见的模型检测工具 1 2 1s p i n 由贝尔实验室的形式化方法与验证小组于1 9 8 0 年开始开发的模型检测工具。 建模方式：使用p r o m e l a 语言建模，整个系统可以看作是一组同步的可扩展的有限状态机。 模型检测器：可当做一个完整的l 1 陀( l m e a rt e m p o r a ll o g i c ) 模型检验系统来使用- 支持 所有的可用的线性时态逻辑表示的正确性验证要求，也可以在有效的o n - t h e - f l y 检验系统中用来 检验协议的安全特征。 其他的特征：将偏序简约( p a r t i a lo r d e rr e d u c t i o n s ) 技术、b i ts t a t eh a s h i n g 方法和线性时序 逻辑有效的结合使用。 注释：快速的产生状态空间，快速的偏序简约算法，h a s h 表存储在物理内存中而不是以文 件的形式存在硬盘上。有很好的图形界面x s p i n 。 建议用于：通信协议的检测和线性时序逻辑模型检测 1 2 2s m v s m v 工具是美国c m u 计算机学院的l m c m i l l i a n 博士于1 9 9 2 年开发出的模型检验工具软 件，它基于“符号模型检验”f s y m b o l i c m o d e l c h e c k i n g ) 技术，s m v 因此而得名。s m v 早期 是为了研究符号模型检损i 应用的可能性，而开发的一种对硬件进行检测的一种实验工具发展到 今天s m v 应经成为世界上广为流行的分析有限状态系统的常用工具。 系统模型用s m v 语言描述，一个s m v 程序由两部分组成：一个有限状态转换系统和一组 c t l 公式s m v 把初始状态和转换关系表示成二叉树图b d d s ( b i n a r yd i e i d i n gd m g r a m s ) ，属性 也就是c r l 公式，也表示成b d d s ，通过模型检测算法搜索系统状态空间，给出结果：一个声明 的属性是正确的，或者是不正确的并给出一个反例( 也就是从初始状态开始的一系列状态) 不 满足这个属性一个c t l 公式真正的值通过遍历状态图的方式确定，这种遍历的时间复杂性和 状态空间大小，公式的长度成线性关系。 8 1 2 3p r f f 网可达性分析工具p r o d p r o d 是由赫尔辛基工业大学计算机理论实验室开发的一套用于p r 仃网可达分析的工具 利用p r o d ，可以实现可达图的c t l 模型检测以及基于o n - t h e n y 方法的u l 模型检测 目前，p r o d 的最新版本为3 3 1 0 。p r o d 提供源代码，可以在u n i x 环境及w i n d o w s 环境下使用。 1 2 4 代数网可达性分析工具m a r i a m a r l a 是赫尔辛基工业大学计算机理论实验室的一个四年研究计划的成果它为软件工业提 供了一种代数网模型可达分析、安全检测及活性分析的工具。利用m a r i a ，可以对由s d l 描述的通信协议规范进行分析 1 2 5 其他模型检测工具 p e r t i 网工具：i n a 、l o l a 、p e p 、d e s i g r d c p n u p p a a l 和k r o n o s ：是用于时控系统的模型检测工具。 c a e s a r a l d e b a r a n ( c a d p ) ：是基于l t s s 的一组模型检测工具。 j a v ap a t h f i n d e r2 ：是j a v a 程序检测器。 s l a m ：一个检测c 程序的检测工具。 9 k 2 1 s p i n 概述 第二章模型检测工具s p i n 2 1 1s p i n 的历史背景 s p i n ( s i m p l ep r o m e l ai n t e r p r e t e r ) 是适合于并行系统，尤其是协议一致性的辅助分析检测 工具，由贝尔实验室的形式化方法与验证小组于1 9 8 0 年开始开发的p a n 就是现在s p i n 的前身a 1 9 8 9 年s p i n 的0 版本推出主要用于检测一系列的o - r e g u l a r 属性。1 9 9 5 年偏序简约和线性时序 逻辑转换的引入使得s p i n 的功能进一步扩大。2 0 0 1 年推出的s p i n 4 0 版本支持c 代码的植入， 应用的灵活性进一步增强。在随后2 0 0 3 年推出的s p i n 4 1 版本加入了深度优先搜索算法，更是 使得s p i n 的发展上了一个新台阶。 n a s a 使用s p i n 检测早在1 9 9 6 年火星探测者所存在的错误，结果发现一些错误是可以在发 射之前就可以被改正的s p i n 从此就被用来检测土星火箭控制软件和一些应用与外层空间的程 序。 l u c e n t 公司也发现了s p i n 的优点，p a t h s t a r a c c e s ss e r v e r 是受益于h o l 2 a n a r m ( s p i n 开发者) 的工作的第一个l u c e n t 产品，h o l z m a n n 用s p i n 检测了5 e s ss w r c h 的新版本代码，这个软件现 在用于l u c e n t 的灵活性部分来改善软件测试的过程。 s p i n 良好的算法设计和非凡的检测能力得到了a c m ( a s s o c i a t l o nf o rc o m p u t i n gm a c h i n e r y ) ( 世界最早的专业计算机协会) 的认可，在2 0 0 1 年授予s p i n 的开发者h o l z m a n n 享有声望的软件 系统奖( s o f t w a r es y s t e m sa w a r d ) ( 其它获得该奖的还有u n i x ，t c p i p ，t c l t k j a v a , w w w 等) 。h o l z m a n n 由此成为继k e nt h o m p s o na n dd e n n i sr r c h i e ( u n i x 的开发者) 和j o h nh l c h a m b e r s ( s 系统的开发者) 之后又一个获得此项殊荣的贝尔人迄今为# s p i n 也是唯一获得 a c m 软件系统奖的模型检测工具 2 0 0 2 年4 月份在多伦多颁发此奖时，提名表扬s p i n 为：“使用先进的理论的验证方法可以 被用于大型的和高度复杂的软件系统中” a c m 的c e oj o l l l i & w h i t e 说道：“g e r a r dh o l n a n n 的s p i n 系统有着非常聪明的查找技 术，因为它不但可以在有限的内存空间中快速的对软件进行检测，而且它可以保证程序在按照 它们原有的工作方式下被检测。” s p i n 是针对软件的检测工具，它是用a n s ic 开发的，可以在所有u n i x 操作系统版本使 用，也可以在安装了l i n u x 、w i n d o w s 9 5 以上版本等操作系统中使用。在使用s p i n 软件进行检 测时，系统还要安装a n s ic 编译软件 2 1 2s p 琳的特征 s p i n 验证主要关心的问题是进程之间的信息能否正确的交互，而不是进程内部的具体计 算。s p i n 是一个基于计算机科学的“形式化方法”，将先进的理论验证方法应用于大型复杂的 软件系统当中的模型检测工具。如今s p i n 被广泛的应用于工业界和学术界其特点如下： 1 ，s p i n 以p r o m e l a 为输入语言，可以对网络协议设计中的规格的逻辑一致性进行检验，并报告 系统中出现的死锁、无效的循环、未定义的接收和标记不完全等情况。 2 s p i n 使用o i l m e - f l y 技术，即无需构建一个全局的状态图或者k r i p k c 结构，而可以根据需要生 成系统自动机的部分状态。 3 s p i n u - 当做一个完整的m ( l i n e a r t e m p o r a l l o g i c ) 模型检验系统来使用，支持所有的可 1 0 ， l “f 。f * 用的线性时态逻辑表示的正确性验证要求，也可以在有效的o n - t h e n y 检验系统中用来检验 协议的安全特征。 4 s p i n 可通过使用会面点来进行同步通信，也可以使用缓冲通道来进行异步通信。 5 对于给定的一个使用p r o m e l a 描述的协议系统，s p i n 可以对其执行随意的模拟，也可以生成 个c 代码程序，然后对该系统的正确性进行有效的检验。 6 在进行检验时。对于中小规模的模型，可以采用穷举状态空间分析，而对于较大规模的系 统，则采用b i ts t a t eh a s h m g 方法来有选择地搜索部分状态空间。 2 1 3 基于s p i n 的协议分析 用s p i n 对协议进行模拟分析，来确定协议的正确性。正确性是指：不存在违背断言 ( a s s e r t i o n ) 的情况、不存在死锁( d e a d l o c k ) 、不存在“坏的”循环、满足我们定义的l t l 公式。 在s p i n p r o m e l a 模型中主要由：断言( a s s e r t i o n ) ，特殊的标记和n e v e r c l a i m s 三种方式来实现。 一个“断言”( a s s e r t 语句) 是一个逻辑表达式。它可以出现在所描述的模型中的任何位置， 并在任何时候都是可以执行的。它相当于指定系统的一个“不变式”，无论什么时候这个表达式 的值都应为真。在s p i n 执行a s s e r t 语句时，如果该语句所指定的条件成立( 表达式的值不为o ) ， 则不产生任何影响；但如果条件不成立( 表达式的值为o ) ，将产生一个错误报告。在p e o m e l a 模型中经常使用a s s e r t 语句来检验在某状态时某个性质是否成立。 死锁( d e a d l o c k ) 是系统运行到某个状态后不能再转向其它任何一个状态在s p i n 验证过 程中如果出现死锁情况，验证器将会给出“i n v a l i de n ds t a t e ”提示语句。要验证p r o m e l a 所描述 的一个系统是否存在死锁，验证器就要能够将正确的结束状态和异常的结束状态区别开来。在一 一个执行序列结束时，最好是所有的进程的实例都运行到了其相应进程体的最后，并且所有的 消息通道都为空然而有的时候，并不一定要求所有的进程都到达了它们进程体的最后才能说 明不存在死锁，其中有的进程可能会停留在空闲状态，也可能会在某些状态循环，等待某个消 息的到来后再进行其他操作为此，在建模的过程中可以用“e n d ”标记来标识正确的结束状态，_ 一个“坏”的循环是指系统不断重复执行一些错的或是没有意义的行为。建模过程中可以 设置“a c c e p t ”标记( 主要用于n e v e r 声明中) ，然后指定验证器找出所有至少执行过一次此标 记语句的循环，如果这样的循环不存在则说明系统是正确的。也可以设置“p r o g r e s s ”来标记一 些必须要不断重复被执行的语句，如果存在没有经过“p r o g r e s s ”的循环，则说明有“坏”的循 环存在 一个线性时序逻辑公式可以表达比“从不发生”或“总是发生”或“不断的发生”这些属 性更复杂的系统要求。比如，系统要求满足“事件p 发生则能得到事件q 也发生了”这个规 范约束条件，这时你就可以用线性时序逻辑公式门( p q ) 来检测看你的系统是否能够满足这二 个条件s p i n 提供了将线性时序逻辑公式翻译为相应的n c v e r c l a i m s 的功能，使用起来相当的 方便 t 2 1 4s p i n 检测的基本过程 s p i n 可以用在三个基础模型中【2 8 1 ： 1 ) 作为一个模拟器，允许快速对建立的系统模型进行随意的、引导性的或交互的仿真 2 ) 可以作为一个详尽的分析器，严格的证明用户提出的正确性要求是否满足( 使用偏序 简约进行最优化检索) 。 ”用于大型系统近似性证明，用s p i n 可以对大型的协议系统进行有效的正确性分析，即 使这个系统覆盖了最大限度的状态空间 s p i n 首先从一个描述的协议系统的高层模型规格开始，经分析没有语法错误后，对系统的 交互进行模拟，直到确认系统设计拥有预期的行为；然后，s p i n 将产生一个用c 语言描述的验 证程序，经检验器编译后被执行，执行中如果发现了违背正确性说明的任何反例，则可反馈给 交互模拟机，通过重现细节剔除引起错误的原因。图2 1 描述了整个的检测过程： 2 2s p i n 的安装和使用 图2 - 1s p i n 模拟和检验的基本过程 2 2 1w i n 3 2 环境下s p i n 的安装和使用 从【2 9 】下载最新的p c _ s p i n * z i p 文件，解压p c _ s p i n * z i p 然后将s p i n * c x e 拷贝到例如d ：k s p i n 下，进入控制台，转到d ：、s p i n 目录下就可以用s p i n 的当前版本对模型进行检测了，在v c 6 0 环境下，编译s p i n 产生的p a n c 文件，得到p a n e x e 我们就可以在w i n d o w s 环境下对模型进行相应的检测和错误迹观察了。 2 2 2 c y g w i n 环境下s p i n 的安装和使用 如果我们只是将刚刚解压得到的s p i n “e ，拷贝到c y g w i n 、：b i n 下的话，相当于我们还是在 w i n d o w s 平台操作s p i n ，下面我们将给出如何完全的仿真u n i x 环境使用s p i n 的操作： 第一步，先下载t ! t p ：f i p c s b e r k e l e y e d u u e b 4 b s d b y a c c t a r z 用编译y a c c c x e ： 将b y a c c t a r z 解压： g u n m p m r z t a r x f + t a r 然后用m a k e 编译，若有错误再用下面命令编译： g c c _ o y a c c + o 将y a c e e x e 拷贝到e y g w i n 、b i n 下( 或s r c + 目录下) 第二步，编译s p i n 1 ) 在 2 9 3 处下载s p i n * t a r g z 放在一个空目录中 2 1 解压： g u n z i p t a r g z t a r - x f + t a r 3 ) 转到s r e * 目录下 c ds r e * 4 ) 打开文件m a k e u n i x ，将第1 2 行等号后的c c 命令改为g e e ，保存 5 ) m a k e f m a k e _ u n i x 6 ) 将生成的s p i n e x e 放到e y g w i n 、b i n 下，然后参考t e s t r e a d m e t e s t s 进入测试 阶段。 注：将测试中的c c 命令换成g c c 命令即可将c y g w i n b i n 中的e p p c x e 拷贝到e y g w i n 、l i b 下，执行t e s tl ，在第五步和第九步中生成p a n “e ，用p a n l 和p a n a 来验证。 1 2 2 3s p i n 的图形界面工具x s p i n 的安装和使用 2 3 1 x s p i n 的安装 在f 2 9 】处下载x s p i n * t c l ，将x s p i n * 1 c l 改名为x s p m 拷贝到c y g w i n 的似f 虾。打开此文件， 在文件的前几行你会看到该软件默认执行的路径是c ：e y g w m b m x s p m 将此项改为你所安装的 c y g w m 的路径然后保存即可。在e y g w i n b m 下找到w