（计算机软件与理论专业论文）基于时间自动机模型验证技术.pdf

i 。 划 9 基于时间自动机的模型验证技术 摘要 随着计算机科学的发展，工业界越来越重视系统的正确性和可靠性，这样使 得形式化的模型验证方法得到了广泛地应用。通过可达性分析，模型检测可以完 成对实时系统的安全性和活性的验证。它的思想是搜索描述系统行为的转换系 统，然后分析可达状态集合，从而确定系统是否满足规格说明。时间自动机是包 含时间约束的有限状态转换系统，它是使用最为广泛的形式化验证方法之一。 在理论研究部分，首先分析了时间自动机的概念，然后给出了时间自动机的 一些扩展形式。实时系统中的事件能否发生对应着时间自动机某个状态从初始状 态开始能否可达，因此模型验证主要任务是状态可达性分析。验证需要采用了一 些符号化的方法来描述状态，文中首先对时钟区域和时钟带两种方法进行了分 析，然后介绍了可达性分析的两种主要的方法。我们重点介绍了基于二元决策图 的模型验证方法，而使用它的前提是在时间自动机的整数语义下。详细地解释了 如何把整数语义下的状态和转换关系表示成二元决策图的形式。我们给出了在这 种数据结构下的可达性分析算法的改进，对该算法进行了时间复杂度分析，并结 合一个具体的验证实例对空间复杂度进行了分析，表明改进后的算法的时间复杂 度基本不变，同时又降低了可达性分析的空间复杂度。 在应用研究部分，首先是介绍了基于时间自动机的验证工具u p p a a l ，然后 是结合该工具给出了模型验证的步骤和建模的标准，最后构造了飞机着陆控制系 统的时间自动机模型，检测了系统是否安全可靠，避免了系统运行时出现错误。 通过使用验证工具u p p a a l ，我们可以方便地为系统构造模型，有利于设计人员 认清系统的运行过程，及时发现系统中存在的一些问题。 关键词：实时系统，模型验证，时间自动机，二元决策图，验证工具 ， - - i ， 基于时间自动机的模型验证技术 a b s t r a c t w i t ht h ed e v e l o p m e n to fc o m p u t e rs c i e n c e ，i n d u s t r yi si n c r e a s i n ge m p h a s i so nt h e a c c u r a c ya n dr e l i a b i l i t yo ft h es y s t e m f o r m a lm o d e lv a l i d a t i o nh a sb e e nw i d e l yu s e d t h r o u g ht h er e a c h a b i l i t ya n a l y s i s ，m o d e lc h e c k i n gr e a l t i m es y s t e m sc a l lc o m p l e t et h e s a f e t ya n da c t i v i t yo fv e r i f i c a t i o n i t si d e ai st os e a r c hf o rs y s t e mb e h a v i o rd e s c r i b e d i nt h ec o n v e r s i o ns y s t e m ，a n dt h e na n a l y z et h es t a t es e tu pi no r d e rt od e t e r m i n e w h e t h e rt h e s y s t e m t om e e tt h e s p e c i f i c a t i o n t i m e da u t o m a t a ( t a ) i s a t i m e - c o n s t r a i n e ds y s t e mo ff i n i t e - s t a t ec o n v e r s i o n i ti st h em o s tw i d e l yu s e dm e t h o d o ff o r m a lv e r i f i c a t i o n p a r ti nt h e o r e t i c a ls t u d i e s ，f i r s to fa l la na n a l y s i so ft h ec o n c e p to ft i m e da u t o m a t a , a n dt h e ng i v e nan u m b e ro ft ae x t e n d e df o r m r e a l t i m es y s t e me v e n t sc a no o e u ri n t h ec o r r e s p o n d i n gt a 、i t has t a t et os t a r tf r o mt h ei n i t i a ls t a t ec a n r e a c h , t h e r e f o r et h e m a i nt a s ko fm o d e lv a l i d a t i o ni sas t a t er e a c h a b i l i t ya n a l y s i s s t a t ei sd e s c r i b e db y s o m es y m b o l i cw a yi nt h ev a l i d a t i o n w ea n a l yt h ec l o c kr e g i o na n dc l o c kz o n e , t h e t w om a i nm e t h o d so fr e a c h a b i l i t ya n a l y s i sa r eg i v ea tl a s t w ea r ef o c i l s e do nt h e b i n a r yd e c i s i o nd i a g r a mb a s e do nt h em o d e lv a l i d a t i o nm e t h o d s ，a n di ti sp r e m i s e do n t h e 墩o fa u t o m a t e dm a c h i n e si nt i m ei n t e g e rs e m a n t i c s w ee x p l a i nh o wt h e c o n f i g u r a t i o ns e t sa n dt r a n s i t i o n so ft h i si n t e g e rs e m a n t i c s nb er e p r e s e n t e da s b d d s w eg i v et h er e a c h a b i l i t y a n a l y s i sa l g o r i t h mi m p r o v e m e n t sw i t ht h i sd a t a s t r u c t u r e ，t h e na n a l y z et h ec o m p l e x i t yo ft h ea l g o r i t h mw i t l lac o n c r e t ee x a m p l eo f t h ev e r i f i c a t i o n ，s h o wt h a tf o rs o m em o d e l st h er e a c h a b i l i t ya n a l y s i ss e e m st ob eo f p o l y n o m i a lt i m ea n da p a c ec o m p l e x i t y p a r ti na p p l i e dr e s e a r c h , f i r s to fa l li n t r o d u c e dt o o lu p p a a lb a s e dt a ，a n dt h e n g i v e nm o d e lv a l i d a t i o n s t e p sa n dm o d e l i n gs t a n d a r d s i na d d i t i o n ，a tl a s ts t r u c t u r e dt a m o d e l so ft h ea i r c r a f tl a n d i n gc o n t r o ls y s t e ma n dt h ee l e v a t o rc o n t r o ls y s t e m ，a n d v e r i f yt h e i rp r o p e r t y , s oe r r o r sc a l lb ea v o i d e di nt h es y s t e ma c t u a lr u n n i n g t h r o u g h t h eu s eo fu p p a a lv e r i f i c a t i o nt o o l s ，w ec a ne a s i l yc o n s t r u c tm o d e l sf o rt h es y s t e m ， w h i c hw i l lh e l pd e s i g n e r st ou n d e r s t a n dt h eo p e r a t i o no ft h es y s t e mp r o c e s s ，t h e t i m e l yd e t e c t i o no fs o m eo ft h ep r o b l e m st h a te x i s ti nt h es y s t e m k e yw o r d s ：r e a l t i m es y s t e m s ，m o d e lc h e c k i n g ，t i m ea u t o m a t a , b d d ，v a l i d a t i o nt o o l 基于时间自动机的模型验证技术 目录 摘暑要i a b s tr a c t i i 目录i i i 第一章前言。1 1 1 研究背景和意义1 1 2 研究现状2 1 3 本文结构3 第二章时间自动机5 2 1 时间自动机的定义5 2 1 1 时间转换系统5 2 1 2 时间约束和时钟解释。5 2 1 3 时间自动机的语法和语义6 2 2 时间语言7 2 3 时间自动机的扩展。：9 2 3 1 对角时钟约束9 2 3 2 叠加时钟约束1 0 2 3 3 内部动作1l 2 3 4 时钟的更新l l 2 4 本章小结1 2 第三章基于时间自动机模型的验证方法1 3 3 1 模型验证方法。1 3 3 1 1 模型验证的概念1 3 3 1 2 时间自动机建模1 4 3 2 符号化语义和验证1 5 3 2 1 时钟区域1 5 3 2 2 时钟带。l6 3 3 可达性分析18 3 3 1 后向分析法。1 8 3 3 2 前向分析法1 9 3 3 3 差值有界矩阵( d b m ) 2 1 3 3 4 存在的问题2 3 3 4 验证工具2 4 3 5 本章小结。2 6 第四章基于b d d 的验证技术。2 7 4 1 二元决策图( b d d ) 。2 7 4 1 1b d d 的概念2 7 4 1 2 变量顺序对b d d 大小的影响2 8 4 2 时间自动机的b d d 表示方法3 0 4 2 1 时间自动机的整数语义3 0 4 2 2 状态和转换关系3 2 4 3 可达性分析3 6 基于时间自动机的模型验证技术 4 3 1 标准算法3 6 4 3 2 算法改进及复杂度分析3 7 4 3 3 案例分析3 9 4 4 本章小结4 l 第五章应用研究4 2 5 1 验证工具u p p a a l 介绍。4 2 5 1 1 基本功能4 2 5 1 2 最新改进4 3 5 2 验证过程4 4 5 2 1 模型验证步骤4 4 5 2 2 建模标准4 5 5 3 飞机着陆控制系统4 6 5 3 1 问题描述4 6 5 3 2 模型构造4 6 5 3 3 分析验证4 8 5 4 本章小结4 9 第六章结论和展望5 0 致 射5l 参考文献5 2 附录攻读硕士学位期间发表的论文。5 6 基于时间自动机的模型验证技术 1 1 研究背景和意义 第一章前言 实时系统是能及时响应外部发生的随机事件，并能在最短的时间内完成对该 事件的处理的计算机软件系统【l 】。实时系统包括过程控制、铁路调度、敏捷制造、 核反应堆等许多计算机控制系统。在实时系统中，系统的可靠性不仅取决于系统 计算结果的正确而且取决于正确结果产生的时间。如何保证系统的正确性和可 靠性成为日益紧迫的问题，对于并发系统，由于其内在的不确定性，这个问题显 得更加严重。 一般来说，实时系统是一类对安全性和可靠性都有着严格要求的应用系统， 如果能在开发系统过程中尽早发现错误，就可以避免浪费大量人力、资金、物力 等资源。对实时系统进行多次测试和行为模拟是确保其可靠性的两种常规方法 f 2 】。测试是在软件开发结束后，利用事先假设的各种测试用例检测系统的正确性， 然而通过用例测试得到的安全系统很可能仍然无法保证对实际情况做出合理的 响应。行为模拟是在不同情况下检查系统是否可以根据不同的输入而做出相应的 正确行为反应，这是一个不断交互的过程。因此，在软件系统开发过程中，就要 求我们能够对实时系统的行为采用形式化的方法进行模拟，并且验证它是否满足 实际的需要。 针对该问题已经提出了很多理论和方法，其中模型验证以其简洁明了和自动 化程度高而引人注目。当时序逻辑扩展到可以用来处理时间约束时，模型验证成 为了一种重要的形式化验证方法，它的基本思想是用逻辑公式描述系统性质，用 状态转换系统模拟系统行为，这样“系统是否满足我们想要的性质 就转化为 “状态转换系统模型是否满足性质相对应的公式”这样的一个数学问题了。在系 统状态有限时，该问题是可判定的【3 1 。 形式化分析需要模型去模拟实时系统的行为，因此关键性的问题就是找到合 理的形式化方法去构造模型，有效的模型构造出来以后，我们才能对系统进行形 式化的分析。由r a l u r 等人提出的时间自动机是模拟和分析计算机科学领域中 许多问题的有力工具1 5 。引，特别是在实时系统的模型验证中占据着重要的地位。 时间自动机模拟系统行为从而验证系统是否满足其规范的问题可以转化为验证 基于时间自动机的模型验证技术 两个自动机所接受的语言是否相互包含的问题【4 】。这种先进行模型构造，然后再 规范验证的方法将给系统设计者提供一种全新的系统分析方式。 1 2 研究现状 为了描述实时系统中出现的时间约束，a i m 等人提出了时间自动机。近年来 使用时间自动机进行的模型验证迅速成为形式化验证研究的一个热点。事实上， 实时系统的可靠性如果采用时间自动机来验证的话，一般可以转化为下面的问 题：两个时间自动机接受的时间正则语言能否相互包含，也可以看作是两个时间 正则语言的交集是不是空的判定问题。我们可以看到，每年都会出现许多优秀的 相关论文研究涉及内容广泛，主要包括了时间自动机理论、如何改进验证算法 和验证工具等，还有以时间自动机为理论基础的验证工具广泛地应用在了生产过 程中。可以说利用时间自动机对实时系统进行的模型验证，在理论和实践方面都 得到了较大的发展。 通过采用r a l u r 等人提出的区域自动机构造算法，可以将时间自动机模型 转变为时间区域自动机，但是在构建区域自动机的过程中，状态个数可能随着时 钟个数的增加而呈现出指数级增长，同时状态个数的增长与时钟约束的常量大小 成正比；此外，用此方法得到的区域自动机模型可能会存在许多不可达的状态。 为了缓解状态空间爆炸问题，许多人都提出了对状态空间进行最小化的方法 9 - 1 s 】，这些方法明显使状态数目变少。例如，r a l u r 等人提出利用状态最小化算 法构建系统区域图来缩小系统规模【9 】，这种方法利用系统的规范说明可以直接构 造一个最小系统区域图，而不需要化简完全区域图。 验证由时间自动机构造出的系统模型是否满足预期的系统性质，可以先把这 些性质用时间逻辑公式表示出来，然后检测模型是否满足它们。验证算法从系统 的状态空间中搜索特定状态。总的来说有两种搜索技术：向前搜索和向后搜索。 前者遍历状态空间是采用从一个状态找该状态后继的方法；而后者则采用从一个 状态找该状态的前趋的方式。由于时间自动机的时钟变量取实数值，结果导致状 态数无限增多，使遍历空间变得困难。关键问题是如何使状态空间最小化，主要 有四种方法加以缓解： 1 ) 区域自动机把状态空间划分为若干区域等价类【5 j ，该方法主要依赖以下 2 基于时间自动机的模型验证技术 结论：可以把稠密的时钟值空间划分为有限类的集合；在区域等价类下 验证问题结论依然成立。a l u r 等人也给出了前向与后向验证算法【2 】。 2 ) 带自动机a l u r 在区域自动机基础上提出了带自动机 5 1 。时钟区域的合 并得到了带自动机，通过该方法减少了时间自动机模型的等待验证的状 态数目，验证模型的时间复杂度降低了【1 8 】。 3 ) 线性不等式表示时钟区域自动机中的区域集合，可以在不显式地构造时 钟区域的情况下，用符号操作不等式代替时钟区域的操作。h e n z i n g e r 使 用t c t l ( 时间计算树逻辑) 公式描述了期望时间性质【r 7 1 。 4 ) 时钟值空间的离散化。使得时间以这样的方式进行流逝：离散空间至少 包含任意时钟区域的一个典型值。g o l l u 等人给出了验证算法【1 6 1 。 验证过程中出现的状态空间爆炸是限制了基于时间自动机的模型验证技术 的发展，如何缓解该问题成为一个研究的热点。近年来，利用时间自动机对实时 系统进行验证有了一定的发展，出现了一些比较成熟的验证工具。 u p p a a l 是一个基于时间自动机的验证工具，它可以有效地对实时系统进行 建模、模拟和自动验证，从而确保在实际环境中实时系统的安全可靠。该工具的 优点是验证速度快和实用性强，这使得它不仅是学术界的一个验证工具，而且成 为模型验证世界中工具的典型代表。由时间自动机构造的模型可以包含多个整型 变量和时钟变量，它们之间的通信依赖于通道和全局整型变量。u p p a a l 己经成 功地应用到了许多有限状态实时系统 1 9 - 2 3 1 ，典型的应用领域包括网络协议验证 和嵌入控制器性能研究。 1 3 本文结构 本文的组织结构如下： 第一章介绍了研究背景、现状和意义。 第二章介绍了时间自动机的定义和时间语言的概念，还有时间自动机的一 些扩展。 第三章给出了基于时间自动机的模型验证方法，在验证过程中用到的符号 化语义和可达性分析，还有用到的算法和数据结构。 3 基于时间自动机的模型验证技术 第四章介绍了如何使用二元决策图表示整数语义下的时问自动机的状态 和转换关系，并且给出了在这种数据结构下的一种可达性分析的算法改进，然后 结合一个验证实例对该算法进行了复杂度分析。 第五章介绍了u p p a a l 工具的基本功能和使用该工具验证的方法，使用 u p p a a li 具所做的一个验证实例，对飞机着陆控制系统进行了模型构造和分析， 并得出有用的结论。 第六章结论和展望 4 基于时间自动机的模型验证技术 第二章时间自动机 直观上说，时间自动机就是标记有非负实数时钟约束条件和重置的状态转换 图【2 4 】。 2 i 时间自动机的定义 在计算机科学界自动机常用做计算机和计算过程的动态数学模型，用来研究 计算机的体系结构、程序设计、逻辑操作乃至计算复杂性理论。为了描述实时系 统的时间约束，a u r 等人提出了时间自动机，该理论在后人不断地研究中得到了 丰富和扩展。 2 1 1时间转换系统 时间转换系统是一个五元组( ，s ，s o ，c 功，其中量6 】： z 是有穷字母表 s 是有穷的状态表 晶s 是初始状态集 c 是时钟的集合，该集合的元素个数是有限的 e s m ( c ) 2 c s 是状态转换关系的集合。边( j ，口，万，a ，s ， 表 示当输入字符为口时从状态j 到状态j 7 的转换，集合名c 表示由转 换发生时被重置的时钟所组成的集合，艿是时钟集合c 上的一个时 钟约束，即艿c p ( c ) 。当万满足时，转换才能发生。 2 1 2 时间约束和时钟解释 为了能清楚地理解时间自动机状态转换是如何发生的，必须掌握时钟约束和 时钟解释的含义，因此我们首先给出它们的详细定义。 定义2 1 时钟约束【s ，6 】 5 基于时间自动机的模型验证技术 令x 是时钟变量的集合，则时钟约束万的集合m ( x ) 的定义如下： 艿：= x c l c 工1 1 万1 4a 喀 其中，工是x 中的一个时钟，c 是非负有理数集q 中的一个常量，从定义可 以看到，最简单的时钟约束形式就是时钟与时间常量之间的比较，另外还允许使 用布尔运算对这些简单时钟约束进行组合。 定义2 2 时钟解释【5 ，6 1 时钟集合c 上的一个时钟解释v 是指为每个时钟分配一个实数值，也可以说 它是从集合c 到非负实数集r 的一个映射。c 上的这个时钟解释 ，满足x 上的一 个时钟约束万，当且仅当依照时钟解释，给出的时钟值，时钟约束万的布尔值为 真。对于t r ，v + t 也是一个时钟解释，它指对时钟集合c 中的每个时钟变量x 都赋值为v ( 功+ f ；同样t 1 1 表示对时钟变量x 赋的值是f “x ) 。对于ys x ， 【】，h 咖表示c 上的一个时钟解释，其中时钟集合y 中的每一个时钟都赋值为f ， 而不包含在集合】，中的时钟的值仍赋为是吠功。 我们刚给出的时钟约束定义是最简单的，但是比较多的时钟变量会出现在大 部分的实际系统中，此时相互约束的情况可能出现不同时钟变量之间，即系统的 时钟约束出现了x y 一刀的形式，其中佟， ，芍，刀( 表示正整数 集) 。这种形式的时钟约束会在本章第三节做出详细介绍。 2 1 3 时间自动机的语法和语义 定义2 3 时间自动机 时间自动机彳，可以把它定义为六元组( ，s ，瓯，c ，i ，毋，其中【5 - 6 】： & 冬s 是一个起始位置集合 s 是一个位置集合，它的元素个数是有限的。 c 是一个有穷时钟集合 是一个有穷标号( 1 a b e l ) 集合 ，是一个映射，它为s 中的每一个位置s 指定( c ) 中的某一个时钟 6 基于时间自动机的模型验证技术 约束，可以把位置对应的时钟约束称为时间不变式。 e s x ( c ) x 2 c s 是一个状态转换关系的集合。( s ，口，万，元，s ， 表示 输入字符口时，从位置s 到s 的一个转换。万是定义在时钟集c 上的一 个时钟约束，可以把它称为时间守卫【2 5 1 ，只有在满足它的情况下，转 换才能发生。五表示在发生位置转移时被重置的所有时钟组成的集合， 且存在五c 。 从上面的定义我们可以看出时间自动机状态间的转换能否发生取决于两个 因素：一方面是输入字符口是否出现；另一方面是输入字符口出现时相应的时钟 约束是否得到满足。时间自动机处于某一位置时，也应该满足一定的时钟约束， 即应该满足位置上的不变式。时钟变量在实数集上取值，会使自动机在某一个状 态停留一段的时间，而又可以把该时间段离散的分解成无限多个时间值，因此在 给出时间自动机的语义之前，先将其状态扩展成形如 的表示方法，其中s 是时间自动机的一个位置，是在位置s 能够使时钟集合中每个时钟都满足j 的 一个时钟解释。 通过状态扩展我们可以得到相应的转换系统来定义时间自动机的语义，对于 时间自动机彳= ( ，s ，蜀，c , i ，毋，彳的转换系统共有两大类转换【5 6 l ： 状态可以因为时间流逝而改变( 延迟转换) ：( 葶，岭专( j ，v ) 当且仅当v 比 ，大，并且在，与v 之间的所有时间值能够满足在状态s 时的时钟约束； 状态可以因为位置转换而改变( 离散转换) ：( s ，哆型_ ( s ，) 当且仅 当口，五c ，在位置s 时时钟解释是1 ，在位置s 时时钟解释为， 并且在输入字符口时自动机的位置从s 转换到s ，此时集合名包含的时 钟被置零。 2 2 时间语言 通过对时间字的定义，应该使实时系统的一个行为能够与事件组成的字母表 中的时间字对应，而时间语言是时间字的集合。与密集时间模型一样，在这里时 7 基于时间自动机的模型验证技术 间域也是非负实数集r 。每个字万都有一个时间序列t 与之相匹配。 定义2 4 一个时间序列t = t t 。t 。是时间值t 。( t ；r ，并且_ r 。 o ) 组成 的无穷序列，需要满足以下两个条件【5 】： 1 单调性：时间序列t 是严格单调递增的，即对于所有的i 1 都有t t t 。 字母表上的一个时间字就是一个二元组( 万，t ) ，其中万是字母表上的 一个无限长字，t 是一个时间序列。字母表上的一个时间语言就是由上的一 些时间字组成的集合。 如果把一个时间字( 万，t ) 作为某个自动机的输入，则在时间为t 。时输入 符号万。如果用时间自动机构造出系统的模型，符号万。则表示系统发生的某个 事件，t 。则表示莎。事件发生的时间。在某些情况下，可能允许事件序列中的多 个并发事件对应相同的时间值，此时可以对时问字的定义稍作修改，即只要求时 间序列是单调上升的( 即对于所有i 1 ，要求t 。t 。+ ) ，不要求严格单调。对 于这种模型，所有结论同样成立。 下面来看看时间语言的一个例子。 例2 1 字母表= a ，b ) ，时间语言厶由满足条件时间5 6 之后不再有b 出 现的所有时间字( 莎，t ) 组成，即 上l = ( r ) l 蛾( h 5 6 ) _ ( 们= 口) ) ) 时间语言厶由所有满足条件a 、b 交替出现且a 、b 之间的时间间隔逐渐增 大的时间字组成，即 如= ( 口6 ) u ，r ) | ( ( 匏一他一1 ) e 图2 - 1 对角约束被一步步移出 9 基于时间自动机的模型验证技术 可达性问题的可判定性在最初的论文中已经得到了证明，它依赖于等价区域 的构造，但是复杂度并没有改变。下面我们来看它是如何增加模型的表达能力的， 通过一步步得移出对角约束，构造出一个不含有对角线约束的等价时间自动机。 在图2 1 展示了如何把对角约束移出( 图中，我们移除了x y c 这个约束，c 是 个非负的整数) 。这种方法的主要思想是在时间流逝的时候对角约束x - y c 的真 值保持不变，只有在时钟x 或者y 被重置为0 时才能发生改变。 2 3 2 叠加时钟约束 这种类型的约束也能够添加到时间自动机的模型中，它的形式是x + y c ，在 这里x 和y 是时钟变量，是一个比较操作符，c 是一个正整数。有了这种扩展 的时间自动机可以识别经典自动机不能识别的语言。图2 2 中的自动机可以识别 这样的一个时间语言：动作a 可以在1 2 ，3 4 ，7 8 ，1 5 1 6 等时间点发生。采用 了这种扩展的时间自动机可以满足以下属性【2 8 1 ： 1 ) 用两个时钟来限制自动机时，在该扩展模型中可达性的检查是可判定的。 2 ) 用四个或者更多时钟来限制自动机时，在该扩展模型中可达性的检查是不 可判定的。 二+ = 秘靠，l t n ) ln 芝1n n d t i - m1 一专 嚣+ 馨= l ，口，2 ：享0 图2 2 一种不能被任何经典时间自动机识别的时间语言 不多于两个时钟的模型的判定性依赖于等价区域的构造，区域集是经典区域集 的完善，如图2 3 所示。对于四个或者更多时钟的情况，模型变得不可判定的了。 对于三个时钟的情况，可达性问题的能否判定变得未知了。 1 0 基于时间自动机的模型验证技术 图2 3 含有两个时钟和叠加时钟约束的时间自动的区域等价 2 3 3 内部动作 我们知道，在有限自动机中内部动作( 也被称做转换) 是可以被清除的 【2 9 】，因为它不会增加有限自动机的表达能力。我们惊讶地看到这种时间自动机 的框架是不同的：尽管内部动作对可达性问题的判定没有做出任何改变，但它增 添了模型的表达能力。图2 4 中描述的自动机可以识别经典时间自动机不能识别 的一种时间语言，这种语言是关于单个字母a 的时间字的集合：每两个时间单元， 标记有a 的转换发生，或者标记有的转换发生。 露= 2 口 卫：= 0 霉= 2 霉：= 0 图2 4 一种不能被任何经典时间自动机识别的时间语言 2 3 4 时钟的更新 在最初的模型中，除了时间流逝以外只有一种操作可以修改时钟的值，它就 是把时钟重置为零。因此，我们自然会考虑在时钟上采用更加复杂的操作。在这 里，更新操作的主要形式是x ：一c 或者x ：一y + c ，在这里x 和y 是时钟变量，一是一 个比较操作符，c 是一个常量。举例来说，更新x ：c 意味着我们给时钟变量x 赋了一个小于或等与c 的不确定值。我们把使用了这种更新方式的时间自动机叫 做可更新时间自动机，这些更新的复杂导致了一般模型的不可判定性，然而一些 子类已经被证明是可判定的。可达性问题主要有： 1 ) 有x ：= c 这种形式的更新的时间自动机是可判定的。 1 1 基于时间自动机的模型验证技术 的。 的。 2 ) 有自增( x ：= x + 1 ) 这种形式的更新但没对角线约束的时间自动机是可判定 3 ) 有自增( x ：= x + 1 ) 这种形式的更新和对角线约束的时间自动机是不可判定 4 ) 有自减( x ：x - 1 ) 这种形式的更新的时间自动机是不可判定的。 再一次的证明，是否满足可判定性是通过构造区域自动机来得出的。对于含 有自减这种更新方式的时间自动机，可达性问题是不可判定的。我们注意到已被 证明是可判定的更新时间自动机能够转换成为等价的含有内部动作的经典时间 自动机。另一方面，这些可更新时间自动机比经典时间自动机更加简练啪3 。采 用这些时钟更新的方式对实时系统的建模是非常有用的。 2 4 本章小结 我们首先给出了时间转换系统，在此基础上介绍了时间自动机的定义。想要 深入理解时间自动机的语义，必须掌握时间约束和时间解释这两个概念。时间自 动机是一类模型验证的理论基础，为了能够在模型构造过程让其更好地描述实际 系统，本章也介绍了它的一些扩展。根据实际需要可以提出一些新的包含更丰富 信息的时间自动机模型，这也就促进了该理论的完善与发展。 1 2 第三章基于时间自动机模型的验证方法 时间自动机是包含时间约束的有限状态转换系统，利用它对实时系统构造出 模型后，要判断系统是否安全，就得检验某些不安全状态是否可达，因此基于时 间自动机的验证技术主要研究状态可达性问题。由于语义描述的时间自动机的状 态是无穷的，因此判定状态是否可达存在着不少的困难。 3 1 模型验证方法 自从提出了时间自动机的概念，便有了一种简单而有效的方法去描述带有时 间因素的系统状态转换，为实时系统的行为模拟和性能分析提供了形式化方法， 在实时系统模型验证中占据重要地位。 3 1 1 模型验证的概念 式化 图3 1 模型验证过程 模型验证是对有限状态系统的一种形式化确认方法。已知一个有穷状态系统 和表示系统规范的某种时序逻辑公式，我们要做的是找到一种方法判定给定系统 是否满足这些时序逻辑公式。如图3 1 所示，模型验证方法的输入包括二部分， 1 3 基于时间自动机的模型验证技术 分别是待验证的系统模型和待验证的性质描述，如果该系统模型满足了所有的性 质，则算法输出 t r u e ：否则给出反例，并且说明不满足的原因。 构造系统模型、描述需满足的规范和选择验证算法是模型验证技术的三个主 要步骤。模型验证算法最初是由e m c l a r k e 、q u e i l l e 、e a e m e r - s o n 、s i f a k i s 等 人在2 0 世纪5 0 年代初期提出，分支时序逻辑c t l 被来描述系统的性质，又称 为c t l 模型检测：不久又出现了线性时序逻辑l t l 模型检测。多数情况下，c t l 模型验证算法的时间复杂度是线性或者多项式的，然而l t l 模型检测算法的时 间复杂度为p s p a c e 完全的。 模型验证的主要思想是进行状态搜索，搜索过程应该是可以结束的，这就要 求系统模型状态的个数是有穷的，因此不能直接对无穷状态系统进行验证。对于 一般系统而言，需要首先经过一个从无穷状态到有限状态的转换过程，对系统进 行模型构造就起到了这样的作用。 3 1 2 时间自动机建模 时间自动机的出现为实时系统的模型验证提供了理论基础。时间自动机在思 想上可以说是稠密时间模型和自动机的有机结合，可以用它对包含时间约束 的实时系统进行建模，建模过程中需要用有限多个时钟来描述带有时间约束的状 态转换。一般而言，用时间自动机对实时系统建模由以下几个步骤组成： 1 ) 首先需要进行系统分析来确定系统要由哪几个子系统来组成，然后才能 分别对每一个子系统使用时间自动机来构造模型； 2 ) 考虑每个子系统在运行的过程中可能到达的一些状态，在不考虑时间的 条件下，将系统可能的状态划分为几个位置，尽量使每个位置都代表一 定的含义，能够在状态转换中起着关键性的作用，位置的个数要尽可能 的少； 3 ) 考虑每个时间自动机的位置上可能允许的时间长度，即确定时间自动机 位置中的不变式，不变式包含的常量的选择很重要，系统出现死锁时， 多数是由不变式的设计不当造成的。在这一步可能要对上一步中确定的 位置进行修改； 4 ) 考虑各个时间自动机的转换关系，即根据每个子系统的时间行为规律， 1 4 基于时间自动机的模型验证技术 确定时间自动机哪些位置间可能发生转换以及该转换的时间卫式，还要 清楚哪些时钟变量需要进行重置； 5 ) 考虑各个子系统间的通讯，时间自动机间提供了相互同步通讯的方法， 同步转换边上的事件( 或者叫做标记) 所对应的字符应该是一样的，此时 需要我们考虑整体系统，经常需要返回到前面去修改系统，使其能够真 实地反映时间系统的行为。 模型构造过程是一个由简单到复杂的过程，先把条件限制最少的模型构造出 来，再逐步将其完善，如果添加条件的过程中出错了，很容易发现出错的原因。 3 2 符号化语义和验证 由于时钟变量是在实数集上取值，所以我们描述的时间自动机的转换系统是 有无穷多个状态的，然而不能够对一个无限的转换系统直接进行自动化验证。 a l u r 等人的文章里提供了一种能够使时间自动机的无限模型转换为有限模型的 方法，他们具体是采用区域等价的方法来实现这一目的的，在本节我们首先具体 介绍这一方法涉及到重要概念，然后介绍了时钟带的概念，它是在区域自动机的 基础上做出的重大改进。这些方法和理论都是可达性分析的基础，使成功遍历系 统所有状态成为现实，这样就使得基于时间自动机的模型验证技术真正具有了可 行性。 3 2 1 时钟区域 为了判定时间自动机的可达性，需要对时间自动机的的行为进行抽象，当检 测从初始位置是否能到达另外某一个位置时，它等价于检测在有限自动机中某个 状态( 或者是一些状态的集合) 是否是可达的。为了达到这个目的，在时间自动 机状态集合上定义了一种等价关系，从两个等价的状态发出的行为有可能是相同 的。 定义3 1 区域等价关系旧 对于时钟集合c 中的一个时钟变量x ，用t x 表示时钟x 的上界值。对于实数 m ，用 m ) 表示m 的小数部分，m 的整数部分用 m 】表示。两个时钟赋值u 和v 1 5 基于时间自动机的模型验证技术 是区域等价的，即u v ，当且仅当下列所有条件得到满足： 1 、对于时钟集合中的任意时钟变量x ，要么阻( 曲】= 【“曲】，要么u ( x ) 和v ( x ) 都比t x 的值要大。 2 、对于时钟集合中的任意时钟变量x 和y ，如果u ( x ) t x 同时u ( y ) r y ， 则： ( 1 ) 伽( 力) = 0 当且仅当p ( 工) ) = 0 ( 2 ) 伽( 功) 缸( y ) ) 当且仅当p ( x ) ) y ( y ) ) 在一个时间自动机中，经常存在这样的等价关系，我们可以认为一个时钟区 域就是万维实数空间r n 中的一个极大子集，组成这个区域的所有点都满足同一 个时钟约束。每一个时钟约束在栉维实数空间中也对应着一个时钟区域，这些时 钟区域构成了关于空间r n 上的一个划分，在该空间中的时钟区域的数量是有限 的是因为形成的这些划分是有限的，这样就将无穷状态空间划分为有穷个等价 类。 通过上面的定义，我们可以知道时间自动机中的时钟区域是在上述等价关系 下关于时钟解释的等价类，它可以帮助我们从理论上证明了时间自动机的可达性 问题是可判定的。但有一种情况不得不引起我们的注意，就是在多数情况下，一 个状态或者一个转换发生时，多个时钟约束都要被要满足的，也就是说要满足多 个时钟约束组成的集合，在这种情况下，如果仍使用时钟区域对时间进行等价划 分的话，就会出现许多的问题，比如时间自动机状态的数目会出现膨胀的趋势， 区域的数目过多使得验证变得困难，还有可能使状态的表示工作变得非常复杂。 为了解决这个问题，在时钟区域的基础上改进得到了时钟带的概念。 3 2 2时钟带 时间自动机的状态集合是无限大的，为了验证这样的模型，不得不在这样大 的一个集合上进行一些操作，因此采用高效的符号化方法来表示这些状态的集 合。最常见的就是利用时钟带来表示。 从时钟约束集中的任意挑选出一个子集，该子集中的每一个时钟约束都对应 着一个时钟区域，那么子集中所有时钟约束对应的时钟区域的并集将构成一个凸 1 6 基于时间自动机的模型验证技术 并集，我们把这样的一个凸并集叫做时钟带( c l o c kz o n e ) 。时钟带可以看作时间约 束的交集，比时钟区域粗糙，一个带可能是由多个区域的并得到的。 经过上面的分析，我们可以得出这样的一个结论：时钟带同样是时钟解释的 集合，可以通过时钟约束的并集来描述它。时钟带可以由下面给出的语法形式进 行描述：伊? = 工 ci 石clc 工ic 工ix - y ci 仍人仍，其中x 和y 表示时间自 动机的时钟集合内的任意时钟。时钟带具有下面的一些性质： 1 ) 任意的时钟区域都可以做为一个时钟带 2 ) 一个时钟区域0 【和一个时钟带p ，a 要么完全包含在p 中，要么和叩不相交 3 ) 两个时钟带的并集仍然是一个时钟带 4 ) 两个时钟带的交集仍然是一个时钟带。 时钟带作为时钟解释的等价类，它不仅可以用来处理简单的时钟约束问题， 如果时间自动机存在多时钟间的相互约束，也可以处理这类较复杂的问题。在这 种情况下便