（计算机软件与理论专业论文）基于时间自动机的实时系统规范验证研究.pdf

基于时间自动机的实时系统规范验证研究 y ，刁a _ ，若z 摘要 实时系统不仅要求逻辑上是正确的，而且要求时间上也是正确的，这类系统 在设计阶段需要进行严格的分析和验证。时间自动机是使用最为广泛的对实时系 统进行规范验证的形式化方法之一。 实时系统验证主要分为安全性验证和活性验证，系统的活性可以通过位置的 不变式和转移的约束条件保证，验证也比较容易，本文对此不作过多讨论。安全 性验证问题可归结为时间自动机的可达性分析，基于状态空间搜索的方法主要不 足在于状态空间的大小随着过程数目的增加呈指数级递增，这就导致了状态空间 爆炸问题。为了解决这个问题，我们必须构造时间自动机状态空间的有穷表示。 本文主要研究了a l u r 提出的域自动机方法、带自动机方法以及i n h y ek a n g 等提出的状态空间最小化方法，并在此基础上提出了时间段转换系统以及对状态 空间的极小化方法。该方法用位置和进入位置的最大最小时钟值集合来表示状态 而得到时间段转换系统，同时通过转换分析保留有效转换来简化这个转换系统。 对简化后的系统，使用转换互模拟进行最小化。文中对该方法进行了可行性分析， 通过与其它方法进行比较阐述了该方法的优点和不足，并建立了铁路交叉口控制 门系统的最小化过程。 在规范验证应用方面，本文研究了两种典型实时系统道岔自动控制系统 和自动筛选器系统。通过对系统进行分析和规范，给出了系统的时间自动机模型， 并使用u p p a a l 对模型进行验证，证明了系统的安全性、有效性和可控性。 关键词：实时系统，时间自动机，模型验证，转换系统，可达性，活性，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 sd e m a n dt h ec o r r e c t n e s so ft i m ea sw e l la sl o g i c ，w h i c hd e m a n d r i g o r o u sa n a l y s e sa n d v e r i f i c a t i o nd u r i n gt h ed e s i g ns t a g e t i m e da u t o m a t ai so n eo f t h em o s tu s e dm e t h o d sf o rs p e c i f y i n ga n dv e r i f y i n gr e a l t i m es y s t e m s 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 si n c l u d e sc h e c k i n gs a f e t yp r o p e r t i e sa n dl i v e n e s s p r o p e r t i e s l i v e n e s sp r o p e r t i e sc a n b eg u a r a n t e e db yi n v a r i a n ta n dc l o c kc o n s t r a i n t s a n di t sv e r i f i c a t i o ni s e a s y s ow ew o n tc o n s i d e r i tt o om u c hi nt h i s p a p e r t h e c h e c k i n go fs a f e t yp r o p e r t i e si sb a s e d o nt h ea n a l y s i sa n ds t a t es p a c ec h e c k i n g t h e m a j o r w e a k n e s so ft h es t a t es p a c ee x p l o r a t i o ni st h a tt h es i z eo ft h es t a t es p a c eg r o w s e x p o n e n t i a l l y w i t ht h en u m b e ro fp r o c e s s e s ，w h i c hc r e a t e st h es t a t es p a c ee x p l o s i o n p r o b l e m s o w em u s tc o n s t r u c tt h ef i n i t er e p r e s e n t a t i o no ft h er e a c h a b l es t a t e s ， 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 n dt h em e t h o do fs t a t e s p a c em i n i m i z a t i o nd e v e l o p e db yi n h y ek a n g f u r t h e r , w ed e v e l o p t i m es e g m e n t t r a n s i t i o ns y s t e ma n dam e t h o do fs t a t es p a c em i n i m i z a t i o n t h em e t h o du s el o c a t i o n a n dt h ep o s s i b l et i m ed i s t a n c es t a y i n gi nt h i sl o c a t i o nt od e n o t et h es t a t e w er e d u c ei t u s i n gt r a n s i t i o na n a l y s i sa n dr e m o v i n g o f fi n v a l i dt r a n s i t i o n t h e n ，w eu s et r a n s i t i o n b i s i m u l a t i o nt om i n i m i z et h et r a n s i t i o n s y s t e m i n t h e p a p e r , w ea n a l y s e s t h e f e a s i b i l i t yo ft h em e t h o d ，a n ds h o w i t sa d v a n t a g ea n dd i s a d v a n t a g eb yc o m p a r i n gi t w i t ho t h e r s w ea l s oc o n s t r u c tt h em i n i m a l p r o c e s s o f t r a i n g a t ec o n t r o ls y s t e m s c o n s i d e r i n g t h ea p p l i c a t i o no f s p e c i f i c a t i o na n dv e r i f i c a t i o n ，w er e s e a r c h t w ok i n d s o fr e a lt i m es y s t e m s - - t u m o u ta u t oc o n t r o ls y s t e m sa n da u t os i z e rs y s t e m s w eg i v e t h et i m e da u t o m a t am o d e l so ft h e mb ya n a l y s e sa n ds p e c i f i c a t i o n ，a n dc h e c kt h e mb y u p b 钆i w h i c hd e m o n s t r a t et h es a f e t y , e f f i c i e n c ya n dc o n t r o l l a b i l i t yo ft h es y s t e m s k e y w o r d s ：r e a l - t i m es y s t e m s ，t i m e da u t o m a t a ，m o d e lc h e c k i n g ，t r a n s i t i o ns y s t e m s ， r e a c h a b i l i t y , l i v e n e s sp r o p e r t i e s ，u p p a a l 1 1 基于时间自动机的实时系统规范验证研究 1 前言 1 1 研究背景 实时系统( r e a l t i m es y s t e m s ) 是指能对来自所控制的外部环境( 物理过程) 的 交互作用做出及时响应以达预定目的的计算机系统，是一种定量的反应式系统 叽过程控制、敏捷制造、铁路调度、核反应堆等许多计算机控制系统都属于实 时系统。这类系统的任何一个错误都会带来重大的经济损失，环境破坏，甚至威 胁到生命安全。这些系统需要一个严格的结构，使各种设计选择可以规范、分析， 在执行前可以被检验。 大家都认为，将来的实时系统将会更复杂，因为随着问题领域的增加，它们 的作用要求也会增加，因此，没有计算机辅助工具，分析和验证将会更复杂。实 时系统的一个共同特点是它们必须在严格的时间限制下作出响应。也就是说它们 的正确性不仅依赖于并发成分如何相互作用，还依赖于这些交互作用发生的时 间。另外，这些系统设计原型是昂贵的，需要在执行前对时间性质作出详细的预 测，并且估计设计的选择。实时系统不仅要求所产生的结果在逻辑上是正确的， 而且要求在时间上也是正确的。也就是说，要能够验证实时系统的安全性和活性。 模型验证是作为一种复杂交互系统的调试方法而出现。在模型验证中，一个 系统的规范是一个逻辑上的正确性比较，以此来发现矛盾。传统的模型验证方法 不能对时间进行建模，所以不适用于实时系统的分析，实时系统的正确性依赖于 不同时延的大小关系。因此，时间自动机作为模拟实时系统行为的模型被引入。 它是广泛使用的对实时系统进行规范验证的形式化方法之一，它通过使用有限个 实数值时钟变量来表示有时问约束的状态转换图。时间自动机的自动分析依赖于 无穷的时钟计算空间的一个有穷商。 各种各样的时间自动机曾被用于描述实对系统f 2 捌，本文采用出r 越u r 等人 引入的时间自动机1 2 , 6 , 7 i ，它给转移和位置都加上了时间约束。 1 2 研究现状 时间自动机的安全性验证是基于状态空间的分析和验证，状态空间探测法的 主要不足在于状态空间的大小随着过程数目的增加呈指数级增加，这样导致了状 举于时间自动机的实时系统规范验证研究 念空间爆炸。这个问题在实时系统中尤其严重，因为实时系统的无穷时间值使得 状态空间无穷。我们必须构造时间自动机状态空间的有穷表示。 易于时间自动机的实时系统验证已经被充分研究t 5 , 8 , 9 , 1 0 】。大部分的验证算 法是基于一个区域图【”，它是时间自动机的一个可达图。在时问的每一点上，时 间自动机的状态由当前位置和时钟值唯一确定。无穷多个时间域导致状态空间有 无穷多个状态。一个域图是对状态进行合并所得到的状态空阳j 的一个有穷表示， 等价类的状态在某种意义上是等价的。但是，域图方法仍然可能受到状态爆炸问 题的侵扰【“。 本文研究的有穷商构造方法主要有r a l u r 提出的基于时间区域等价的域自 动机构造方法，以及将连续时间区域合并后形成凸时钟带的带自动机构造方法 【6 ，”。域自动机的转换图中的很多顶点可以合并，状态空间不是最小的。虽然带 自动机有较少的可达顶点，但是带的个数是域个数的指数倍，因此，带自动机的 规模有可能会比域自动机大指数倍。 要构造一个时间自动机状态空间的有穷表示，除了建造域或者带自动机外， 还可以使用一个最小化算法，即通过对个给定的初始划分进行它所需的划分来 获得一个稳定的虽小表示。本文研究的晟小化方法主要是i n h y ek a n g 等提出的 利用历史等价性和强转移模拟关系合并等价状态，把状态表示为一个结点和一个 没有时间值的历史，历史记录了直到当前结点系统所执行的全部转移【1 1 】。这个算 法可以较好的解决状态爆炸问题，但是算法需要对历史构造带权图，以此来计算 最大最小距离，而且判断两个状态是否满足强转移模拟关系的条件比较复杂。当 然还有其它最小化方法1 1 2 - 1 7 。 1 3 研究内容 本文系统地研究了基于时间自动机的验证方法。首先介绍了如何用时间自动 机对实时系统建模，接着阐述时间自动机对实时系统验证的两个主要方面：安全 性和活性。关于安全性，可以通过可达性的分析来验证，本文第3 章着重介绍了 这些内容。关于活性，我们在第4 章的时间自动机理论验证中介绍。本文在第5 章研究了以时问自动机作为模型的验证工具u p p a a l ，以及基于该工具的实时系 统规范验证。 2 基于时间自动机的实时系统规范验证研究 时间自动机的安全性验证是基于状态空间的分析和验证，状念空间探测法的 主要不足之处在于状态空间的大小随着过程数目的增加呈指数级增长，这样导致 了状态空间爆炸问题。这个问题在实时系统中尤其严重，因为实时系统的无穷时 间值使得状态空间无穷。本文通过给位置增加进入该位置的最早时间和离开该状 态的最晚时间来模拟状态构造了一种转换系统。通过转换分析删去无效转换来简 化该转换系统。并借鉴双向转移互模拟对该转换系统进行最小化，由此得到个 最小可达状态图。并将该方法应用于一个典型的实时系统铁路交叉口控制门 系统，得到了该系统的最小可达状态图。 本文所介绍的工具中，u p p a a l 是一个发, nl p 较成熟，且效率很高的自动验 证工具。我的另一个主要工作是用工具u p p a a l 对两个实时系统道岔自动 控制系统和筛选器控制系统进行了规范以及验证。 1 4 本文结构 本文是如下组织的： 第1 章引言，介绍研究背景、现状和本文主要研究内容和意义。 第2 章介绍时间自动机建模方法。 第3 章介绍时间自动机验证的可达性分析，着重讲述如何解决状态空间爆炸 问题，提出了一种实时系统状态空间分析的方法。 第4 章介绍了时间自动机理论验证。 第5 章介绍使用时间自动机模型的工具及其应用，着重介绍了自动验证工具 u p p a a l ，并使用u p p a a l 对两个具体的实时系统进行了规范和验 证。 第6 章对本文进行总结，展望未来的工作。 基于时间自动机的实时系统规范验证研究 2 时间自动机建模 通常，我们使用标有事件标记的状态转换图对系统进行建模。 2 1 转换系统 2 1 1 转抉系统 一个转换系统 6 , 7 1 s 是一个四元组( q ，q o , z ，一 ，这里： q 是一个状态集合， q o q 是一个初始状态集合， z 是一个标记( 或事件) 集合， 一q x z q 是一个转换集合。 将一中的一个转换c 毋a ，q ，记为q 山g7 。系统从一个初始状态开始，如果 q 山口，那么系统在事件a 时从状态q 转移到q 。如果对某个标记 a ，q g ，那么记之为q q 。如果q 一4 q ，则状态q 是从状态口可达的。 如果状态q 是从某个初始状态可达的，那么q 是转换系统中的一个可达状态。 一个复杂系统可以被描述为多个相互作用的转换系统的积。设 s 。= c q 。，钟，z 。，一。 和s ：= t q ：，q ：，艺：，一： 是两个转换系统。那么，在s 。和s ： 的积中，一个状态是一个对偶国，q7 ) ，目q e q l ，日q ：，积的转换标记为z 。u z ：中的标记。对一个标记口，为得到积的一个标记为a 的转换，需要每个成员系 统执行一个标记为a 转换。形式上，这个积表示为s 。i is ：，是一个转换系统 ，这里( 吼，q ：) 山0 ：，q ：) i f f 口lnz 2 且g l 三- _ 1 口：，9 2 ! 2 q ：，或者 a z 1 2 r q l 山1 “，q ：正q 2 ，或者 a g z 2 z l 且口2 2 q ：，q ：= q l 。 d 基于时间自动机的实时系统规范验证研究 其中，z ，表示集合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 n t ) ，且要求只有在不变式为真时，时间可以在这 个位置上流逝。在给出时间自动机的形式化定义前，让我们先看一下几个例子。 图2 1 时间自动机的一个例子 考虑图2 1 所示的时间自动机。初始位置为s ，有一个单一时钟工。初始位 置没有不变式约束，这意味着系统可以在位置s 停留任意时间。当系统在标记a 发生时转移到位置s ，同时时钟算复位。在位置s 时，时钟x 的值记录从上一个 转换发生到即时的时间，从位置s 到j 的转移能够发生当且仅当这个值大于1 。 位置s 7 的不变式zs2 说明系统在s 最多可以停留2 时间个单位，个转移必须 在不变式变为不满足前发生。那么这个自动机表示的时间约束是在a 和接下来的 b 之间的时间延迟总在1 和2 之间。 d ：望 2 图2 2 有两个时钟的时间自动机 5 c 基于时闫自动机的实时系统规范验证研究 当有多个时钟时允许多个并发的延迟，如图2 2 所示。每次在标记口下系统 吠s 。到s 1 转移时，时钟x 复位。位置s 。和s ：的不变式0 1 ) 保证从s ：至1 s 3 的标记 为c 的转移在先前的a 发生后的一个时间单位内发生。在从s 。n s 。的标记为b 的 转移发生时另一个独立的时钟y 复位，在从s ，n s 。的标记为d 的转移发生时检查 时钟y 的值，确保在6 和接下来的d 之间的时间延迟总是大于2 。s ，没有不变式 约束，事件d 可以无限延迟，也可以不发生。 2 2 时间自动机 2 。2 。1 语法和语义 在给出时间自动机的定义前，先给出两个定义： 定义1 1 时钟约束1 6 , 7 1 对于一个时钟变量集x ，时钟约束伊的集合中昭) 定义为如下文法 妒：= x 量c i cs x i 工 c i c z i 妒1a 妒2 这里，x 是x 中的一个时钟，c 是取+ 中的一个常量，取+ 表示非副实数集， 妒。和妒：是时钟约束。另外，诸如t r u e ，x e 2 ，5 】等是一种缩写的时钟约束。 定义1 2 时钟解释1 6 ， r l 一个时钟集合z 的一个时钟解释v 是指给每个时钟分配一个实数值；即：它 是个从x 到非负实数集瓜+ 的一个映射。工的一个时钟解释v 满足x 上的一个 时钟约束妒t 当且仅当依n v 给出的值，妒为真。对于6 矗，y + 6 表示一个时 钟解释，它对每一个时钟z 的赋值为v 0 ) + 6 。对y z ，v y ：- 0 1 表示x 的一 个时钟解释，它给每个z y 复位，并使其余的时钟值持续增加。 定义1 3 时闾自动机用 一+ 时f n q 自动机彳是一个六元组( ，l o , z ，x ，西，其中 三是一个有穷的位置集合， 三。c l 是一个开始位置集合， 6 基于时间自动机的实时系统规范验证研究 是一个有穷标记集合， x 是一个有穷时钟集合， ，是一个映射，它给己中的每个位置s 指定由傅) 中的一个时钟约束， e c l x 中( x ) 2 。l 是一个转移集合。( s 4 ，e , a s ) 表示输入标记口时，从 位置s 到位置s 。的转移。妒是x 上的一个时钟约束，它在转移发生时被满足； a z 是在该转移发生时复位的时钟集合。 定义1 4 时间转换系统【7 l 时间自动机的爿语义通过和它相关的转换系统颤来定义。颤的一个状态是 一个二元组( s ，v ) ，s 是a 的个位置，v 是满足不变式姻的石的一个时钟解释。 a 的所有状态的集合记为必，如果s 是爿的一个初始位置，且对于所有的时钟 x ，v g ) 1 0 ，那么状态( s ，v ) 是一个初始状态。戳有两种类型的转换： 状态可以因为时间流逝而改变：对一个状态o ，和一个实数值时间增量 6 0 ，如果对于所有的0 sd s6 ，y + 6 都满足不变式，( s ) ，那么 ( s ，v ) k o ，v + 6 ) 。 状态可以因为一个位置转移而改变：对于一个状态( s ，v ) 和一个转移 ( s ，4 ，妒，a ，s )，如果v 满足妒，那么o ，v ) ! 一0 ，v 阻净0 ) 。 这样，甄是具有标记集zur + 的一个转换系统，即它的转换标记可以是 口，也可以是d r + 。 2 2 2 时间自动机积的构造 一般情况，一个比较复杂的系统由并行的、互相通讯的几个时间自动机组成。 这些并发的时间自动机可以用如下方法合成为一个时间自动机：这个时间自动机 的非共享事件的转换是交叉执行的，而共享一个事件的转换是同步的。为了描述 这样的系统，就需要用到两个或者多个时间自动机，因此给出一个时间自动机积 的构造方、法( 7 】，这样，复杂系统可以被定义为成员自动机的积。 设a 。t ( l l , l o ，z ，z 。，1 1 ，e ，) 和彳：一伍：，e ，z 2 ，x 2 ，i ：，e 2 ) 是两个时间自动 基于时间自动机的实时系统规范验证硼f 究 机，假设时钟集合，和x ：不相交，那么a ，和4 的积记为a 。0 爿：，它是一个时 间自动机( 三，x l ：，霉骂，u ：，x u x ：，e ) ，这旱，l ( s l ，s 2 ) = l ( s ，) a i ( s 2 ) ， 积的转移e 的定义如下： 1 对于所有，r 3 ：，e 。中的每一个转移( 毛，a ，吼，1 ，s ：) 和e ：中的每一个转 移( s ：，妒：，a ：，5 ：) ，e 中包含转移( “，s ：) ，口，妒。a 妒：， ua ：，( s ：，s ：) ) 。 2 对于所有口。：，e 。中的每一个转移( s ，口，妒，a ，s ) 和：中的每一个位置f ， e 中包含转移( ( s ，f ) ，口，仍a ，( 5 ，f ) ) 。 3 对于所有a 2 z 。，e ：中的每一个转移( 以a ，仍a ，s ) 和l 。中的每一个位置f ， e 中包含转移( ( f ，s ) ，口，伊，丑，( f ，s ，) ) 。 这样，积的位置是成员位置组成的元组( 称为复合位置) ，一个复合位置的不变 式是成员位置不变式的联合。转移通过用相同的标记同步转移得到。积的构造在 图2 3 说明。很容易检验积的转换系统是成员转换系统的积：s i i 也和i is 。：是 同型的。这表明时间转换系统不仅在公共标记的转移上同步，而且在时间流逝量 上也是同步的。 ：! ，搴考 1 i6 i ：= 0 图2 3 时间自动机积构造 例子：铁路交叉口控制门系统 我们考虑一个在轨道交叉处开关门( t r a i n - g a t e ) 的自动控制器的例子，如图2 4 所示，这个问题曾被用作实时系统的不同形式化方法的比较1 1 甜。系统由图2 5 所 示的三个主要成分组成，t r a i n ，g a t e ，和c o n t r o l l e r ，它们之间通过以下事件同 8 基于时间自动机的实时系统规范验证研究 步和通讯：a p p r o a c h , e x i t , l o w e r 和d o w n 。当个火车接近路口时，t r a i n 给 c o n t r o l l e r 发出信号a p p r o a c h ，至少3 0 0 秒后进入路口( 用事件抽表示1 。当一个 火车离开路口时( 用事件e x i t 表示) ，t r a i n 给c o n t r o l l e r 发出信号e x i t 。在信号 a p p r o a c h 发出后5 0 0 秒内发出e x i t 信号。控制器在接收到a p p r o a c h 信号1 0 0 秒 时发出l o w e r 信号给g a t e ，在e x i t 信号后1 0 0 秒内发出r a i s e 信号。g a t e 收到l o w e r 后1 0 0 秒内作出响应d o w n ，收到r a i s e 后1 0 0 到2 0 0 秒之间做出响应u d 。整个 系统就是合成的时间自动机t r a i n l l g a t e l l c o n t r o l l e r ，我们称之为g t c ，如图2 6 所示。位置( f j 内表示t r a i n ，g a t e ，和c o n t r o l l e r 分别在位置f ，和k 。积位置的不 变式是这三个成员不变式的联合。 n p p r o a d l i n g i ng a t e 图2 4 铁路交叉口控制门系统示意 涉二移 。i 。沁tf 。司o o i i i n , 。； 毪 t r 赫n 9 g 撇 基于时间自动机的实时系统规范验证研究 ；1 0 w 觏 c o n t r o l l e r 图2 5 成员自动机t r a i n 、g a t e 和c o n t r o l l e r 注：i n v ( 0 ，0 ，0 ) = t r u e i n v ( 2 ，0 ，1 ) - ( x = 5 0 0 , z = 1 0 0 ) i n v o ，1 ，3 ) = o r - 1 0 0 ，z = 1 0 0 ) l n v ( 2 ，1 ，2 ) = ( x = 5 0 0 ，y = 1 0 0 ) i n v o ，2 ，3 ) = ( z = 1 0 0 ) i n v ( 2 ，2 ，2 ) = f x = 5 0 0 ) i n v ( 0 ，3 ，0 ) = ( x o o ，z = 1 0 0 ) i n v ( 2 ，3 ，1 ) = ( x = 5 0 0 ，y = 2 0 0 , z = l o o ) i n v ( 1 ，0 ，1 ) = ( x - 5 0 0 ，y = 1 0 0 ) i n v ( 3 ，0 ，1 ) = ( x = 5 0 0 # = 1 0 0 ) i n v ( 1 ，1 ，2 ) = ( x = 5 0 0 ) i n v ( 3 ，1 ，2 ) = ( x = 5 0 0 ，y = l o o ) i n v ( 1 ，2 ，2 ) = ( x = 5 0 0 ) i n v ( 3 ，2 ，2 ) = “ = 5 0 0 ) l n v ( 1 ，3 ，1 ) = ( x = 5 0 0 ，y = 2 0 0 , z = 1 0 0 ) i n v ( 3 ，3 ，1 ) = ( x = 5 0 0 ，y = 2 0 0 ，z 2 0 0 约束的事件胁前边发生。事实上，在转换系统s c r c 中没有t r a i n 在位置2 ，g a t e 不在位置2 的可达状态。 基于时间自动帆的实时系统规范验证研究 3 可达性分析 时间自动机a 的一个位置s 是可达的，如果某个含位置s 的状态q 是转换系 统函的一个可达状态 7 i 。可达性问题的输入包括个时间自动机a 和一个a 的 目标位置的集合r 。可达性问题决定某个目标位置是否是可达的。实时系 统的安全性验证可以用时间自动机的可达性问题表示，就像在控制门例子中表明 的那样。既然一个时间自动机的转换系统乳是无限的，那么可达性问题的解决 方法就应该包括有穷商( q u o t i e n t s ) 的构造。 3 1 时间抽象转换系统 设a 是一个时间自动机，转换系统颤有无穷多个状态和无穷多个标记。第 一步，通过隐藏标记为时间增加的转换来定义另一个转换系统，它的转换只允许 用中的符号标记。为了达到这个目标，每当颤包括一个从状态q 到状态口的d 标记的转换和一个从q7 到q ”的a 标记为的转换，我们就增加一个从q 到的n 标记的转换。该转换系统被称为时间抽象( t i m e a b s t r a c t ) 转换系统，因为它不保留 在转换中时间流逝量的信息。 形式地，一个时间自动机a 的时间抽象转换系统记为巩。定义如下：u a 的状态空间等于勘的状态空间必，乩的初始状态集合等于颤的初始状态集合。 的标记集合等于a 的标记集合。砜的转换关系是j ：对状态q 和q ，以及 标记a ， g 辛掣当且仅当存在一个状态g ”和一个时间值6 月使得在转换系统 岛中有q q ”与日。 在时间自动机的可达性问题上，我们希望确定目标位置的可达性。注意a 的一个位置s 是可达的当且仅当在时间抽象转换系统观中，某含位置s 的状 态是可达的。由此可知为了解决可达性问题，我们可以考虑时间抽象转换系统 以而不是乳。 稳定商 虽然时间抽象转换系统巩包含有穷多个标记，但是它仍然有无穷多个状态。 基于时问自动机的实时系统规范验证研究 为了解决这个问题，我们考虑在状态空间 上的等价关系，以此将状态分组。 一个时间自动机的状态空间必上一个等价关系被称为稳定的当且仅当如果 口。且gs ，那么，存在一个状态。使得就琴2 t 并且有口7 一钮。换句话说， 一个稳定的等价是时问抽象转换系统的一个互模拟。 设a 是一个时间自动机，是q _ 的一个稳定划分，考虑关系的两个等价 类玎和玎。由于稳定性，玎包含一个状态q 使得对某个q 石，q = 叮当且仅 当对石中的每个q ，存在某个q ，万，使得譬s 矿。这表明为解决可达性问题， 只需要等价类的迹，丽不是单个的状态。觇关于稳定划分的商是转换系统 【u 。卜：。 一的状态是的等价类；如果一个等价类仃包含以的初始状态， 那么玎是【u 卜的一个初始状态：标记集是；如果对某个q 和q ， 乩】 拥有g 尊矿，那么【卜包含口标记的从等价类万到石，的转换。 为了将可达性问题，r ) 简化为一个在的商的可达性问题，需要保证， 非稳定性的不能将目标状态和非目标状态等价。对于目标位置的一个集合 工，如果一旦( s ，v ) o ，v ) ，要么s 和s 都属于r ，要么s 和s 都不属于r ， 那么一个等价关系被称为r 一敏感的。 命题3 1 稳定商【7 1 设a 是一个时间自动机，是幽上的一个等价关系，l ，是 a 的一个位置集合，使得是稳定的，且r 一敏感的。那么l p 的一个位置是可 达的当且仅当存在一个等价关系，使得等价类玎在商 卜中是可达的，并且 石包含一个状态它的位置在矿中。 因此，为了解决可达性问题口，l 5 ) ，需要搜索一个稳定的、l 一敏感的， 且只含有有限多个等价类的等价关系。 3 2 域自动机 常整数限制 回忆一下时间自动机的定义，允许时钟约束中可以和有理常数比较。给出一 1 端于时间自动机的实时系统规范验证研究 个时间自动机a ，可以将a 中时间约束中出现的所有常数乘以它们分母的最小 公倍数，这种变换并不改变可达性问题的解。因此，我们可以限定时间自动机的 时钟约束只包括整数常量。注意在变换后的时间自动机中的最大常量由原来自动 机的常量的分母的积限定( 不会超过这个积) ，可知这个转换在时钟约束编码上引 起至多二次方的增大。 区域等价 如果一个自动机存在两个有同样位置的状态在所有的时钟值的整数部分一 致，且在小数部分的顺序一致，那么可以在这个自动机的状态空间上定义一个等 价关系，使这两个状态等价。时钟值的整数部分需要确定一个特殊时钟约束是否 被满足，但是小数部分的顺序用来决定哪一个时钟首先改变它的整数部分。例如， 如果两个时钟z 和y 在一个状态上的值在o 和1 之间，那么一个有时钟约束仅= 1 ) 的转换是否可以跟随一个有时钟约束0 ，= 1 ) 的转换，取决于时钟的当前值是否 满足0 9 ) 。时钟值的整数部分可以任意大，但是如果一个时钟x 从未和一个大于 c 的常数比较( 即与工比较的最大常量为c ) ，那么它的实际值一旦超过c ，就对决 定允许的转移没有任何影响了。 现在我们形式化这个概念。对任意6 e r ，p ) 表示d 的小数部分，p 1 表 示6 的整数部分；也就是，6 ；p 1 + 户( 6 ) 。对每个时钟x x ，设c 。是在一个不 变式或一个约束条件中出现的某时钟约束中与工相比较的最大的整数c 。 我们称等价关系e 为区域等价( r e 百o ne q u i v a l e n c e ) ，定义在x 的所有时钟解 释的集合上，对两个时钟解释y 和v ，vz v 当且仅当下面所有条件满足： 1 对于所有耳x ，要么p ) 1 和p ) i m m ，要么两者都大于q 。 2 对于所有x ，) ，x ，如果v o ) 5 c ，胃t v ( y ) sc ，那么步( v o ) ) s 步( v ( ) ，) ) 当且仅当f r ( v o ) ) sp ( v ( y ) ) 。 3 对于所有x x ，如果v o ) sc ；，那么p p o ) ) = 0 当且仅当o ) ) = 0 。 a 的一个时钟区域是一个s 关系下的关于时钟解释的等价类。用m 定义v 所 属的时钟域。每个时钟域由它能满足的所有时钟约束组成的集合唯一确定。例 如，考虑一个在两个时钟上的时钟解释，v g ) = 0 3 和v ) = o 7 ，【v 上的每个时钟 1 4 基于时间自动机的实时系统规范验证研究 解释满足约束( o q 9 1 ) ，且用【o x y 1 来表示这个域。 通过一个例子可以很好的理解等价类，考虑一个时间转换表，它有两个时钟 x 和y ，c = 2 且c 。= 1 ，时钟域如图3 1 所示。 12； 6 个点域： ( 0 ，1 ) 】、 ( 1 1 ) ，【( 1 0 ) 、【( 0 ，o ) 、【( 2 。1 ) 】、【( 2 ，0 ) 、 1 4 个开 旅线域： o x l ，户o l 【o x l ，f 1 、 1 x 2 ，尸o 】、 1 x 2 ，尸1 、 【o s 1 ，x = o 】、【0 9 1 x = 1 】、f 0 9 i ，x - - 2 、【0 z 可 1 、 1 2 ) 一0 】、d ， 1 ，x = 0 、陟 1 ，z = 1 、 y 1 ，x = 2 8 个开自殳域t o z 9 1 】、【0 9 嘲 u 【1 靠亨“ 1 】、 o x u 1 x 1 图3 1 时钟域 域的个数是有限的，并且对a 的各个时钟的约束舻，如果v e v7 ，那么v 满 足妒当且仅当v7 满足尹。一个时钟域满足一个时钟约束妒当且仅当时钟域中的每 个时钟解释满足妒。每个域可以表示如下 1 对每个时钟x ，时钟约束属于下面的集合 弘= c l c = o 工，吱) u c l x c ；) ， 2 对菜个c ，d ，使c - l z c 虽d - l y d 的每一对时钟工和y ，o ) 大于、等 于或者小于户o ，) 。 通过计算上面形式的等式的可能组合的个数，总结出时钟域的个数的上限是 2 。n 。( 2 c 。+ 2 ) ，其中k 是时钟的个数。那么时钟域的个数在时钟约束的编 码上是指数形式的。 域自动机 在时钟解释上的域等价关系s 被扩展到一个在状态空间上的等价关系，这要 求等价状态有同样的位置和域一等价时钟解释；( s ，v ) s o ，v ) 当且仅当s ：s 且 基于时间自动机的实时系统规范验证副f 究 vzv7 。域等价的关键性质是它的稳定性： 命题3 2 稳定性域等价s 是稳定的。 对稳定性进行直觉理解，让我们考虑一下图3 1 的域，属于相同域的两个状 态满足a 的同样的约束条件集，因此，如果从一个状态开始的转换是可能的， 那么从另一个状态开始的同样的转换也是可能的。在这个转换中某些时钟可能被 复位。x 设置为零的作用是在y 轴上的投影。注意，等价状态投影到等价状态。 现在考虑一个状态随着时间流逝的演化。随着时间的流逝，因为时钟x 和y 都以 同样的速度增加，状态沿着对角线向上移动。对一个给出的时钟域，在这样一个 转换中沿着对角线向上时遇到的域序列是相同的，和在域中选择哪一个状态是无 关的。 一个时间自动机关于域等价的商 u 。】a 被称为a 的域自动机，记为r ( a ) 。s 的等价类的个数是有限的，它是稳定的，且它是一敏感的，和磊标位置的选 择无关。可得出，为了解决可达性问题似，l 7 ) ，可以寻找有限域自动机r ( a ) 。 考虑图3 2 所示的时间自动机a 口。字母表是 a ，b ，c ，d ) 。相应的域自动机是 r ( a o ) ，如图3 3 所示，只有从初始状态c 如，p 。y = o 】，可达的域被给出，注意 c x = l ， c y = 1 。自动机的时间约束保证了从到如的转换永远不可能发生。具有 状态分量8 2 的可达域满足涉= l p l 】，且这个域没有出去的边，这样域自动机帮助 我们总结出一个b 标记的转换后不会有转换发生。 二i y i d 习 基于时问自动机的实时系统规范验证研究 3 3 带自动机 图3 3 域自动机r ( a o ) 重新考虑图3 3 的域自动机，初始域包括一个状态o 。，z = y = 0 ) ，且有三个 后继状态包含位置毛，相应的时钟域是【，= 0 q 1 】。个 策略是将这三个域叠加得到并集【y = o 。这个时钟域的凸并集被称为时钟带( c l o c k z o r l e s ) 。一个时钟带是一个时钟解释的集合，由约束的并集描述，这些约束在一 个时钟或不同的两个时钟上设立上限或下限。形式上时钟带的集合由下面的语法 产生 妒：= 工 c i 工sc i c 工l c c x l x - y c i x - - y s c i 妒1 妒2 对一个时钟带妒，满足妒的时钟解释的集合仍记为妒。如果a 有k 个时钟， 那么集合妒是一个在k 维欧几里德几何空间上的凸集。观察下边的时钟带的性质 1 每个时钟域是一个时钟带； 2 对一个时钟域万和一个时钟带妒，, r g 要么完全包含在妒中，要么和妒不 相交； 3 两个时钟带的交是时钟带； 4 位置的不变式和转换的约束条件中所用的每一个时钟约束是一个时钟带 ( 从1 到3 循环) ； 1 7 基于时间自动机的实时系统规范验证研究 5 对两个时钟带妒和妒，如果并集妒u 妒是凸的，那么它是一个时钟带。 由此可知时钟带的集合和域的凸并集的集合是一致的。 基于时钟带的可达性分析用下列三个带上的操作： 对两个时钟带妒和妒，两个带的交集是一个带，记为妒a 妒。 对一个时钟带妒，如果用妒n 表示时钟解释v + 6 的集合，v 妒且 6e r ，那么，妒”表示时钟解释的集合，这些时钟解释通过允许时 间从某个在舻中的时钟解释流逝得到，这个时钟带集合在这个操作下 封闭：对一个时钟带c p ，集合c pn 是时钟带。 对时钟的一个子集九和一个时钟带妒，设时钟带烈a ：= 0 】表示时钟解 释v z 1 0 】的集合，v e 伊，v z _ 0 】是一个时钟带。 对一个位置s 和一个时钟带妒，一个带是一个对偶( s ，妒) ，我们建立一个转 换系统，它的状态是带。考虑一个带( s ，妒) 和a 的一个转移e = ( s ，a ，妒，a ，s ) ，对 某个v 妒，状态o ，v ) 可以从状态0 ，v ) 使时间流逝和执行转移e 得到，用 s u c c ，e ) 表示这种时钟解释v 的集合。也就是说，集合( s ，s u c c ，p ) ) 表示在转 移e 下带0 ，妒) 的后继状态。为了得到集s u c c ，e ) ，( i ) 将妒和s 的不变式求交， ( i i ) 时间流逝用n ，( i i i ) f 汉$ ns 的不变式的交集，( i v ) 取和e 的约束条件妒的交集， ( v ) 将 中的时钟重置零。第一和第三步保证不变式在时间流逝过程中满足不变 式( 既然不变式是凸的，那么它可以确保从开始和结束状态满足不变式) ，那么 s u c c ，e ) ；“( 妒a ，o ) ) n ) i n v ( s ) a 妒) 【a - 0 】 这样，时钟带的关键性质是关于转移在后继下封闭。 命题3 3 带后继对时间自动机a 的一个时钟带舻和一个转移e ，时钟解释的集 合s u c c ，e ) 是一个时钟带。 一个带自动机通过在带0 ，妒) 和o ，s u c c ，p ) ) 之间增加边得到。对一个时问 基于时问自动机的实时系统规范验证研究 自动机a ，带自动机