（计算机软件与理论专业论文）实时模型检测中精确加速的研究.pdf

原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研 究所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的科研成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本声明的法律责任由本人承担。 学位论文作者：尹传龙日期：彬年妫。日 学位论文使用授权声明 本人在导师指导下完成的论文及相关的职务作品，知识产权归属郑州大学。 根据郑州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部 门或机构送交论文的复印件和电子版，允许论文被查阅和借阅；本人授权郑州 大学可以将本学位论文的全部或部分编入有关数据库进行检索，可以采用影印、 缩印或者其他复制手段保存论文和汇编本学位论文。本人离校后发表、使用学 位论文或与该学位论文直接相关的学术论文或成果时，第一署名单位仍然为郑 州大学。保密论文在解密后应遵守此规定。 学位论文懈穸磅蔻 日期：彬年；- n 岁口同 摘要 摘要 实时系统经常会出现不同的时间度量。然而，当这些系统建模成时间自动 机，然后运用符号模型检测技术进行验证时，验证速度会由于不必要的符号状 态空间分裂( 片段问题) 而明显下降。 精确加速可以解决由于不同时间度量而造成的模型检测时出现的片段问 题，而且它不改变时间自动机的可达性，并可以有效地加速前向符号可达性分 析。本文中，我们对精确加速原理进行了剖析，提出了一种基于驻留环实现精 确加速的方法，解决了原来精确加速中附加环的大小需要依赖于可加速环窗口 的问题，使得时间自动机精确加速模型的构造更加的简单快捷。同时我们还利 用得出的推论，探讨了一种快速计算驻留环边界条件的方法，虽延时了加速的 时机，但避免了可加速环窗口的复杂计算。 此外，为了实现精确加速，还提出了一种识别时间自动机中可加速环的方 法。针对时间自动机规模较大的问题，在识别可加速环的方法中引入拓扑排序 的思想，通过简化时间自动机的规模，提高了识别时间自动机中可加速环的效 率。通过实例验证和复杂度分析说明该方法是可行的。 关键字：模型检测；时间自动机；精确加速；可加速环；窗口；回路 a b s t r a c t a b s t r a c t d i f f e r e n tt i m es c a l e sd oo f t e no c c u ri nr e a l - t i m es y s t e m s h o w e v e r , w h e nt h e s e s y s t e m sa r em o d e l e da s ( n e t w o r k so f ) t i m e da u t o m a t a ，t h ev a l i d a t i o nu s i n gs y m b o l i c m o d e lc h e c k i n g t e c h n i q u e sc a ns i g n i f i c a n t l yb es l o w e dd o w nb yu n n e c e s s a r y f r a g m e n t a t i o no ft h es y m b o l i cs t a t es p a c e ( f r a g m e n t a t i o np r o b l e m ) e x a c ta c c e l e r a t i o nc a na d d r e s st h ef r a g m e n t a t i o np r o b l e mi n t h em o d e l c h e c k i n gw h e nd i f f e r e n tt i m es c a l e so c c u ri nr e a l t i m es y s t e m s ，a n di td o e sn o ta l t e r r e a c h a b i l i t yp r o p e r t i e s ，a n da l s oc a ns p e e d - u pf o r w a r ds y m b o l i cr e a c h a b i l i t ya n a l y s i s i nas i g n i f i c a n tw a y i nt h i sp a p e r , w ep r o p o s ean e ww a yt oc o n s t r u c tt h ea d d i t i o n a l c y c l ei nt h ee x a c ta c c e l e r a t i o nt e c h n i q u e ，w h i c hc a nr e s o l v et h ep r o b l e mt h a tt h es i z e o ft h ea d d i t i o n a lc y c l ed e p e n d so nt h ew i n d o wo ft h ea c c e l e r a t a b l e c y c l e ，a n d m a k i n gt h ec o n s t r u c t i o no fa d d i t i o n a lc y c l e si sm o r es i m p l e ra n dq u i c k e r w ea l s o e x p l o r eaf a s tm e t h o do fc a l c u l a t i n ge d g ec o n d i t i o n s ，t h u se s c a p et oc o m p u t et h e w i n d o wo ft h ea c c e l e r a t e dc y c l e i na d d i t i o n ，t oc a r r yo u te x a c ta c c e l e r a t i o n ，aw a yt o i d e n t i f ya c c e l e r a t a b l e c y c l e si nt i m e da u t o m a t ai sp r o p o s e d i n s p i r e db yt h et o p o l o g i c a ls o r t ，t h em e t h o d i m p r o v e st h ee f f i c i e n c yt oi d e n t i f ya c c e l e r a t a b l ec y c l e si nt i m e da u t o m a t ab y r e d u c i n gt h es i z eo ft i m e da u t o m a t a t h ev a l i d i t yo ft h i sm e t h o db ye x a m p l e sa n dt h e c o m p l e x i t ya n a l y s i si l l u m i n a t et h ef e a s i b i l i t y k e yw o r d s ：m o d e lc h e c k i n g ；t i m e da u t o m a t a ；e x a c ta c c e l e r a t i o n ；a c c e l e r a t e d c y c l e ；w i n d o w ；l o o p i i 目录 摘要l a b s t r a c t ：i i l 引言1 1 1 研究背景1 1 2 研究现状2 1 3 研究内容“5 1 4 本文结构6 2时间自动机“7 2 1 相关背景7 2 2 时间自动机7 2 3 区域自动机1 0 2 3 1 区域等价1 0 2 3 2 区域自动机1 1 2 4 带自动机1 2 2 5 可达性分析1 4 2 6 小结”1 6 3 加速技术分析1 7 3 1 片段问题1 7 3 2 模型增量1 8 3 3 精确加速2 1 3 3 1 环2 2 3 3 2 可加速环2 2 3 3 3 加速”2 3 3 4 加速技术分析2 6 3 5 小结2 8 i i i 目录 4 基于驻留环的精确加速2 9 4 1 精确加速缺陷分析2 9 4 2 精确加速原理分析3 0 4 3 基于驻留环的精确加速3 1 4 4 对比分析3 4 4 5 小结3 6 5一种快速计算边界控制条件的方法3 7 5 1 窗口的计算3 7 5 2 一种快速计算边界控制条件的方法3 8 5 3 实例验证及分析3 9 5 4 小结4 0 6 一种识别可加速环的方法4 1 6 1 相关背景4 1 6 2 模型检测工具u p p a a l 。4 1 6 2 1 用u p p a a l 建模4 1 6 2 2 用u p p a a l 检测4 2 6 3 可加速环识别算法4 4 6 4 实例验证及复杂度分析4 6 6 5 小结4 8 7 总结与展望4 9 参考文献5 0 致谢5 3 个人简历在学期间发表的学术论文与研究成果5 4 i v 1 引言 1引言 1 1研究背景 随着计算机科学的发展，工业界越来越重视借用严格的数学工具来保证系 统的f 确性和可靠性。因此，形式化的模型检测方法得到了广泛的接受和应用。 模型检测的基本原理在于先为系统建立形式化模型，说明想要检测的性质，然 后用算法去检测该模型是否满足所述性质，它的基本思想是状态空间的穷尽搜 索。效率是模型检测技术在系统验证和证明中最重要的方面。目前，影响模型 检测技术应用的主要问题是规模较大时状态空间的搜索时的效率问题。事实上， 系统状态空间一般是与组件的大小成指数增长的，这就导致系统的实际验证常 常变得较为复杂。对于这个问题，实际的解决方法是对特殊应用领域中的算法 和数据结构进行优化。 实时系统是一类重要的计算机系统，它需要满足一定的时间约束条件，如 执行时间、应答时间、延迟等。时间自动机非常适合建模实时系统及时间起主 导的协议，它是实时时间系统建模和证明的一种理论。其他具有相同功能的形 式化的方法有时间p e t r i 网，时间进程代数，实时时间逻辑等。在砧u r 和d i l l 的工 作基础之上，许多以时间自动机为输入语言的模型检测器的开发也逐渐流行起 来，而且目前这些工具已经被应用到了许多安全的研究中，如模型检测工具 u p p a a i ，和k r o n o s 。 可编程逻辑控制器( p l c s ) 在工业中广泛用于控制实时嵌入，如铁路枢纽， 电梯及生产线等，它的体系模型结构是简单而又强大的轮询实时系统。轮询实 时系统( p o l l i n gr e a l t i m es y s t e m ) 以一个可以分成三部分的环工作：输入待检测 的值，由输入和旧的状态计算得到新的局部状态和输出值，最后新的输出值写 入到输出端。在这样的系统中经常会运用不同的时间度量，当用时间自动机对 这样的系统建模，然后运用符号模型检测技术进行验证时，验证速度会由于不 必要的状态空间分裂( 片段问题) 而明显下降。结果，模型检测所需要的时间 和空间就增加了。这个问题一般出现在符号模型检测中，时间自动机由于等待 控制程序的某种行为，从而导致了大量的符号状态空间片段。 事实上，在用u p p a a l 工具证明l e g o 程序的时候，片段问题就早已出现， 1 引言 对此h u n c 和i v e r s e n 也已经给出了描述雎3 3 。例如，图1 1 是控制程序和环境的 模型的例子。建模控制程序的自动机是以微秒为单位，而建模环境功能的自动 机是以秒为单位。这种差别就会引起符号状态空间不必要的片段。此外，在实 时轮询系统，如可编程的逻辑控制器，以及考虑上下文的通信协议的验证中也 会出现片段问题。片段问题的出现导致了检测效率的降低。 e m i r o n m e n tc o n t t o lp r o g r a m 2 | 。 s c h t n 图1 1 控制程序和环境的模型 1 2 研究现状 模型检测是- - 1 7 成熟的技术，它是基于对某一整个状态空间模型的穷尽探 索来完成系统检测和通信协议验证的。时间自动机的验证技术实际上也是基于 状态空间穷尽探索来完成的，但由于时间自动机引入了实数作为时钟变量，在 验证过程中就会产生大量的中间状态，这也大大超出了计算机的存储能力，从 而导致了状态爆炸问题。对于这个问题，一种方法是通过适当的等价替代来约 减产生的整个状态空间，最后在约减后的状态空间上进行检测，这就是静态约 减方法。另一种方法是利用模型有关信息实时计算出状态空间，即边生成状态， 边约减，这就是动态约减方法。 c o n v e xh u l l 抽象就是一种静态约减的方法。在时间自动机中，一个符号状 态由位置和时钟带组成，即使在同一个位置也会存在不同的符号状态，因为彼 此的时钟带不同。 2 1引言 如果有两个时间区域d 1 和d 2 ，那么满足d 1 d 且d 2 d 的最小时间区 域d 就称为c o n v e xh u l l 。图1 2 表示的就是c o n v e xh u l l 的例子。图1 2 的右边 表示的是时钟带z 1 和时钟带z 2 的并集还是一个时钟带，而图1 2 左边的时钟带 z 1 和时钟带z 2 的并集不是凸的。因此，经过c o n v e xh u l l 操作后可达的符号状态， 在c o n v e xh u l l 操作前不一定可达。 j ，。 旋 磊 j 一曼， 。 图1 2c o n v e xh u l l 操作 图1 2 告诉我们c o n v e xh u l l 抽象技术能够减少生成的状态数目，约减了状 态空间，虽然它具有不完备性的特点，改变了可达性，但是它可以保证安全性。 只要经过c o n v e xh u l l 抽象操作后不满足的性质，在c o n v e xh u l l 抽象操作前也一 定不满足这种性质。 。 m o i l e r 提出的增量模型踟的方法实际上就是属于c o n v e xh u l l 抽象技术的一 种，它是基于一个时间自动机的句法调整来加速状态空间搜索，可以解决片段 问题，并且构造方便，但很可惜，由于具有不完备的特点，不能保证可达性。 转换合并( t r a n s i t i o nm e r g e ) 也是静态约减方法的一种，如果在模型中有两 个连续局部不可见的行为，那么转换合并就可以用将它们静态合并成一个原子 行为。精确加速是一种转换合并n 6 。1 ，主要用来解决上述由于时间度量而造 成的状态空间分裂问题，而且它并不改变时间自动机的可达性，并可以有效加 速前向搜索可达性分析。早在文献 2 2 中的符号系统证明中也有类似的技术， 离散控制图用静态分析来检测“兴趣环”，用元转换来计算这些环的反复迭代。 这样有了这些元转换后，加快了状态搜索，提高了效率。为了分析建模成有穷 自动机的通信协议，运用q d d s 的符号技术也引用了元转换来加速状态空间的 搜索妇3 2 4 1 。用一个元转换来关联在控制图中特殊的环，如反复从一个信道接收信 息的环，这样有了元转换之后就可以计算出反复执行这些特殊环能到达的所有 状态。然而，在这些方法中，只有少数的环能够被加速，这是主要是受限于q d d s 表达能力。为了克服这个问题，引入了约束q d d s ，这样就可以加速控制图中的 3 1 引言 所有环5 i 。基于同样的思想，m a r t i j nh c n d r i k s n 3 第一次将这种加速技术应用到时 间自动机，提出了精确加速的概念。在精确加速中，也是通过添加的元转换来 计算时间自动机中反复执行一个环可以到达的所有状态，这样也加快了状态空 间搜索，并可以保证可达性。 在国外，由r o b e r tb o s c h 随3 提出的汽车外围监管( c a rp c r i p h e r ys u p e r v i s i o n ) 系统是一种混合系统，用时间自动机对系统进行建模，模型将非线性的连续的 变量分割成有穷个状态区域，而将连续变量上的约束对应成时钟约束。由于在 环境和c p s 组件中存在的不同时间度量，从而会引起了状态空间的无限增大，在 文献中是用c o n v e xh u l l 技术来处理，最后由于不能保证可达性，提出了用精确加 速来解决该问题的研究设想。 线性关系分析( l i n e a rr e l m i o n a n a l y s i s ) 可以计算程序的上界近似可达状态， 它能应用在许多领域，如编译时错误诊断。州，自动验证心6 2 7 1 和形式化证明等瞳吼 2 9 3 。和许多近似验证方法一样，u 溘面临着精度和代价之间的折衷问题，较高 的代价限制了它的应用。在文献 9 中，作者将加速应用在线性关系分析中，不 但补充了合并扩展操作，而且可以提高分析的精确性和性能。j d r 6 m el e r o u x n 伽 等将加速的应用也从符号证明扩展到数据流分析中，与传统的基于扩展的抽象 技术相比，这种方法可以通过选择抽象域来控制精度，而且精度也不再依赖于 抽象值计算的方法。最近也有文献提出将加速技术和基于插补 ( i n t e r p o l a t i o n b a s e d ) 模型检测合并应用，基于插补的模型检测可以提供有效的 自动抽象方案，帮助加速技术处理更小的块。同样加速技术可以帮助基于插补 的模型检测处理更复杂的行为u 。 在国内，模型检测中的加速技术方面的研究主要集中在关于可达性的约减 技术上。文献 3 1 介绍了可达性分析中的几种比较流行的状态空间的约减技术， 它将约减技术分为两类，一类是针对时钟约束的约减，另一类是针对路径遍历 的约减。针对时钟约束的约减技术又分为静态方法与动态方法两类。静态方法 是在检验之前分析或利用局部信息进行的约减方法；动态方法是在检验过程中 分析或利用全局信息的约减方法。针对路径遍历的约减，主要介绍了偏序优化 技术。紧接着作者又提出了一种动态约减方法，该方法利用在验证过程中相邻 符号间的依赖关系，删除无关原子公式，从而达到约减状态的目的。此外，文 献 3 3 提出的求复合后继的方法也能有效地约减状态空间。 虽然加速技术在不断地发展进步，然而精确加速在实际应用中还是存在一 4 1 引言 些问题的，而且据我们所知，还没有文献专门对精确加速中存在的这些问题进 行解决。 首先，在精确加速过程中，关键技术在于它为时间自动机添加了个附加 环，构造了它的加速模型。然而，构造附加环时需要可加速环的次数取决于可 加速环窗口，即 a ，b 。当a b 比值接近1 时，比如a - - 1 0 0 ，b = 1 0 1 ，我们在 构造附加环的时候，就需要1 0 0 个可加速环，这种情况下，精确加速虽然加速 了可达性分析，但还是大大增加了状态空间，同时也增大了构造附加环的难度， 给构造加速模型带来了不便。显然，构造附加环依赖于可加速环窗口的条件限 制了精确加速在实际中的应用。 同时要想应用精确加速技术，首先要识别出时间自动机中的可加速环。如 何识别出时间自动机中的可加速环就成为了精确加速技术的重要环节，同时也 是完成精确加速的最基础步骤。 1 3 研究内容 本文中，我们对精确加速如何解决片段问题而不改变可达性进行了描述， 对精确加速应用时存在的一些问题进行了总结，指出了精确加速构造附加环时 存在的问题。针对这些问题，本文主要在以下几个方面进行了研究： 1 ) 利用一个经常出现在控制系统的实例，构造它的加速模型，通过前向 可达性分析对比，解释了精确加速是如何解决由于不同时间度量而造成的片段 问题的，并结合图表分析，指出了精确加速可以加速前向可达性分析的原因在 于加速模型合并了状态片段，可以保证可达性的原因在于加速模型没有一开始 就对出现的片段进行合并加速，而是通过执行附加环等待复位位置上出现交集 时钟带之后才开始合并。 2 ) 利用分析得到的精确加速原理，提出了一种基于驻留环实现精确加速 的方法。该方法利用边界控制条件来控制进入驻留环的时间，从而达到控制加 速时机的目的。相比原来精确加速，首先，基于驻留环的精确加速是建立在精 确加速原理之上的，同样也加速了前向符号状态搜索，且不改变可达性。其次， 向时间自动机添加的驻留环的大小是固定的，这样就解决了原来精确加速中附 加环大小需要依赖可加速环窗1 3 的问题，使得构造时问自动机精确加速模型更 加的简单快捷。最后，驻留环是简单的，仅由一个位置及其边界条件组成，相 1 引言 比原来的精确加速，也会大大节省存储空间。 3 ) 基于驻留环的方法和原来的构造方法一样也都需要计算可加速环窗口 的大小。不同的是，原来构造方法中窗口用来确定构造附加环需要可加速环的 次数，这里我们需要窗口是为了得到控制条件。我们利用得出的推论，探讨了 一种快速计算驻留环边界条件的方法，虽然延迟了进行驻留环的时间，但避免 了可加速环窗口的复杂计算，在实际应用中是可以考虑的。 4 ) 受拓扑排序的启发，还提出了一种识别时间自动机中可加速环的方法。 方法并没有直接将图论中输出有向图回路的算法应用到识别可加速环中，而是 利用拓扑排序的思想，先将时间自动机的规模进行简化处理，然后才对处理后 的时间自动机再利用有关识别有向图回路的算法，输出时间自动机中的可加速 环，这样就提高了效率，也为构造时间自动机的加速模型并完成加速奠定了基 础。 1 4 本文结构 本文第2 章介绍了时间自动机的有关概念，包括时间自动机的语义、语法 和带自动机等基本知识。 第3 章首先用实例解释了片段问题，接着介绍了两种加速技术，分析说明 了两种加速技术是如何解决片段问题的，最后对两种加速技术进行了对比分析。 紧接着第4 章先细致分析了精确加速的原理，指出了精确加速构造附加环 时存在的问题。针对该问题，提出了基于驻留环实现精确加速的方法用来解决 构造附加环的问题。 为了避免可加速环窗口的复杂计算，第5 章提出予一种快速计算控制条件 的方法。 第6 章给出了一种识别可加速环的方法，并通过模型检测工具u p p a a l 进 行了实例验证及分析了算法复杂度。 最后是总结与展望。 6 2 时间自动机 2 时间自动机 2 1 相关背景 实时系统有着广泛的应用，尤其经常用在对时间有特殊要求的装置上。实 时系统要求具有很高的可靠性，即使系统在设计时出现微小的错误，通常也将 会引起非常严重的后果。随着实时系统中硬件和软件的规模及功能的增加，这 类系统设计的难度及设计中包含偏差的概率也随着大大增加，这就给软件和硬 件产品的可靠性带来了重大的挑战。因此，工业界希望利用形式化方法和相应 工具，帮助设计人员在产品设计的早期阶段就能发现逻辑错误。 传统的模型检测技术对时间没有一个清晰的建模，而且不适合分析可靠性 依赖于不同延时大小的实时系统。因此，时间自动机作为建模实时系统行为的 一种形式化符号而被引入。它的定义提供了一个简单而又全面的方法，为模型 检测的发展提供了扎实的基础。许多年以来，该方法已经得到了广泛研究，在 验证算法、模型检测和工具上都取得了进步。 时间自动机本质上是一个扩展到实数变量的有穷自动机( 一个包含了有穷 节点集或位置集和边集的图形) 。这样一个自动机可以作为一个时间系统的抽象 模型。变量对系统中的逻辑时钟建模，当系统开始时，它们被初始化为0 而且以 相同的速度同步增加。时钟约束如边界约束，用来限制自动机的行为。当时钟 值满足边上的边界，用边表示的转换可能被触发。当一个转换触发时，时钟可 能复位为0 。 2 2 时间自动机 假定x 是时钟集，时钟约束的集合( x ) 定义如下，其中x x ，c n ， 表示二元关系 ， 驴：= x cl 1 八2 从x 到r + 的映射集合是x 的时钟解释v ，其中r + 是包含0 的正实数集。当 且仅当满足v 给定的值时，我们说时钟解释v 满足时钟约束，记作vl = 。 对于d e r ，v + d 也是时钟解释，它将每一个时钟变量赋值为v ( x ) + d ；对于 y - x ，v 【y = o 】也是时钟解释，它将每一个时钟变量x y 复位为0 ，对于x 喏y 7 2 时间自动机 的时钟变量，时钟值保持不变。 定义2 1 n 2 1 ( 时间自动机) 时间自动机a 是一个( 厶产，z 厶历元 组，其中是有穷位置集，产是初始位置集，是有穷事件集，堤时钟集， 是映射，它为每个位置z 分配了一个位置不变式，e l x x 2 。西( 肋x l 是转换规则集。一条转换( z ，a ，矿，a ，z ) 表示如果当前位置，的时钟解释满 足时钟约束驴，那么系统可以通过实现事件a 从位置z 转换到另一个位置n 同时 把a 胂的所有时钟复位。 时间自动机a 的语义是定义了一个和它相关联的转换系统s a 。一个s a 状态 是( z ，v ) 对，其中z 是a 中的一个位置，v 是x 中的一个时钟解释使得v 满足i ( z ) 。 在s a 中有两种类型的转换： 1 ) 由时间流逝引起的延时转换：对于一个状态( s ，v ) 和一个实数增量 d 0 ，( s ，v ) ( s ，v + d ) 成立，当对于所有0 d 6 ，v + d - 满足不变式i ( s ) 。 2 )由状态开关引起的行为转换：对于一个状态( s ，v ) 和一个转换 ( s ，a ， 驴，九，sv ) 使得v 满足够，( s ，v ) ( s ，v 九：= 0 1 ) 。 定义2 2 ( 时间轨迹)假设m = ( l ，z o ，以厶助是一个时间自动 机，我们说一个有穷或无穷序列( ( z o ，v 0 ) ，( z 1 ，v 1 ) ，) 是m 的一个( z ，v ) 时间轨迹，当 1 ) l o = l ，v 0 = v ，且 2 ) ( ( 1 i ，v i ) ，( 1 i + 1 ，v i + 1 ) ) 是一个a 行为转换，a 或一个6 延时转换，6 r + ， 对于所有出现在轨迹中的i 0 。 ( z ，v ) 轨迹是压缩的，当( z ，v ) 轨迹以一个延时转换开始，且不包括两 个连续的行为或延时转换，而是每个行为转换后紧跟着一个延时转换，每个延 时转换紧跟着一个行为转换。 假定t r ( m ) 表示时间自动机m 的所有( 1 0 ，v i n i 。) 轨迹集合，其中l o 是m 的初始状态，且v i i l i t ( x ) = o ，对于m 中的所有时钟x 。 例1 实时系统通常包含一个控制程序，它通过传感器来控制和监管外界环 境。用时间自动机建模和证明实时系统不仅需要一个组成控制程序任务的模型， 还需要一个环境模型。图2 1 的时间自动机p ，它表示一个控制程序和外界环境 的简化模型。环l 0 ，l 1 ，l 2 对应控制程序，时钟z 用来建模外界环境。只要在 位置l 0 ，时间自动机就会考虑能否满足外界环境z ；，l a r g e 条件，从而导致跳 2 时间自动机 出控制环。因此，阀值常量l a r g e 的大小决定外界环境对控制程序执行时间反 应的快慢：即常数越大，反应越慢。 1 2l 1 图2 1时i 司自动机p 时间自动机可以定义成一个乘积构造，这样一个复杂的系统就可以表示成 各个组件的乘积。 定义2 3 ( 乘积构造) 假设a 1 = ( l 1 ，l 1 ”，e 1 ，x 1 ，1 1 ，e 1 ) ，a 2 = ( l 2 ， l 2 u ，2 ，x 2 ，1 2 ，e 2 ) 是两个时间自动机。如果时钟集x 1 和x 2 是不相交的， 那么a 1 和a 2 乘积，记为a 1a 2 ，它是这样一个自动机( l l x l 2 ，l 1 0 x l 2 0 ， e 1oe 2 ，x l ux 2 ，i ，e ) ，其中，i ( s l ，s 2 ) = i ( s 1 ) a 1 ( s 2 ) 且转换定义如 下： 1 对于a 1 n e 2 ，每个( s l ，a ，t p l ，九1 ，s l ) 属于e 1 且每个( s 2 ， a ， 92 ，娩，s 2 ) 属于e 2 ，则e 包含( ( s 1 ，s 2 ) ，a ，驴1 八驴2 ，九1u 娩， ( s l ，s 2 ) ) 2 对于a y 4 y 2 ， 每个( s ，a ， 驴，九，s t ) 属于e 1 且每个t 属于 l 2 ，贝0e 包含( ( s ，t ) ，a ，妒，九，( s ，t ) ) 3 对于a 2 1 ，每个( s ，a ，妒，九，s t ) 属于e 2 且每个t 属于l 1 ， 贝0e 包含( ( t ，s ) ，a ，缈，九，( t ，s 1 ) ) 因此，乘积的位置是组件位置的组合对，组合后位置的不变式是组件位置 不变式的联合。图2 2 描述了乘积的构造。 很容易证明乘积构造对应的转换系统就是组件转换系统的乘积：s a i l i a 2 和 s a i l i s a 2 是同构的，这表明时间转换系统不仅在行为转换上同步，而在时间流逝 量上也是同步的。 2 时间自动机 图2 2 两个时间自动机乘积的构造 l ，6 ，：= 0 2 3 区域自动机 时间自动机定义的转换系统有无数多个状态，这就致使不能直接应用传统 有穷模型检测算法。针对这个问题，a l u r 通过引入了所谓的区域作为有穷符号 技术来证明可达性是可判定的。 2 3 1区域等价 在时间自动机的状态空间上定义一个等价关系，两个状态等价，当它们位 置相同且在所有时钟值的整数部分一致而所有时钟值的小数部分是有顺序的。 时钟值的整数部分决定是否遇到了一个特殊的时钟约束，而小数部分的顺序决 定哪个时钟先改变它的整数部分。例如，在一个状态中如果两个时钟x 和y 都 是在0 和1 之间，那么关联时钟约束( x = 1 ) 的一个转换执行后紧接着执行关 联时钟约束( y = 1 ) 的一个转换，取决于当前的时钟是否满足( x y ) 。 现在我们给出这个定义的形式化表示。对于任意d e r ，f r ( d ) 表示d 的小 数部分，厂6 1 代表d 的整数部分；即，d = r 艿_ l + f r ( d ) 。对于每一个时钟x x ， c x 是出现在不变式或边界的时钟约束中的最大整数。 定义2 4 ( 区域等价) 定义在所有时钟解释集上的等价关系丝称为区域等 价。对于两个时钟解释v 和v ，v - - - v 当且仅当下列条件成立： 1 对于所有x x ，或者忡) 1 和m 茹) 相等，或者v ( x ) 和v ( x ) 都大于c x 2 对于所有x ，y x ，v ( x ) c x ，v ( y ) c v ，f r ( v ( x ) ) f r ( v ( y ) ) 1 0 2 时间自动机 当且仅当f r ( v ( x ) ) f r ( v ( v ) ) 3 对于所有x ，y x ，v ( x ) c x ，f r ( v ( x ) ) = o 当且仅当f r ( v ( x ) ) ：= 0 我们用【v 】表示v 所属的时钟区域。每一个区域都能通过它所满足( 有穷) 的时钟约束来唯一确定。川。例如，两个时钟v ( x ) = 0 5 和v ( v ) = o 8 的一个 时钟解释v ，在【v 】中的每一个时钟解释都满足约束( 0 x y 1 ) ，从而，就可 以用【0 x y 1 】代表这个区域。 对于a 的一个时钟约束9 ，如果v 丝v ，那么v 满足驴当且仅当v 满足够。 一个时钟区域满足一个时钟约束9 当且仅当在该区域中的每一个时钟解释满足 伊。 可以得到时钟区域数目的上限为k ! 宰2 1 - h x ( 2 c x + 2 ) ，其中k 是时钟数目。 因此，时钟区域数目与时钟约束的编码成指数关系。 2 3 2 区域自动机 当等价状态有相同位置和区域等价时钟解释时，时钟解释上的区域等价关 系丝就可以扩展为状态空问的等价关系：( s ，v ) 丝( s ，v ) 当且仅当s = s 且v - - 丝v t 。 定义2 5 ( 区域自动机) 假定时间自动机a = ( l ，t o ，x ，i ，e ) ，其 区域自动机r ( a ) 为： r ( a ) 的状态为( ，a ) 的形式，其中l l ，a 是一个时钟区域 初始状态为( 如，【v o 】) 的形式，其中l o z o ，对任意x x ，v o ( x ) = 0 r ( a ) 的转换为( ( s ，a ) ，( s - ，a ) ，仃) 当且仅当( 舢) o ( s ，v ) 其中v e 口，v 口。 3 1 d 2 时间自动机 图2 4 时间自动机a 。，的区域自动机r ( a 。，) 例2 考虑图2 3 中的时间自动机i o 对应的区域自动机r ( a 0 ) 由图2 4 表 示。图2 4 表示了自动机从初始区域( s o ， x - - y - - 0 ) 可达的区域，其中c x - - - - - 1 ， c y - - - - 1 。 2 4 带自动机 区域自动机的区域数目与时钟成指数增长，为了进一步减少区域的数目， 从而提出了带自动机的概念。 在图2 4 的区域自动机中，初始区域包含单个状态( s o ，x - - y = o ) ，它的三 个后继，对应的时钟区域分别为【y = 0 x 1 】。 有一种策略是把这三个区域合并得到【y = o 】。这些凸的时钟区域的合并区域称为 时钟带。时钟带是由时钟约束联合描述的时钟解释集，而且每个时钟约束中的 时钟或不同的两个时钟都有上界或下界。时钟带在语法上是这样定义的： 9 ：2x cix cic ( xic xlx - y cix - y ci 驴1 at p2 对于一个时钟带驴，满足妒的时钟解释也记为妒。如果a 有k 个时钟，那么 集合妒在k 维的欧几里得空间中是一个凸的集合。时钟带有下面的性质： 1 每个时钟区域都是一个时钟带。 2 对于一个时钟区域和一个时钟带妒，或者p 完全被驴包含，或者与妒的 1 2 2 时间自动机 交集为空。 3 两个时钟带的交仍是一个时钟带。 4 位置不变式和转换的每一个时钟约束都是一个时钟带( 由1 和3 得到) 5 对于两个时钟带驴和，如果并集妒u 是凸的，那么它也是一个时钟带。 建立在时钟带上的可达性分析运用了以下三个操作。 对于两个时钟带驴和妒，两个带的交也是一个带，记作驴八驴。 对于一个带妒，用妒f 表示时钟解释集v + d ，v 舻且d e r 。时钟带 在这个操作下是封闭的：对于一个时钟带驴，集合9f 仍是一个时钟 带。 对于时钟的一个子集九和一个时钟带驴，驴队：= 0 1 表示时钟解释集 v 【九：= 0 】，v 妒，v 【九：= 0 】也是一个时钟带。 带是一个( s ，t p ) 对，其中s 是一个位置和够是一个时钟区域。我们可以 定义一个带的转换系统。假设一个带( s ，够) ，时间自动机a 的一个转换e = ( s ， a ，妒，九，s ) 。s u c c ( 妒，e ) 表示一个时钟解释集v ，它使得对于某些v 舻， 状态( s ，v ) 可以通过时间流逝和执行e 转换从状态( s ，v ) 可达。即，( s ， s u c c ( 驴，e ) ) 集描述了带( s ，伊) 在e 转换下的后继。为了得到s u c c ( 妒，e ) 集，需要以下步骤：( i ) 9 与s 的不变式相交( i i ) 执行f 让时间流逝( i i i ) 与s 的不变式相交( i v ) 与e 的时钟约束妒相交( v ) 复位九中的时钟。第一步和第 三步保证了在时间流逝时满足不变式。因此， s u c c ( 驴，e ) = ( ( ( 妒八i ( s ) ) 1 f ) 八i n v ( s ) 八妒) 队：= o 】 图2 5 时间自动机a 0 的带白动机z ( a 。，) 2 时间自动机 定义2 6 ( 带自动机) 对于一个时间自动机a 来说，带自动机z ( a ) 是 这样一个转换系统：z ( a ) 的状态是a 的带，对于a 的每一个初始位置s ，带 ( s ，f x ：= 0 1 ) 是z ( a ) 的一个初始位置，而且对于a 的每个转换e = ( s ，a ， ，九，s ) 和每个时钟带驴，存在一个转换( ( s ，驴) ，a ，( s ，s u c c ( 驴，e ) ) ) 。 例3 图2 5 表示的是图2 3 中时间自动机a 0 的带自动机z ( a o ) 。与图2 4 中它的区域自动机r ( a 0 ) 相比，在带自动机中，每个节点在每一个输入符号 下最多只有一个后继，而且z ( a 0 ) 节点的数目小于r ( a o ) 的节点数目。 2 5 可达性分析 时间自动机a 的一个位置s 是可达的，当位置s 上的某一状态q 是转换系 统s a 的可达状态。可达性问题就是判断某一目标位置是否是可达的。实时系统 安全性需求的验证就是建立在时间自动机可达性问题基础上的。可能，自动机 最有用的功能就是给定一个目标状态或一个目标状态集，然后判断自动机是否 可达。 定义2 7( 可达)( z ，u ) _ ( ，u ) ，当( z ，u ) 与( r ，u ) ，对于 某些仃u r + 成立。对于一个初始状态为( 1 0 ，u o ) 的自动机，( z ，u ) 是可达 的当且仅当( z o ，u o ) _ + ( f ，u ) 。给定一个约束妒，状态( z ，) 是可达的当 ( z ，u ) 是可达的，且u 满足矽。 可达性分析用来检测状态上的属性包括两个基本步，一是自动机状态空间 的计算，二是搜索与目标属性相符或矛盾的状态。第一步在搜索前执行，或在 搜索进行中实时完成。实时计算状态空间比预先计算有一个明显的优势，实时 计算状态空间只用产生验证目标属性所需的部分状态空间。然而，当验证某些 属性如不变式属性时，实时方法也会产生整个状态空间。 算法1 描述了可达性分析算法，它是模型检测工具u p p a a l 的核心。假设 一个时间自动机a 的初始状态集和目标状态集的分别用( z o ，d o ) 和( 矗，毋f ) 表示，k 是时钟单元。算法1 用来检测初始状态是否可以到达到位置为z ，且时钟 赋值满足加的任意状态。它实时计算自动机的带，搜索包含位置z ，且与妒，相交 带的符号状态。对于每个未搜索的符号状态，计算它延时和行为转换导致的后 继，然后与已搜索的状态相比较。如果一个后继已经被搜索过，那么它将被忽 略。另方面，如果一个后继还没被搜索过，那么它将被添加到等待进一步搜 1 4 2 时间自动机 索的状态列表中。 a l g o r i t h m1r c a c h a b i l i 咚* a n a l y s i s p a s s e d = 口，w a i 1 1 = ( 1 0 ，d o ) w h i l e 弧i 了0d o t a k e ( 1 t 功f r o mw a i 1 i f l = l ，a d n 多，口t h e nr e t u r n “y e s ” i f dgd f o r a l l ( 1 ，d p a s s e d t h e n a d d ( 1 d ) t op a s s e l ) 如i 对i l ，d ) s u o h t h a