（计算机软件与理论专业论文）基于时间自动机模型验证方法优化研究.pdf

基予对闯矗囊瓿挨燮验证方法 惹让磷究 摘要 实时系统楚一种带有时简约束的计算系统，这些系统的许多动作的完成是与 时间相关的，即要满足一定的时间限制。为了确保实时系统的正确性和可靠性， 黪要对其进行严格靛分辑零l 验涯。实对系统豹验证不仅簧求逻辑上怒正确豹，嚣 。照要求时间上也是正确的。现在网络协议的复杂性舀盏增加。协议中的每一处链 误和缺陷都将给网络系统的稳定性、可靠性等带来巨大的危害。执议的验证中往 缝也嚣要验涯一些时霹蛙矮。 对实时系统和协议通常采用形式化的方法来进行验证。有限自动桃是最为重 要的一种形式描述与验证技术，它是很多形式化方法的基础。它直观性强，可安 魂与冀宅形式纯方法豹缀会耪转换。毽楚莛l 子其投毒港楚熬靖溺豹搬念，冀糍处 理事件的序列，而一i 能准确地描述事件发生的时间，因此在模型验诞上的应用受 蒯很大的限制。为解决这个问题，r a l l l r 等人提出了时间自动机模型。时间自动 秘在有穷垂动援熬墓丢窭土热入了薅铮交爨，逮过薅镑变豢巍霹镑壤豹跪较来约紊 状态的转移，因此时间自动机可以准确地描述带有时间的系统。 时间自动机的状态空间的大小随着问题规模的增大呈指数级递增。当系统规 貘较大跨，鏊予簿藕垂囊瓠弱验证裁会变缚龚翥复杂。瑟竣霉要对孵润窭动瓿豹 模型验证方法进行优化。 本文主要研究了域自动机方法、带自动机方法以及基于历史等价和转换互模 缀戆最枣毯方法。文中对露镑壤及其上熬操孬绘高了簿麓号纯豹裘示方法，从 而便于域自动机在实际操作中的实现。本文还提出了耩于状态转移时间关系的优 他方法。该方法通过计算状态转移的最早可能发生时间和最晚可能发生时间来判 凝转移是套是鸯效熬，逶适搽黎有效转移寒筵 乏转换系统。 基于时间自动机已经开发出了多种自动验证工具。这些工具已经在实时系统 和协议验证中得到了广泛成用。本文使用 n o s 验诫了f d d i 协议来说明了熬 予嚣重阗垂动橇戆验证过巷。 关键词；时间自动机，实时系统，网络协议，模型验证，协议验证 基于时间自动机模型验证方法优化研究 a b s t r a c t r e a l t i m es y s t e m si sak i n do fs y s t e m sw i t ht i m ec o n s 打a i n t t h ea c t i o ni sc o 衄e c t c d w i ms o m et i m ec o n s 廿；l i n t c o r f e c t l l e s sa n ds e c u r i t ya f ei m p o r t a n t t ot h e s es y s t e m s ，s o a n a l y s i sa 1 1 dv a l i d a t i o na r en e e d e d t h ev a h d a t i o no f r e a l _ t i m es y s t e l n si l o to n l yn e e d s t h el o g i ci sc o r r e c t ，b u ta l s ot h et i m ei sc o r r e c t t h ep r o t o c o lc o m p l e x i t yi si n c r e a s i n g r a p i d ly ，e v e r yf a u l ti sh a 瑚m lt om es t a b i l i t ya n dt h er e l i a b i l i t y t h ev a l i d a t i o no f p m t o c o l sa l s on e e d st ov a l i d a t es o m ep r o p e r t yo f t i m e f i n i t ea u t o m a t ai sa ni m p o n a n tt e c h n i q u eo ff o r m a l i z e dd e s c r i p t i o na n dv a l i d a t i o n ni st h ef o u n d a t i o no fm a n yf o 瑚a l i z e dt e c h n i q u e s nc a nb ea s s e m b l e dw i t ho t h e r t e c h n i q u e s b u ti td o e s n th a v ec l e a rc o n c e p to ft i m e s oi tc a no n l yd e a lw i t ht h e s e q u e n c eo fe v e n t sa 1 1 dc a n td e s c r i b e 血et i m ec l e a d y r a l u rh a sp u tat h e o r yo f t i m e da u t o m a t a t i m e da u t o m a t ai n c l u d e dt i m ev a f i a b l e si n t o6 n i t ea u t o m a t a t h e s t a t e s p a c eo f t i m e da u t o m a t ag m w se x p o n e n t i a l l yw i t ht h es c a l eo fq u e s t i o n s t h ev a l i d a t i o no fs y s t e m sb a s e do nt i m e da u t o m a tb e c o m e sv e r yc o m p l e xw h e nt h e s c a l eo fq u e s t i o n si s1 a 喀e s ot h eo p t i m i z a t i o no ft h et e c h n i q u eo fm o d e lc h e c k i n g b a s e do nt j m e da u t o m a t ai sn e e d e d i nt h i sp a p e r ，w er e s e a r c hr e g i o na u t o m a t a ，z o n ea u t o m a t aa 1 1 dt h em e t h o do fs t a t e s p a c em i n i m j z a t i o nb a s e do nh i s t o r ye q u i v a l e n c ea n db i s i m u l a t i o n 仃彻s i t i o n w e d e v e l o pas y m b o l i cm e t h o do ft i l ep r e s e n t a t i o na dc o m p u t a t i o no fr c g i o n s s oi ti s e a s i e rt ou s et h er c g i o n s w ed e v e l o pam e t h o db a s e do n 血et i m er e l a t i o no f 的n s j t i o n s t h i sm e t h o dc o m p u t e s 恤ee a d i e s tt i m ea n dt l l el a s tt i m eo ft r a l l s i t i o n st o d e c i d et h e 仃a n s i t i o n sa r ev a l i do rn o t t h e nt h em i n i m i z e dt r a n s i t i o ns y s t e m sc a nb e g e tm r o u g hg e t t i n gr i do f t h et r a n s i t i o n sw h i c ha r ei n v a l i d a1 0 to fa u t o m a t i ct o o l sh a v eb e e nd e v e l o p e do nt i m e da u t o m a t a t h e s et 0 0 l sh a v e b e e nu s ew i d e l yd l l r i n gt h ev a l i d a t i o no fr e a l t i m es y s t e m sa n dp r o t o c o l s i nt h j s p a p e r ，w ec h e c k t h ef d d i p r o t o c 0 1u s i n gk m n o s k e yw o r d s ：t i m e da u t o m a t a ，r e a l - 石m es y s t e m s ，n e t 、v o r kp r o t o c o l ，m o d e lc h e c k i n g ， p r o t o c o lv e r i f i c a t i o n i i 郑重声明 y 9 7 7 0 本人的学位论文是在导师指导下独立撰写并完成的，学位论文没有剽窃、抄 袭等违反学术道德、学术规范的侵权行为，否则，本人愿意承担由此产生的一切 法律责任和法律后果，特此郑重声明。 学位论文作者( 签名) ：高冠右 2 占年6 月z 日 基于时间自动机模型验自f 方法优化研究 1 1 研究背景 第一章前言 实时系统【1 1 是一类重要的计算机系统，它能够对来自所拧制的外部环境的交 互作用做出及时响应以达到预定目的。实时系统涉及到许多工业应用领域，如： 工业过程控制系统、航天航空系统、军事防御系统、交通控制系统、嵌入式系统 等。这类系统的正确性很重要，出现的任何一个错误都会带来重大的经济损失、 环境破坏，甚至威胁到生命安全。与其他系统不同，这些系统需要满足一定的时 间约束，如执行时间、应答时间、延迟时间等等。因此实时系统【2 ，3 j 不仅要求所 产生的结果在逻辑上是正确的，而且要求在时间上也是正确的。也就是说它们的 正确性不仅依赖于劳发成分如何相互作用，还依赖于这些交互作用发生的时间。 然而要保证所实现的系统能够满足所有的时间属性是一项复杂的工程。 现在越来越重视借用严格的数学工具来描述系统并对系统进行验证来保证 系统的正确性和提高系统的可靠性。在这样的背景下，形式化的模型验证方法得 到了广泛的接受和应用。模型验证其基本原理实现为系统建立形式化模型，阐明 所要验证的性质，然后用算法去检测该模型是否满足所述性质。常用的方法有过 程代数、p e t r i 网、时间自动机等。时间自动机p 】是r a l 提出的一种能够有效 描述实时系统的形式化计算模型。通常情况下，我们用一组时间自动机模型表示 一个实时系统的各个组成成分，用一个确定的时间自动机来模拟系统的规范说 明。然后构造表示各组成部分的时间自动机的积自动机，如果积自动机识别的语 言包含在表示系统规范说明的自动机所识别的语言之中，那么就表示实时系统满 足该规范说明，否则就不满足。也可以通过判断这两个时间自动机所识别语言的 交集是否为空来判断系统的规范说明是否被满足。 时间自动机不仅适合于实时系统的验证【4 5 ，6 j ，也适合协议的验证。使用时间 自动机验证协议不仅可以对己设计的协议进行分析和验证，找出其中潜在的错 误，还可以在协议开发的前期最大限度地检测和纠正协议错误和缺陷，例如死锁、 活锁、不可执行的行动、协议外部性能不符合服务要求等。 基于时间自动机模型验证方法优化研究 1 2 研究现状 时间自动机的性质己经得到比较充分的研究9 1 1 0 】。时间自动机模型也被进 一步扩展，提出了概率时间自动机，时间i ，0 自动机，线性代价时间自动机， 时间树自动机1 3 1 等新的模型。最主要的研究方向还是基于时间自动机的模型验 证。基于时间自动机已经开发出了多种自动验证工具，如u p p a a l ，k r o n o s ，c o s p a l l 等。 由于时钟集合中的时钟可以取值为任意正实数，时间自动机的状态空间的大 小随着过程数目的增加而呈指数级增加，因此在实践中，对规模较大的系统采用 时间自动机所产生的状态空间个数巨大，由于系统本身结构的复杂性，因此小可 避免地产生了状态空间的爆炸问题。所以要对时间自动机的验证过程进行优化。 在对时间自动机验证时，经常需要考虑某个状态是不是从起始状态可以到达的， 通常的方法是在时钟值上找到一个等价关系一，使得两个状态( ，v ) 和( f ，v ) 只要 满足( ，v ) ；( ，v ) 就可得出l 是可达的当且l 是可达的，而且= 所得出的等价类 的数目是有限的。通过这样的等价关系就可以把具有相同可达性的状态合并以减 小时间自动机的状态空间。关键的问题是如何找出这样的等价关系和如何表示这 样的等价类。常用的这样的等价关系有域等价关系等。 1 3 研究内容 本文研究了基于时间自动机的验证优化方法。对时间自动机的验证优化方法 主要有域自动机，带自动机，最小化算法 “之2 1 等。域自动机通过域等价关系把时 间自动机状态空间划分成域，满足域等价关系的状态被合并，从而减少了状态空 问。但是域自动机的转换图中很多顶点还可以合并，其状态空间并卅i 是最小的。 和域自动机相比，带自动机有较少的可达状态，但是带的个数是域个数的指数倍。 最小化算法有很多种，本文研究了基于历史等价关系和转换互模拟关系来合并状 态的方法。 本文对时钟域及其上的操作给出了一种符号化的表示方法，从而便于域自动 机在实际操作中的实现。本文还提出了基于状态转移时间关系的优化方法。该方 基于时间自动机模型验证方法优化耐f 究 法通过计算状态转移的最早可能发生时问和最晚可能发生时间来判断转移是否 是有效的。若转移的最早可能发生时间不大于最晚可能发生时间，那么可以认为 该转移的时间约束可满足，即该转移是有效的。若从初始转移开始一直到进入该 转移的一个转移序列中的所有转移的时间约束都是可满足的，那么这个转移就是 从初始转移可达的。通过保留有效转移，去掉无效转移可以得到简化的转换系统。 在进行分析前还可以去除时间自动机的转换图中的无效循环来简化分析过程。现 在基于时间自动机的验证已经得到了比较广泛的应用。本文用k m n o s 验证了 f d d i 协议来说明了基于时间自动机的验证过程。 1 4 本文结构 本文是如下组织的： 第一章前言，介绍研究背景、现状和本文的主要研究内容和意义。 第二章介绍时间自动机的基本概念，给出了时间自动机的形式化定义。 第三章介绍时间自动机验证过程。 第四章研究了时间自动机验证优化方法，基于时间自动机验证优化方法主 要有域自动机、带自动机、最小化方法等，本文给出了域及其操作的符号化表示 方法，提出了基于状态转移时间关系的优化方法。该方法通过计算状态转移的最 早可能发生时间和最晚可能发生时间来判断转移是否是有效的，通过保留有效转 移来简化转换系统。 第五章本文用心o n o s 验证了f d d i 协议来说明了基于时间自动机的验证过 程。 第六章对本文进行总结，展望未来的工作。 基于时间自动机模型验证方法优化研究 2 1 时间自动机简介 第二章时间自动机 传统的自动机能够处理事件的序列，但是它们没有清楚的时间的概念，因而 在实时系统等的验证上的应用受到很大的限制。但是时间自动机可以准确地描述 带有时间的系统。 例如图2 1 ( a ) 中的自动机表示了一个灯控开关的控制过程，这个灯有三个状 态：关( o 回、微亮( 1 i g h t ) 、亮( b r i 曲t ) 。这三个状态通过按下灯上的按钮来进行转 换( p r e s s ) 。初始时灯处于关闭状态，按下按钮可以使灯变为微亮状态。当灯处于微 亮状态时，既可以继续按下按钮使灯变为亮状态，也可以过一会再按下按钮使灯 回到关状态。传统的自动机无法描述带有时间的性质，因此无法区别上面的两个 行为。我们可以引入一个代表时间的变量x 。当灯在初始状态时按下按钮，x 被 初始化为o ( x ：= o ) 并且x 随着时间的流逝而增加。当用户紧接着按下按钮时 ( x c = 3 ) ，灯由微亮状态变为亮状态。若用户没有紧接着按下按钮时，表示用户想 使灯处于微亮状态。过一段时间( x 3 ) ，用户再次按下按钮，把灯关闭。 d r e s s a p r e s s p r e s s 4 基于时间自动机模型验证方法优化研究 b 图2 1 由此可见时间自动机增加了对带有时间的实时系统的描述能力。大多数描述 时间的系统分为离散时间模型2 4 和稠密时间模型。离散时间模型中时钟是一 个递增的自然数序列，事件只能在整数时间发生，时钟计时是通过一个一个的时 钟嘀嗒来进行。稠密时间模型中时钟值可以是任意的非负实数，事件可以在任意 时刻发生，从而可以更加真实地模拟实时系统。本文中采用的是稠密时间模型。 2 1 1 转换系统 我们使用标有事件标记的状态转换图对系统进行建模。 一个转换系统s 是一个四元组 ，其中： q 是一个状态集合， q o q 是初始状态集合， 是一个标记( 或事件) 集合， 叶q q 是一个转换集合。 系统从一个衲始状态开始。对_ 中的一个转换 ，我们记为 g _ 目。如果有口与g ，那么系统在事件n 发生时从状态g 转移到g 。如 果对某个标记口有g 兰_ g ，那么记之为g _ g 。状态9 是从状态q 可达的，那 么记为g 寸，g 。转换系统中的可达状态是从初始状态可以到达的状态的集合。 一个复杂系统可以被描述为多个相互作用的转换系统的积。设 置= 和s ：= 是两个转换系统。那么，在墨和s ： 的积中，一个状态是一个对偶( q ，g ，) ，且q q i ，g q 2 ，积的转换标记为。u ，中的标记。对一个标记口，为得到积的个标记为a 的转换，需要每个成员系 统执行一个标记为a 转换。形式上，这个积表示为s f fs ：，是一个转换系统 ，其中( 吼，可2 ) 与( “，“) 当且仅当 基于时问自动机模型验证方法优化研究 ln 2 且g l 旦_ _ i g ：，9 2 旦。- 2 9 ：，或者 i 2 且g i 旦 i g ；，g ；= 9 2 ，或者 口2 1 日口2 与2 q ；，g 仁目l 。 其中，：表示集合z 。与：的差集。 可以看出同时属于两个自动机字母表的标记被用作同步。在这个定义中，同 步是封闭的，即对一个共同的标记n ，一个成员( 转换系统) 可以执行一个标记为 n 的转换，当且仅当另一个成员也可以执行这样一个转换。 2 1 2 有时间约束的转换系统 为了表示有时间约束的系统行为，可以用一个实数值时钟的有穷集来扩大有 穷图。图的顶点称为位置( 1 0 c a t i o n s ) ，边称为转移( s w i t c h e s ) 。转移是瞬时的，但 时问可以在一个位置流逝。时钟可以随任何转移同时复位。在任一瞬间，时钟值 为从上一次复位到现在所已经流逝的时间。给每一个转移联合一个时钟约束，且 要求转移可以发生当且仅当时钟的当前值满足约束。对每一个位置，给它增加一 个时钟约束，称为它的不变式( i n v a r i a m ) ，且要求只有在= ，f 、变式为真时，时间才 可以在这个位置上流逝。存给出时间自动机的形式化定义前，让我们先看以下几 个例子。 图2 2 时间自动机的一个例于 考虑图2 2 所示的时间自动机。初始位置为s ，有一个单一一时钟x 。初始位 置没有1 i 变式约束，这意味着系统可以在位置s 停留任意时间。当系统在标记a 发生时转移到位置s ，同时时钟x 复位。在位置s 时，时钟x 的值记录从上一个 转换发生到即时的时间，从位置s 到s 的转移能够发生当且仅当这个值大于1 。 位置s 的不变式x 2 说明系统在s 最多可以停留2 时间个单位，一个转移必须 在不变式变为不满足前发生。那么这个自动机表示的时间约束是在d 和接下来的 基于时间自动机模型验证方法优化研究 6 之间的时间延迟总存1 和2 之间。 图2 3 有两个时钟的时i 司自动机 当有多个时钟时允许多个并发的延迟，如图2 3 所示。每次在标记n 下系统 从s 。到s 转移时，时钟x 复位。位置s 。和s ：的不变式c 水1 ) 保证从s ：到s ，的标记 为c 的转移存先前的n 发生后的一个时间单位内发生。存从_ 到s ：的标记为6 的 转移发生时另一个独立的时钟y 复位，在从岛到s 。的标记为d 的转移发生时检查 时钟，的值，确保在6 和接下来的d 之间的时间延迟总是大于2 。屯没有不变式 约束，事件d 可以无限延迟，也可以不发生。 2 1 3 时间语言 我们用字符来表示事件，所有事件的集合即为一个字符集。这个字符集上的 一个字称为时间字。每个时间字都对应于实时系统的一个动作行为。 定义2 1 时间序列f = q 2 t 是时间僮t 的无穷序列，其中t 尺且 t 0 ，满足下列条件： 1 单调性：f 是单调递增的，即对所有f 1 ，t f 。 有限字符集三上的时问字是一个对偶( 正) ，盯= q 哑是字符集z 上的无限 字，而f 是时间序列。上的时间语言是上时间字的集合。 如果时间字( 盯，f ) 被看作自动机的一个输入，那么它表示在f 时刻输入字符 盯。如果每个旺表示系统发生的一个事件，则相应的t 就可以理解成事件旺发 生的时间。存某些特定情况下，时间字序列中许多连续发生的事件可能有相同的 基于时间白动机模型验证方法优化研究 时间值。考虑到这种可能性，我们对时问字的形式化定义作一些改动，即不要求 时间序列中的时间值是严格单调递增的，而只要求时间序列是单调递增的( 对所 有f 1 ，有t 互+ 1 ) 。 我们考虑如下一个有关时间语言的例子。 例令有限字符集为扣，6 ，定义时间语言厶为满足以下条件的所有时间字 ( 仉f ) 组成的集合：在时间5 6 后1 i 会有b 出现。那么时间语言厶就可以表示成 如下形式： ，= ( 盯，f ) 1 v f ( ( 0 5 6 ) h = 口) ) ) 我们定义操作u n t i m e 来去掉符号所对应的时间值 定义2 2 对上的时问语言l ，对某个时间序列f 有( 以f ) l ，u n t i m e ( l ) 是包含仃m 的甜语言。 2 1 4 时钟约束和时钟解释 为了形式化地定义时间自动机，我们需要说明状态转移过程中对时钟有什么 样的约束。时钟是一个非负实数集上的变量。所有的时钟都以统一的速度流逝。 在开始时时钟一般都置为0 ，而日随着事件的发生，时钟可以被重置为o 。时钟 约束的最简单形式是将一个时钟值和一个时间常量进行比较，而且时钟约束只能 是上述原子形式的时钟约束的布尔结合。下面是其形式化定义。 定义2 3 时钟约束 时钟约束d 的集合巾扛) 递归定义如下： 万：= c i c x i _ 1 占1 4 谚 其中，x 是一个时钟变量集，x 是x 中的一个时钟变量，c 是有理数集q 中的一 个常量。形式为z y m 的约束条件称为对角线约束，为了保证时间自动机的可 判定性，通常不允许对角线约束出现。 时钟变量集x 上的一个时钟解释v 是指为每个时钟变量赋予一个实数值，可 以表示为从z 到非负实数集矿的一个映射。如果在v 所给定的时钟赋值下时钟约 束占的布尔值为真，我们就称时钟解释v 满足x 上的一个时钟约束万。 r 基于时间自动机模型验证方法优化研究 对于f r ，v + f 是一个时钟解释，它表示对时钟变量集x 中的每一个时钟 变量x 都赋值为v ( x ) + f ；f v 表示对时钟变量x 的赋值为fv ( x ) 。对于y x ， r 卜f 】v 表示对任意的x y 赋值为f ，而剩下的时钟变量满足v 。 2 1 5 时间自动机的语法和语义 定义2 4 一个时间自动机一是一个六元组( 工，三。，并，e ) ，其中： 三是有限的位置集合， 如是一个起始位置集合，且厶上 是一个有限字符集合， z 是一个有限时钟集合， ，把三中的每个位置j 映射到m 伍) 中的某个时钟约束， e 互上2 。m 伍) 工是转移的集合。 转移( s ，口，仍丑，j ) 表示输入字符口时从位置s 到位置j 的一个转移。五x 表 示发生状态转移时所有要被重置的时钟变量的集合。妒是定义在时钟集盖上的一 个时钟约束，在位置转移发生时必须被满足。转移是瞬时发生的，而时钟可以在 位置上有一段延迟。边e 上的时间约束如果满足的话允许转移发生，位置上的 时间约束如果不满足的话将强迫转移发生。 如果给定一个时间字( 盯，f ) ，时间自动机4 在零时刻将从它的起始位置集合 中的一个位置开始，这时所有的时钟值均被初始化为0 。随着时间的流逝，所有 时钟值都不断发生改变。，如果在时刻t 输入字符q ，并日当前的时钟值时钟约 束万，就会发生从状态j 到j 的形如( j ，日，仍五，s 的转移，随着转移五中的时钟变 量均被重置为o ，并且这些时钟变量从转移发生的时刻开始重新记录时间。因此 在时间自动机中发生一次转移，不仅会发生状态的转移，而且会对转移过程中涉 及到的某些时钟变量进行重置操作。时间自动机的这种行为能用它的一个运行来 描述。对于一个时间序列_ = 五龟，我们定义0 = o 。 基于时间自动机模型验证方法优化研究 定义2 5 时间自动机( l 上。，e ) 所识别的时间字( 盯，) 上的个运行r 表示为0 ，v ) ，定义为如下的无穷序列： r ：( ，v o ) 詈_ ( 置，h ) 卺一( s z ，v 2 ) 卺_ 其中，s ，s 并日对v j o ，v ，阻- r ，而且需要满足以下条件； 起始条件：s o ，且对魄c ，( x ) = o ； 连续性：对v f l ，在转移集合e 中存在一个形如( s 。，n 。，识。 + j 。) 的 转移，使得( v 一+ 一i 一，) 满足巧，并且叶= 丑卜o ( 叶一。+ i 一一) 。 时间自动机的一个运行描述了一个转移序列并记录了每个转移位置以及与 该转移位置所对应的所有时钟变量的时钟值。集合i n f ( r ) 包含那些对无穷多个 砸0 ) 使得s = 墨的所有状态s ，即在r 中出现无穷多次的状态所组成的集合。对 时间字( 仃，f ) 上的一个运行r = ( j ，v ) ，当处于互和气之间的某个时刻r 时，时钟 集合中所有时钟变量的时钟值等于m + f i 。因此，当发生从s ，到薯+ 的位置转移 时，我们就用时钟值v + t + 一t 来检测时钟值是否满足时钟约束；在气时刻， 被重置的那些时钟变量的时钟值都被置为o 。 在实际应用中经常会遇到异步和分布式系统等由几个子系统组成的系统，这 就需要先构造各个子系统的时间自动机，然后再组合成构造各个时间自动机的积 自动机来描述整个系统。积自动机一般通过对相同的动作标记来进行合成。 设一，= ( 工，三：，。，肖，“e 。) ，一：= 仁：，焉，：，工：，j ：，e ：) 为两个时间自动机。 那么积自动机记为爿。怕：，表示为 ( 厶。，三：焉，。u ：，x u ：，j ，) ， 其中，0 ，s ：) = ，“) ，0 ：) 并且转换可定义为： 1 对口。n ：，对巨中的( q ，a ，竹，五，一) 和：中的( j ：，口，仍，五，s ：) ，e 为 ( ( _ ，s 。) ，a ，仍、仍， u 五，0 ，s ：) ) 。 苎堕囹皇垫垫堡型堕堡塑堕垡些要塞 2 对n i ：，对e ，中的( s ，口，妒，丑，s ) 和三：中的每个t ，e 为( g ，f ) ，a ，妒，五，g ，) ) 3 对a ：。，对e ：中的( s ，口，仍a ，s ) 和厶中的每个t ，e 为( 0 ，f l a ，妒，a ，0 ，f ) ) 下图为时间自动机a l 和a 2 及它们的积自动机。 a l 一2 图2 4 时间自动机a l 和a 2 的积自动机 为了更有效地得到积自动机，在工具u p p a a l l 中采用了握手同步( h a n d s h a k e s y l l c h r o n i z a t i o n ) 和广播信道( b r o a d c a s tc h 籼e l s ) 两种方式。 2 2 时间b u c h i 自动机和时间m u l l e r 自动机 根据时间自动机接受条件的不同，时间自动机可分为时间b u c h i 自动机和时 间m u l l e r 自动机。 基于时间自动机模型验证方法优化研究 定义2 6 时间b u c h i 自动机( 简称为t b a ) 是一个六元组( ，s ，岛，c ，e ，) ， 其中( ，s ，s 。，c ，e ) 是一个时间转换表，f s 是接受状态的集合。 t b a 在时间字( 仉f ) 上的运行r = g ，i ) 称为接受运行当且仅当i n f p ) n ，中 对t b a a 接受的时间字的集合构成一个语言) ，定义为集合 ( 仃，f ) 恤在 b ，f ) 上有接受运行) 。 时间b u c h i 自动机接受的语言类称为时间j e 则语言。 定义2 7 时间语言l 是时间正则语言当日仅当对某个t b a 有l _ l ( a ) 时间正则语言类在( 有限的) 并和交下是封闭的。对l ( a ) ，u n t i m e 【l ( a ) 去掉了时间信息。而且在字母表上存存一个b u c h i 自动机接受u n t i m e 【l ( a ) 】 我们还可以用m u l l e r 接受条件来定义时间自动机。 定义2 8 时间m u l l e r 自动机( 简称为t m a ) 是一个六元组( ，s ，& ，c ，e ，f ) ， 其中( ，s ，氐，c ，e ) 是一个时间转换表，2 5 是接受状态的集合。 t m a 在时间字p ，f ) 上的运行r = 仁，i ) 称为接受运行当日仅当i n f ( r ) f 。 t m aa 接受的时间字的集合构成一个语言三0 ) ，定义为集合 ( 蠢z - ) a 在 ( 盯，f ) 上有接受运行 。 2 3 确定的时间自动机 定义2 9 一个时间转换表( ，s ，c ，e ) 是确定的当且仅当同时满足下面两 个条件： 1 它只有唯一的起始状态，即慨l = l 。 2 对任意s s 和口以及任意两个转换( s ，一，“，一，4 ) 和( s ，一，口，一以) ，时钟 限制必须满足互斥条件( 也就是说，4 ，、疋不满足) 。 一个时间转换表在给定的时间字一卜- 最多只有个运行。 一一个时间自动机是确定的当目仅当它的时间转换表是确定的。 确定的时间m u l l e r 自动机( d ，r m a ) 所接受的时间语言类存并、交、补运算下 是封闭的。确定的时间b u c h i 自动机( d t b a ) 所接受的时间语言类存并和交运算 下是封闭的，在补运算下不是封闭的。 t m a ，t b a ，d t m a 和d t b a 的所接受的语言类的关系如下： t m a = t b a ： 7 _ m 爿 d7 1 m 纠 d z l & 4 。 基于时间自动机模型验证方法优化研究 第三章基于时间自动机的验证过程 3 1 可达性分析 在时间自动机的验证过程中经常需要判断某个状态是否是从起始状态可以 到达的。实时系统的安全性验证就可以用时间自动机的可达性问题表示。如果状 态q 是可达的，那么含有状态q 的位置s 也是可达的。时间自动机a 可达性问 题的目的是为了判定某个目标位置是否是可达的，它和a 的目标位置的集合 r 至有关。可达性问题可以通过构造位置之间等价关系的有穷商来解决。 一个时问自动机的状态空间q a 上的一个等价关系被称为稳定的当目仅当 如果叫且g j g ，那么存在状态u 使得“j “并且有g “。 设a 是一个时间自动机，是q n 的一个稳定划分，考虑关系的两个等价 类石和石。由于稳定性，乃包含一个状态q 使得对某个q ，g j q 当且仅当 对石中的每个q ，都存在某个g ，使得g j 矿。这表明为解决可达性问题，只 需要等价类，而不是单个的状态。a 关于稳定划分的商是转换系统 a 卜 a 卜的 状态是一的等价类如果一个等价类石包含a 的初始状态，那么石是【a 卜的一个初 始状态；如果对某个g 万和q ，【a 包含q j g ，那么【a 卜包含标记为a 的从 等价类万到石的转换。 为了将可达性问题( a ，l 9 ) 简化为一个在等价关系上的商的可达性问题，需 要保证，非稳定性的不能将目的状态和非目的状态等价。对于目的位置的一个 集合r 三，如果存在( ( s ，v ) ( s ，v ) ，要么s 和s 都属于l f ，要么s 和s 都_ i 属 于l f ，这样一个等价关系被称为l f 一敏感的。 设a 是一个时间自动机，是q a 上的一个等价关系，l f 是a 的一个位置集 合，使得是稳定的，且是l f 一敏感的。那么l f 的一个位置是可达的当且仅当存 在一个等价关系，使得等价类石在商【a 卜中是可达的，并且石包含它的位置在 l f 中的一个状态。 因此，为了解决可达性问题( a ，l ) ，需要找到一个稳定的、l f 一敏感，月只含 基于时间自动机模型验证方法优化研究 有有限多个等价类的等价关系。 3 2 轨迹语义及其时间扩展 在轨迹( 仃a c e ) 语义内，我们考虑每个进程的一组可观察到的事件，并_ 月用所 有轨迹的集合来描述这个进程。一个轨迹是进程运行时可以观察到的事件的线性 序列。例如一个事件可能代表对一个变量的赋值，或者是在控制面板上按下一个 按钮，或者是一个消息的到达。在本文的模型中，一个踪迹是一组事件的序列。 那么如果两个事件a 和b 同时发生，相关的踪迹会有一个集合 a ，b l 。存通常的 交替模型中，这个集合会被所有可能的序列所代替，也就是说，b 跟随着a 或a 跟随着b 。同样，仅使用无限序列来模拟实时系统的非终止交互作用。形式化地， 给定事件集合a ，一个轨迹仃= 仉是在p + ( 爿) ( a 的所有非空子集的集合) 上的一个无穷字。 我们考虑进程的并行组合：一组进程的并行组合描述所有这些进程同时运行 时的共同行为。通常使用投影来定义并行组合的运算符。口尸+ ( 彳) 。存占o 上 的投影( 记作盯i b ) 是把盯中的每个事件集合和b 相交并删去序列中的所有空集。 例3 1 设信道p 联结二元素，a 代表一个消息到达p 的末端，b 代表在p 的另一 端消息的传送。当前消息未达到另一端时，p 不能接受新消息。相应地事件a ， b 交替出现。设消息爿i 断出现，唯一可能的轨迹是： 哪：知) 一 6 ) - 伽) _ 弘) - 使用符号a 表示平凡集 a ，p 的进程可表示为( a ，b ) ，- 6 。) ) 。 若还有另一信道o 与上例中的p 相连。q 消息事件的到达和b 相同。设c 表示q 另一端消息的传递，进程q 由【 6 ，c l ( 6 c ) 。) 给出。若p ，q 要复合，它们需 要在公共元素b 上同步，在每一对b 之间允许事件a 发生在c 之前，c 发生在a 之前或二者同时发生。因此，旧i q 】具有事件集k ，6 ，c ) ，并且有无限个轨迹。 存此框架下，验证问题表现为包含问题。实现和表述都以非时间进程给出， 实现进程是若干较小元素进程的组合。对于规范( 4 ，x 。) ，实现( 爿，x ，) 是正确的 基于时间自动机模型验证方法优化研究 当且仅当z ，置。 对上例所示信道，实现进程是旧| q 。规范以进程s = ，6 ，c ) ( 口6 c ) 。) 的形式 给出。因此，规范要求另一消息到达p 之前，消息到达q 的另一端。此时，由 于【p 怜】具有多余的轨迹，例如a 6 0 c 6 ) 。，所以其不满足s 的规范。 根据以上验证问题的定义，j ，= 巾对每一个规范的实现都是正确的。为克 服此问题，需要区别系统控制的输出事件和环境控制的输入事件。要求实现不能 阻止环境执行输入事件。 下面介绍加入时间扩展的轨迹语义。 非时间进程模拟事件序列，而非事件发生的确切时间。因此，上例仅给出了 事件a 和b 的序列而没有事件实际发生的时间。可以通过在轨迹中加入一时间值 序列来描述时间。同样，在这里使用实数集来模拟时间。 时间序列f = l f ：是时间值t ( t r ) 的无限序列，而且满足严格单调递 增条件。在事件集合a 上的时间轨迹是一序偶( 盯，f ) ，其中盯是a 上的轨迹，f 是时间序列。在轨迹中，卅i 同事件可在个元素中可同时发生。 在时间轨迹p ，f ) 内，每个t 给出了事件q 的发生时间。特别地，q 给出了 第个观察到的事件的发生时间。设t 0 且= 0 。递增条件蕴涵着在有界时 间间隔内，仅有有限个事件可以发生。例如1 2 ，3 4 ，7 8 这样的收敛的时间序列 就被排除在外。这样收敛的时间序列意味着在一个时间单位之前，系统有无限多 个事件发生。 事件进程是一个对偶( a ，l ) ，其中a 是有限事件集，l 是a 上的时间轨迹的 集合。 考虑例3 1 中的信道p 。设第一个消息在时间l 到达，后继消息以3 个时间 单位的固定间隔到达。并且每个消息通过信道花费1 个时间单位。进程存存一个 唯的时间轨迹： 邝= ( 口，1 ) _ ( 6 ，2 ) _ ( n ，4 ) _ ( 6 ，5 ) _ 其所代表的时间进程为：尸7 = 瞄，6 l 伽，) ) 。 基于时闻自动机模型验证方法优化研究 非时间进程的操作可以很容易地扩展到时间进程。为得到p ，f ) 在占4 上 的投影，首先以b 交盯的每个事件集合，沿与之相关的时间值删去空集。并行 组合操作除了用到时间追踪的投影的操作外，保持不变。因此，对两个进程的并 行组合操作，要求二者在同一时间参与共同的事件。这就排除了时间进程之间交 错的可能性，即两个时间轨迹的并行组合要么是单个的时间轨迹要么是空的。 若有信道q 连接到另一信道p 上。q 只有唯一可能的轨迹c r o = ( 6 c ) 。另外， q 的时间规范表明个消息通过信道的时间，即相邻b 和c 间的延迟是某个在 l ，2 之间的实数。那么时间进程q 7 有无限个时问轨迹，可以用如下形式给出： 【 6 ，c ) 慨，f 】v f 也一，+ l 乃， f 2 。+ 2 翊 【p 7 忪7j 的描述通过复合所和q 7 每一个时间轨迹得到。得到的进程有无数 个时间轨迹。例如： ( 口，1 ) _ ( 6 ，2 ) _ ( c ，3 8 ) - 0 ，4 ) _ ( 6 ，5 ) _ ( c ，6 0 2 ) _ 与事件相联系的时间值可以通过u m i m e 操作忽略。对时间进程p = ( a l ) ，e 历f 砌e 【( 一，上) 是非时间进程，其是由事件集合a 和轨迹盯组成的使得对某个 时间序列f ，( 仉f ) 三。 醐舰e 怆) m f 咖e 】胁，砌e ( b ) 但是，上面式子的两边不一定相等。换句话说，当两个进程组合时，时问轨 迹保留的信息约束了可能的轨迹。 考虑信道p 和q 相连的情况，对p 和q 分别忽略时问信息： 讲m 8 ( p 7 ) = p ，【历f f 研e ( q 7 ) = q ， 那么【p 7 峥7 _ j 忽略时间信息后所得到的轨迹为( a 6 c ) ”。但是【p 忪】有无限个轨 迹，而且在每一对b 之间，事件a 和c 可以以任何次序出现。 验证问题以包含问题出现。 考虑信道p 和q 相连的情况。若以时间进程p 7 峪7j 模拟实现，那么其满足 规范s 。s 可以表示为时间进程瞄，6 ，c l a 施) 。，f 】) 。尽管规范s 仅包含事件序列， 基于时间自动机模型验证方法优化研究 但是【p 忪7j 对应于s 的正确性依赖于两个信道的时间约束。 3 3 使用时间自动机验证 对于一个时间进程( a ，l ) ，l 是p + ) 上一个时间语言。一个时间正则进 程是一个时间进程，其中l 是一个时间正则语言并且能被时间自动机所表达。 通常一个系统可以看成几个子系统的组合。每个系统都能用一个时间正则进 程鼻= ( 一，三( 一，) ) 。可以构造一个t b a a r 来表示进程的组合肌鼻j 。为了这样做， 我们需要找出1 i 同自动机相同的字母表，然后做交运算。系统要验证的规格可以 用字母表j p + ( 爿) 上另一个时间正则语言s 来给定，其中彳= u ，4 ，。当日仅当 三，) c ：s 时系统是正确的，也就是说判断a 所接受的语言是否是语言s 的子集。 这个问题也可以通过时间自动机的判空问题来解决即三( 4 ) n s 中，也就是判 断a 所接受的语言和语言s 的交集是否为空。 有穷自动机的状态空间是以指数倍增加的。时间自动机是在有穷自动机上增 加时钟变量而进行的扩展，所以时间自动机的状态图的规模也是随着问题规模的 增大而成指数倍的增加。这个问题是