（计算机软件与理论专业论文）基于时间自动机的模型验证理论及应用研究.pdf

郑州大学硕士学位论文 摘要 实时系统是一类重要的计算机应用系统，它经常被使用在对安全性要求极高 的操作环境中，因此确保此类系统的正确性至关重要，并且需要我们使用形式化 的方法对实时系统进行规范验证。 本文在r a l u r 等人提出的时问自动机的基础上深入研究了系统模型验证理 论及其实际应用。我们通过判定实时系统以及它的规范说明所对应的时间正则语 言的交集是否为空对实时系统进行规范验证，比较常用的验证方法包括构造区域 自动机和带自动机。通过对这些方法分析研究，我们发现当系统规模较大时，规 范建模过程就会相对复杂，而且还可能会出现状态组合爆炸的问题。因此，系统 需要一种能较好解决这些问题的自动规范验证技术。 u p p a a l 是一种以时间自动机作为行为模型、在实时系统和通讯协议的自动 规范验证中占据重要位置的验证工具。在对u p p a a l 的基本结构和工作原理分 析之后，我们发现它采用的限制技术和快速验证技术可以避免构建状态空间中的 不可达状态，能在一定程度上解决状态空间爆炸问题。但是系统在自动规范验证 时没能有效利用问题求解过程中的启发性信息，并且存在一些无用状态循环，就 会导致问题求解效率低下。本文针对这些问题对快速前向验证算法进行改进，提 出了一种带有启发性信息的快速前向验证算法。文中设计估价函数用于估算每一 个全局状态到达目标全局状态需要付出的代价，定义无用状态循环用来避免对无 用状态重复分析，这样既节省了系统存储空间，又提高了求解问题的效率。接下 来，本文对一个通讯协议进行分析和规范，并且利用u p p a a l 对该协议的时间 自动机模型进行自动规范验证，证明了协议的正确性和安全性。 带有时间特性的p e t r i 网也是一种适合描述和分析实时系统的模型工具，但 是它的性能分析能力有一定局限性。因此，本文利用将时延p e t r i 网转换到时间 自动机的语义等价转换算法，将一个带有单处理器的铁路岔道系统的时延p e t r i 网模型转换成与其语义等价的一组时间自动机模型，并且利用u p p a a l 对转换 后系统模型的安全性和受限活性进行自动规范验证。 关键字：实时系统，时间自动机，协议验证，时延p e t r i 网，u p p a a l 郑州大学硕士学位论文 a b s t r a c t r e a l t i m es y s t e m sa r e u s u a l l yu s e d i n s a f e t y c r i t i c a le n v i r o n m e n t ，w h i c ha r e i m p o r t a n tc o m p u t e ra p p l i c a t i o ns y s t e m s i ti se x t r e m e l yi m p o r t a n tt oe n s u r et h e c o r r e c t n e s so f t h e s es y s t e m s s oi ti sn e c e s s a r yt os p e c i f ya n dv e r i f yt h ep r o p e r t i e so f r e a l t i m es y s t e m su s i n gf o r m a lm e t h o d s b a s e do nt i m e da u t o m a t ad e v e l o p e db yr a l u r t h e o r i e so fs p e c i f i c a t i o na n d v e r i f i c a t i o no fr e a l - t i m es y s t e m sa n dt h e i ra p p l i c a t i o n sa r ed e s c r i b e di n t h i sp a p e r r e a l - t i m es y s t e m sa r es p e c i f i e da n dv e r i f i e db yc h e c k i n gw h e t h e rt h ei n t e r s e c t i o ni s e m p t y , w h i c hi st h ei n t e r s e c t i o no ft i m e dr e g u l a rl a n g u a g e sr e c e i v e db ya u t o m a t o n m o d e l so fs y s t e mw i t ht h el a n g u a g e sr e c e i v e db yi t ss p e c i f i c a t i o na u t o m a t o nm o d e l s t h ec o u u t i o rm e t h o d sa r ec o n s t r u c t i n gr e g i o na u t o m a t aa n dz o n ea u t o m a t a w h e nt h e s c a l eo fas y s t e mi sv e r yl a r g e ，i ti sd i 斑c u l tt os p e c i f ya n dm o d e li t ，w h a t sm o r e ，t h e p r o b l e mo fs t a t e s p a c ee x p l o s i o nm a yo c c u r a sw e l l t h e ni ti si ng r e a tn e e do ft h e f o r m a lt e c h n i q u eo fa u t o m a t i cv e r i f i c a t i o nt os o l v et h e s ep r o b l e m s u p p 从li sak i n do fa u t o m a t i cv e r i f i c a f i o nt o o l ，w h i c ht a k e st h et i m e da u t o m a t a a si t sb e h a v i o r a lm o d e la n dp l a y sav e r yi m p o r t a n tr o l ei nt h es p e c i f i c a t i o na n d v e r i f i c a t i o no fr e a l - t i m es y s t e m sa n dc o m m u n i c a t i o np r o t o c o l s t or e s o l v et h e p r o b l e mo fs t a t e - s p a c ee x p l o s i o n ，u p p a a l u s e sc o n s t r a i n ts o t v i n gt e c h n i q u e sa n d f o r w a r dv e r i f i c a t i o nt e c h n i q u e st oa v o i db u i l d i n gt h es t a t es p a c et h a ta r en o tr e a c h a b l e h o w e v e r , t h es y s t e mc a nn o td e a lw i mp r o b l e m si na ne f f i c i e n tw a y , f o rt h ea b s e n c e o fh e u r i s t i ci n f o r m a t i o na n dt h ep r e s e n c eo fs o m eo s e l e s ss t a t ec i r c l e s t h u sa n i m p r o v e da l g o r i t h mu t i l i z i n g h e u r i s t i ci n f o r m a t i o ni s p r o p o s e d t os e t t l et h e s e p r o b l e m sm e n t i o n e da b o v e i nt h ea l g o r i t h m , a ne v a l u a t i o nf u n c t i o ni s d e s i g n e dt o e v a i u a t et h ec o s to f r e a c h n ga i m i n gg l o b a ls t a t ef o re v e r yg l o b ms t a t e ；a n dt h eu s e l e s s s t a t ec i r c l ei sd e f i n e dt oa v o i da n a l y z i n gu s e l e s ss t a t e sr e p e a t e d l y i nt h ef o l l o w i n g s e c t i o n s ，ac o m m u n i c a t i o np r o t o c o li sa n a l y z e da n ds p e c i f i e d ，f o l l o w e db yt h e a u t o m a t i cv e r i f i c a t i o no ft h et i m e da u t o m a t o nm o d e l so ft h i sp r o t o c o lb a s e do n u p 队a l w h i c hp r o v e st h ec o r r e c t n e s sa n ds a f e t yo f t h ep r o t o c 0 1 h 旦业兰塑主兰堡丝垄 a sat y p eo fm o d e l c h e c k i n gt o o l s ，p e t r in e t se x t e n d e dw i t ht i m e f 孔t o r sa r c s u i t a b l et od e s c r i b ea n da n a l y z er e a l t i m es y s t e m s b u tt h e yc a no n l y o f f e rl i r n i t e d 姐a i y s i sc a p a b i l i t i e ss o m e t i m e s at r a n s l a t i o n 越g o f i t h mi sd e s c r i b e di n t h i sp a p e r w h l c hc a nm a pat i m e dp e t r in e t sm o d e lo fa r a i l r o a dc r o s s i n gs y s t e mw i t has i n 9 1 e c o n t r o l l e rp l a t f o r mi n t oas e to fs e m a n t i c a l l ye q u i v a l e n tt i m e da u t o m a t a rt h e n t i l e p r o p e n i e so fs a f e t ya n db o u n d e dl i v e n e s so ft h et r a n s f o r m e ds y s t e mi s v e r i f i e db v u p p a a 【 k e y w o r d s ：r e a l - t i m es y s t e m ，t i m e da u t o m a t a ，p r o t o c o lv e r i f i c a t i o n ，t i m e dp e 研n e t s u p p a a l l i t v7 8 2 7 6 6 郑重声明 本人的学位论文是在导师指导下独立撰写并完成的，学位论文没有剽窃、抄 袭等违反学术道德、学术规范的侵权行为，否则，本人愿意承担由此产生的一切 法律责任和法律后果，特此郑重声明。 学位论文作者( 签名) ： 工静 , 2 0 0 5 年6 月 五日 郑州大学硕士学位论文 1 1 研究背景 第一章绪论 实时系统是一类重要的计算机应用系统，它被广泛地应用在许多工业领域 里，如：过程控制系统、军事防御系统、空中交通系统、病人监护系统等，它可 以根据所控制外部环境的交互情况及时做出响应以期达到预定目的。实时系统最 大的特点是执行动作一定要满足特定的时间约束，如应答时间、可执行时间、任 务周期等。确保这类系统的安全性和正确性十分重要，并且实时系统的正确性主 要依赖执行事件发生的确切时间。因此，实时系统在对安全性和正确性有严格要 求的应用系统中广泛使用，而且系统开发运行过程中若能尽早检测到错误，就可 以节约大量的资金支出以及人力、物力资源。 确保实时系统正确性和安全性的传统方法是对其进行行为模拟和反复测试。 行为模拟是一个不断交互反应的过程，即检测在不同情况下系统是否可以依据不 同的输入而做出相应正确的行为反应。测试是在系统建立之后，利用所能够预想 到的各种测试用例检胡i 系统性能的正确性。然而，即使系统能通过所有可以预想 到的测试用例，但是仍然无法保证它对所有的实际情况都能做出正确反应。因此， 这就要求我们在系统开发过程中，能够利用形式化的方法模拟实时系统的行为， 并且验证它是否满足其规范说明。 系统规范验证的方法是模拟所有可能的运行状态下系统所有可能的输入，因 此我们需要使用形式化方法模拟系统行为，使用逻辑语言表示系统的规范说明并 且需要一个有效的算法来验证所构建的系统模型是否满足用逻辑语言表述的规 范说明。例如，在一座桥上有一个铁路控制器系统，它需要满足的一个性质是在 任何时刻只允许一列火车通过大桥，这是铁路控制器系统的安全性要求；它的另 一个性质是在某一规定时刻之前火车必须穿过大桥，这是系统的有界活性【l 】。 在计算机科学领域内，自动机是分析模拟许多现象的有力工具，特别是在并 行有限状态实时系统中，自动机理论具有相当重要的地位。因此，系统的行为可 以用自动机来模拟，检查验证一个系统是否满足其规范说明的问题，就可以归结 为一个检查两个自动机所识别的语言是否相互包含的问题【2 j 。时间自动桃在实对 郑州大学硕士学位论文 系统的规范说明和模型验证中占据重要的地位，它是常用的一种描述实时系统的 形式化方法，即我们可以利用一组时间自动机为实时系统建立形式化模型。本文 采用的时问自动机模型是由r a t u r 和d i l l 等人在文章 3 ，4 ，5 ，6 】中所提出的。 1 2 研究现状 利用时间自动机对实时系统进行规范验证，在近年来得到了广泛发展。在时 间自动机中，每个动作行为都与其发生的时间密切相关，这些发生时闽又被状 态转换所允许的时间间隔所限制，也就是说，个动作行为是否能在一定的对间 间隔内发生，完全由所有与系统动作行为相关的时间值是否满足每一个与系统状 态转换相伴随的时钟约束。事实上，利用时间自动机验证一个具有有限状态的实 时系统的正确性问题，往往可以转化为判定相应的两个时间自动机所识别的时间 正则语言是否相互包含的问题，也可以看作是一个判定这两个时间正则语言的交 集是否为空的问题。 判定一个时间正则语言是否为空的方法是将识别该语言的时间自动机转化 为相应的一自动机，比较常用的方法是利用r a l u r 和d i l l 提出的构造区域自动 机的算法1 3 , a ，嗡时间自动机模型转化为区域自动机。但是在构建区域自动机的过 程中，可能会出现状态个数随着时钟个数的增加呈指数级递增，并且状态个数的 增加与时钟约束中的常量大小成正比；此外，构造出来的区域自动机模型可能会 存在许多不可达或虽可达但无用的状态。为了消除状态空间组合爆炸问题，研究 人员提出了对状态空间进行最小化的方法 7 , 8 , 9 , 1 0 , 1 1 , 12 1 3 1 ，这些方法可以较好地减少 状态个数。例如，r a l u r 等人在他们的文章【7 】中提出一种利用状态最小化算法 构建系统区域图的方法来减小所构建的系统规模。该算法可以利用系统的规范说 明直接构建一个最小系统区域图，而不需要首先构建完全区域图( d e t a i l e dr e g i o n g r a p h ) ，再对其进行化简。最近该算法已经被用于转换系统的最小化和可达性分 析之中。 我们在进行系统性质验证时，也可以使用些试探法( h e u r i s t i c s ) 来解决构建 系统模型过程中出现的状态空间爆炸问题。常用的方法有下面三种： 1 ) 在区域自动机的基础上，构造带自动机z ( a ) 。虽然带自动机模型中时钟 带的数目增长与时钟区域数日的增长呈指数级递增，可是带自动机拥有 2 郑州大学硕七学位论文 较少的可达状态，并且可达状态的数目对时钟约束中所涉及的时钟常量 的大小变化不敏感； 2 ) 构造个与带自动机z ( a ) 相似但形式比其简单的带自动机z 似) ，对 z ( 爿) 所识别的时问语言进行判断。如果z 。( 爿) 所识别的语言为空，就 表明z ( 爿) 所识别的语言为空，从而可以断定一所识别的语言也为空；反 之，不能得到类似结论，只能对带自动机z ( 爿) 所识别的时间语言的性质 进行重新判定； 3 ) 迭代算法。构造一系列与时间b i i c h i 自动机彳近似的时间b i i c h i 自动机 心，4 ，4 ，4 ，而且三( 4 + 。) c l ( 4 ) ，对于某一个珂，满足( 一) = 上( 4 ，) 。 即通过验证时间b t t c h i 自动机4 所识别的时间语言l ( 4 ) 是否为空来判 断时间b f l c h i 自动机一所识别的时间语言l ( a ) 是否为空或继续构造时 间b t i c h i 自动机4 + l ，直到存在一个正整数珂满足工( 4 ) = ( 4 ) 时结束。 近年来，利用时间自动机对实时系统进行自动规范验证技术有了一定的发 展，特别是在通讯协议自动验证方面显示了其极大的优点。其中以时间自动机作 为行为模型的自动验证工具u p p a a l 可以有效地对实时系统进行建模、模拟和 自动验证，从而确保了实时系统在实际运行中的高度正确性；此外，u p p a a l 在算法分析和通讯协议验证方面的应用也十分广泛。u p p a a l 所使用的行为模型 是由r a l u r 和d i l l 提出的时间自动机模型，每一个时间自动机模型都有可能拥 有一组整型变量和时钟变量，时间自动机之间可以通过共享的整型变量和通道进 行互相通信。重要的是，u p p a a l 采用限制技术和快速验证技术对解决建模验证 过程中出现的状态空间爆炸问题具有良好的效用。u p p a a l 已经成功地应用在许 多实时系统的用例研究中( 1 4 , 1 5 , 1 6 , 1 7 , 1 8 ，典型的应用领域包括实时控制器性能研究 和通讯协议的规范验证。 带有时间特性的p e t r i 网也是一种非常适合描述和分析实时系统性能的模型 工具。虽然这些p c t r i 网自身拥有相应的性能分析工具，但这些工具的分析能力 有一定的局限性。同时，以时间自动机作为模型基础的自动验证工具u p p a a l 功能强大、发展成熟、通用性好。因此，z o n g h u ag u 和k a n gg 等人提出种将 郑州大学硕士学位论文 时延p e t r i 网转换到时间自动机的算法【1 9 j ，利用该算法可以将实时系统的时延 p e t r i 网模型转换成与其语义等价的时间自动机模型，然后利用验证工具u p p a a l 对转换后的系统模型的安全性( s a f e t y ) 和受限活性( b o u n d e dl i v e n e s s ) 进行自 动验证。 1 3 本文的组织 第一部分简单介绍了为确保实时系统的正确性和安全性，利用时间自动机对 其进行建模和规范验证的问题在目前的研究现状以及研究意义。 第二部分给出时间自动机的形式化定义，以及利用时间自动机对实时系统进 行规范说明和性能验证的方法。例如，在时钟解释等价类基础上构建实时系统的 区域自动机模型和在区域自动机基础上构建带自动机等方法。 第三部分介绍了以时间自动机作为行为模型的自动验证工具u p p a a l 的结 构以及它采用的限制技术和快速验证技术，提出了一种带有启发性信息的快速前 向验证算法，提高了系统求解问题的效率。 第四部分利用自动验证工具u p p a a l 模拟一个网络通信协议的运行，并且 对该协议的正确性和安全性进行自动规范验证。 第五部分利用时延p e 砸网到时间自动机的语义等价转换算法，将具有单处 理器的铁路岔道系统的对延p e t r i 网模型转换成与其语义等价的时间自动机模 型，并且利用验证工具u p p a a l 对转换后的系统模型的安全性和受限活性进行 自动规范验证。 第六部分是对以往工作的总结，提出下一阶段的研究构想。 4 郑州犬学硕士学位论文 第二豪基于时间自动机的规范验证方法 时间自动机是一个带有有限时钟集合的有穷状态机，时钟集合中的时钟变量 可以取任意实数值。时钟值可以在自动机的状态转移过程中各自独立地被重嚣为 零，而且所有的时钟变量均以同样的速度记录从起始位置( 或被重置以后的位置) 开始所流逝的时间。时间自动机可以识别时间字，即一个无穷字符序列，并且其 中的每一个字符都伴随有一个非负实数时钟值，以表示事件发生的时问。时间自 动机提供了一种简单而有效的方法描述带有时间因素的系统状态转换图，因此为 实时系统的行为建模和性能分析提供了形式化方法，在实时系统的规范说明和模 型验证中占据重要地位。 2 1 时间自动机的定义 为了引入时间自动机的概念，我们约定_ 表示时间序列，v 表示时钟解释， 表示有限字符集，盯表示字符序列，占表示时间约束，t 表示时钟值。 2 1 1 转换系统 一个转换系统【3 ，4 6 h 是一个四元组( ，s ，瓯，e ) ，其中； s 是一个有限的状态集合， r ( s o s ) 是一个初始状态集合， 是一个有限字符集合， e s s 是一个状态转移集合。 转换系统彳从一个初始状态s o ( s o s o ) 开始，占中的一个状态转移( 5 ，口，j 表 示转换系统4 在输入字符a 时，从状态s 到状态s 的一个转移。通常，对于定义 在字符集z 上的一个无限字仃= q 吒，我们称，：s o 当墨红是生一是 转换系统爿定义在字盯上的一个运行，其中s o s o ，( 品+ q ，丑) ( v f 1 ) 。 郑州大学硕士学位论文 2 1 2 时间语言 我们用时间字表示实时系统的一个动作行为，即定义在事件字符集上的一个 时问字与系统的一个动作行为相对应。在稠密时间自动机模型下，通常用非负实 数集尺+ 作为系统时钟变量的取值范围。一个与时间序列r 相结合的字符序列盯 定义如下： 定义2 1 【3 l 时间序列t = t i t 2 一t i 是时间值q 的无限序列，t i r + 且t 0 ， 满足以下条件： 单调性：f 是严格单调递增的，即t ，。 有限字符集上的时间字是一个对偶p ，f ) ，盯= q 仃：是字符集上的无限 字，而上的时间语言是上的时间字集合。 我们可以将时间字p ，r ) 看作时间自动机的一个输入，它表示自动机在f 时 刻输入字符盯。如果用时间自动机来模拟实时系统的行为，那么时间字 ( q 盯：，t i t 2 ) 中的一个符号分量q 表示系统发生的一个事件，则相应的分量r 。 表示该事件发生的时间。在某些特定情况下，时间字序列中许多连续发生的事件 可能有相同的时间值。为了有效地处理这种情况，我们可以对时间字的形式化定 义作一些改动，即不要求时间序列中的时闽僵是严格单调递增的，而只要求时间 序列是单调递增的即可( 也就是说，对所有i i ，有t + ) 。 我们考虑如下一个有关时间语言的例子口1 。 例令有限字符集为 口，b ，定义时间语言厶为满足以下条件的所有时间宇 汀，f ) 组成的集合：在每一个时间字序列中，字母口和b 交替出现，并且每一对 连续出现的字母口和b ，它们之间的时间差满足递增关系。那么时间语言厶就可 以表示成如下形式： 厶= ( ( 口6 ) 。，f ) i v t ( ( 2 ，一t 2 ，一1 ) 的转移， 使得( v f 一。+ 0 - - 1 t 一。) 满足嗔，并且如果存在x ( x ) ，则v i ( x ) = o ；否则 v j ( x ) = v f l ( x ) + j f i 。1 ，可以筒记为v i = 卜o 】( 叶一1 + - - f i 一1 ) 。 8 郑州人学硕士学位论文 时间自动机的一个运行描述了个转移序列并记录了每个转移位置以及与 该转移位置相伴随的所有时钟变量的时钟值。对于一个时间序列_ r = t 1 t 2 ，我 们定义= 0 ，集合i n f ( r ) 包含那些对无穷多个i ( i 0 ) 使得j = j ，的所有位置 s ( s s ) ，即在r 中出现无穷多次的位置组成的集合。设时间字p ，f ) 上的一个运 行是，= ( s ，v ) ，当处于时间分量f 和f + 之间的某个t 时刻时，时钟集合中所有时 钟变量的时钟值是由时钟解释v j + t - r , n n 予n 。因此，当发生从到s 。的位置 转移时，我们就用时钟赋值v f + f l + 。一f l 来检测时钟值是否满足与位置转移相伴随 的时钟约束；在+ 。时刻，被重置的那些时钟变量的时钟值是0 。 2 2 确定的时间自动机 2 2 i 时间b f i e h i 自动机 一个时间b t l c h i 自动机嗍( 简记为t b a ) 是一个七元组( ，s ，s o ，c ，j ，e ，f ， 其中( ，s ，s o ，c ，i ，毋是一个时间自动机，f s 是一个接受状态集合。时间b f i c h i 自动机( t b a ) 在时间字( 仃，f ) 上的一个运行r 是一个接受运行当且仅当 i n f ( r ) n f o 。对一个时间b f i c h i 自动机t b aa ，它所识别的时间语言l ( a 1 定 义为如下所示的集合： p ，f ) i a 在p ，f ) 上有一个接受运行) 在接受运行中被t b aa 识别的所有时间字组成的集合称为t b aa 识别的 时间语言，被t b aa 识别的时间语言称为时间正则语言3 1 。 2 2 2 确定的时间自动机 在没有时钟约束的情况下，一个确定有穷自动机b 0 】有唯一的初始位置， 而且对任何一个位置s 0 s ) ，在给定输入字符a ( a ) 时，转移( s ，a ，s ) 唯一地 9 郑州大学硕士学位论文 确定了下一个位置，。我们可以用类似的标准来定义确定的时间自动机：给定一 个带有时钟约束占的位置5 ，和一个输入字符口以及一个确定时刻f ，位置转移 ( s ，口，j ，a ，5 。) 唯一地确定了下一个带有时钟约束的位置墨。确定的时间自动机允 许在同一个位置发生多个标记有相同输入字符的转移，但是伴随这些转移的时钟 约束必须互不相同，这样就保证了在任何时刻只能有唯一的一个位置转移发生。 一个时间自动机 的位置转移 所涉及的时钟约束4 和疋是互斥的( 即最 如的布尔值为假) 。 求取确定的时间自动机的补自动机是比较容易的，因为确定的时间自动枫在 给定的时间字上至多只有一个运行。检验两个时间自动机所识别语言的交集是否 为空集的算法也可以用于检验两个确定的时间自动机所识别语言的交集是否为 空集1 2 , 4 。 2 3 基于时间自动机的实时系统的规范和验证方法研究 时间自动机可以有效地描述实时系统的各种特征：活性、周期性、公平性、 有界响应、时间延迟和非确定性等，因此时间自动机在实时系统的规范验证过程 中得到了广泛应用。通常情况下，我们用一组时间自动机模型表示一个实时系统 的各个组成部分，用一个确定的时问自动机来模拟系统的规范说明。然后构造表 示实时系统各组成部分的时间自动机的积时间自动机1 4 j ，如果积时间自动机所识 别的语言包含在表示系统规范说明的自动机所识别的语言之中，那么就表明实时 系统满足该规范说明：否则就不满足。或通过判断这两个时间自动机所识别语言 的交集是否为空来判断系统的规范说明是否被满足。 2 3 1 区域自动机 1 时钟区域 1 0 郑州大学硕士学位论文 定义2 5 设爿= ( ，s ，s o ，c ，d 是一个时间自动机，如果有s s ，v 是时钟 变量集合c 上的一个时钟解释，就称序偶( s ，d 是爿的一个状态。 时间自动机4 的时钟变量的取值范围是非负实数集r + ，如果4 的状态是定 义2 5 所描述的形式，那么状态数f i 是不可数的，因此我们无法建立一个状态数 目是不可变的自动机，即无法用时间自动机爿的状态构建一个系统的自动机模 型。但是研究人员发现，如果两个时间自动机具有相同的a 位置，并且处于该 位置的所有时钟值的整数部分相同，小数部分的次序保持不变，那么起始于这两 个状态的运行将非常相似。时钟值的整数部分通常用于确定是否满足相应的时钟 约束，而时钟值的小数部分的顺序则用于确定哪一个时钟变量将首先改变它的时 钟值的整数部分。例如，在时间自动机的某一个状态，如果时钟变量工和y 的时 钟值满足( 0 x 1 a 0 y 1 ) ，那么伴随有时钟约束( y = 1 ) 的位置转移是否可以 跟在伴随有时钟约束o = 1 ) 的位置转移之后，完全取决于这两个时钟变量目前的 时钟值是否满足 y ) 。 在给出时钟解释集合上等价关系的形式化定义之前，我们先对要用到的符号 作一个简单介绍。对v f r + ，一( r ) 表示r 的小数部分， t j 表示t 的整数部分， 即扛【，j + 夕。对于时间自动机一= ，其中s o s ，并j i v x a c ，v o ( x ) = o ； 3 ) r ( a ) 中有一个状态转移( ( s ，口) ，a ， 当且仅当时间自动机4 中存在 一个转移( j ，a ，占，丑，s se 并且存在一个时钟区域口满足以下三个条件： 口7 是口的时间后继；口。满足时钟约束占；= 阴h o a 。 3 利用区域自动机进行系统规范验证 对一个有限状态的时间过程p ( a ，) ，其中4 是时问过程中所有事件组成的 集合，三是定义在集合p ( 椰上的时间语言，我们可以用时间b t l c h i 自动机t b aa e 1 2 郑州大学硕士学位论文 模拟时间过程尸，即用时间b i i c h i 自动机t b aa e 模拟时间过程p 的过程转换图， 用自动机4 的时钟变量表示时间过程p 的时间延迟，用自动机4 的接受条件表 示时间过程尸的公平性条件【6 】。因此，时间b i i c h i 自动机t b a 以所识别的时间 语言三( 4 ) 可以用来表示时间过程p 的所有时间运行。一个时间过程_ p 往往包含 多个执行过程，因此相应的t b a4 的构建是困难和繁琐的。通常情况下，我们 将时间过程p 的一个执行过程描述为该时间过程的一个子过程p = ( 4 ，上( 4 ) ) ， 其中4 表示子过程只所涉及到的事件组成的集合。这样我们就可以为每一个子过 程构建其相应的t b aa e , ，然后构建一个t b a 4 表示所有子过程的积叽 。 时间过程p 的规范说明用一个确定的t b aa s 表示，其中4 识别的语言集合是定 义在字符集p ( a ) ( a = u ，4 ) 上的时间正则语言s 。时间过程p 是正确的当且仅 当三( 4 ) s 或者三( 4 ) n s o ，即时间过程p 能够满足自身的规范说明s 。 接下来我们根据区域自动机的构建方法，构建t b aa i 和t b a4 的积时间 自动机4 = 4 1 4 对应的区域自动机矗( 4 ) 。为了检验t b a4 和t b a4 所识 别语言的包含关系，我们可以在区域自动机r ( 4 ) 中查找是否存在一个满足如下 条件的状态环 6 1 ： 1 ) 它包含r ( 4 ) 的初始状态( s o ，【v 0 】) ； 2 ) 它的时钟变量满足递增条件：对所有的时钟变量x ( x c ) ，该状态环中 至少存在一个时钟区域满足【 = o ) v ) 】； 3 ) 由于子过程只的定义要求只考虑那些所有自动枫模型都无穷多次参与 执行的无限运行，因此，对每一个l i 一，该状态环中应该包含一个 过程p 的所有子过程对应的自动机t b a a e , 参与的状态转移： 4 ) 所有子过程对应的t b a 如必须满足公平性原则：即对每一个1 i - ”， 状态环中必须包含一个状态，它的第i 个状态分量属于t b aa e , 的接受 l 郑州大学硕士学位论文 集合f ； 5 ) 规范说明对应的t b aa s 的公平性无法被满足：该状态环中不能包含这 样的状态，它的与t b a 呜对应的状态分量属于t b aa s 的接受集合只。 如果区域自动机震( 4 ) 中存在满足上述条件的状态环，就说明 上( 一，) 旺s l ( a ，) s ，即( 一，) n s = 彩。 虽然区域自动机在实时系统的规范验证过程中起到了举足轻重的作用，但是 区域自动机的状态数目会随着时钟集合中时钟变量数目的增加而呈指数级递增， 并且状态个数的增加与时钟约束中的常量大小成正比。此外，构造出来的区域自 动机模型可能会存在许多不可达或虽可达但无用豹状态，因此研究人员就考虑利 用一些启发式规范验证方法来解决这些问题。 2 3 2 启发式规范验证方法 为了解决区域自动机构建过程中出现的状态空间爆炸问题，我们也可以引用 一些带有启发式的规范验证方法，比如说在区域自动机的基础上构建带自动机， 通过构建与时间自动机a 相似的时间自动机等方法，下面分别进行介绍。 1 带自动机 时间自动机a = 中的一个时钟带是将一个或多个时钟区域进 行合并。带自动机z ( 一) 是建立在字符集上的一个转换系纠3 | 4 ，6 l ： 1 ) z o ) 的状态形如 ，其中s s 并且是口一个时钟带； 2 ) 初始状态形如( ， v o 】) ，其中s o ，而且垤c ，v o ( x ) = 0 ； 3 ) z ( a ) 中有一个状态转移( ( s ，口) ，a ， ) 当且仅当时钟带包含所有满 足状态转移 - c ，x y c ( x ，y 是时钟变量，c 是时钟常量) 的线性不等式以及这些不等式的布 尔合取式表示，那么就称该时钟带是简单的；这样就可以保证时钟带中所有时钟 变量不等式的形式一致。便于用形式化方法统一表示。一个简单时钟带可以用有 界差分矩阵( d i f f e r e n c e b o u n d m a t r i x ) 表示f 2 l 】。如果带自动机z o ) 的状态 是从起始状态可达的，那么时钟带口就是简单时钟带的并集。 一个时间自动机爿所识别的时间语言是否为空可以通过判断带自动机z “) 中是否存在状态环来进行。理论上讲，时钟带的数目会随着时钟区域数目的增加 而呈指数级递增，这样带自动机z ( a ) 的状态数目应该远远大于区域自动机r ( a ) 的状态数目。但实际上，带自动机中的每一个状态在输入一个确定字符的情况下， 至多有一个后继状态，因此带自动机拥有较少的可达状态。此外，虽然时钟区域 的数目与时钟约束中常量大小的变化成正比，但是实验表明时钟带的数目对于时 钟约束中常量大小的变化不敏感，因此带自动机的状态数目远远小于区域自动机 的状态数目。 2 近似法 为了提高在带自动机中搜索状态环的效率，我们可以引入近似法技术。带自 动机中的时钟带都是简单时钟带，某些时钟带可以是一些简单时钟带的并集，如 果使用一个包含所有简单时钟带的最小简单时钟带代替这些简单时钟带的并集， 将会加快搜索速度。例如，时钟带x 1 v 2 x 3 可以用简单时钟带x 当且仅当时钟带盯是包含所有 时钟解释v 的最小简单时钟带( ，霰要满足 s ， ，口， 。 在带自动机z ( 彳) 的基础上构建近似带自动机捌z + ( 4 ) ，因此z ( 爿) 的接受条 件可以转换为z ( 彳) 的接受条件，即我们可以通过检查z + ( 一) 中是否存在状态环 来验证一所识别的时间语言是否为空。如果z ( 一) 识别的语言为空，就表明z ( a ) 识别的语言也为空，从而可以断定彳识别的语言为空。如果a 表示一个时间过程 p 和它的规范说明s 的补的积时间自动机( 即l ( a ) = l ( p ) n l ( s ) = o ) ，那么就 说明时间过程尸满足其规范说明s 。当z ( 一) 识别的语言非空时，我们就不能得 到z ( 一) 识别的语言也不为空的结论。此时，我们就