基于时间自动机的调度算法动态分析及应用研究

143理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html15页基于一般时间自动机的调度行为分析Thorsten Gerdsmeier1，2和Rachel Cardell-Oliver3埃塞克斯大学计算机科学系科尔切斯特CO4 3SQ，英国摘要本文提出了一种对实时程序在不同调度算法下的行为进行动态、自动分析的方法。每个调度算法都由一个通用的时间自动机定义，它可以用特定任务集的数据来实例化。 由此产生的实例化时间自动机网络可以在模型检查器Uppaal中自动分析，以确保满足正确性。还可以计算各种调度度量。我们假设数据，如最坏情况下的执行时间，周期，截止日期和优先级已预先计算每个任务。在本文中，我们提出了通用规范的单处理器调度使用立即上限优先级协议（ICPP）和最早期限优先（EDF）算法，并分析了行为的矿井泵控制器在Ada95下实现的每种调度算法。1介绍为了分析程序，而不是规范，我们必须考虑如何在实现环境中调度它们的执行。自20世纪70年代以来，在特定的调度策略下分析给定任务集的可能调度问题一直是一个活跃的研究课题。速率单调分析[12]及其扩展提供了一组特定的周期性任务的可并行性的保守分析这样的预测是安全的（如果RMA预测任务是可调度的，那么它们在实现中将是可调度的），但可能是悲观的（RMA可能预测任务不能被调度，而实际上实现是可调度的）。RMA方法的一个主要优点是，将实参数代入1第一作者由埃塞克斯大学的奖项支持2电子邮件：gerdst@essex.ac.uk3电子邮件：cardr@essex.ac.uk2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-N D链接。格兹迈尔和卡德尔-奥利弗144公式，是它是相对便宜的应用。一个系统也可以通过实现它和测量任务执行时间来分析。执行的实现方法是昂贵的，因为一个系统必须实现之前，它可以被分析，总是有一个不确定性，是否最坏的情况下执行时间已被观察到。最近，一些作者考虑了自动的，动态的分析，探索所有可能的行为，一组任务在互动时，他们正在执行。这种方法保证了安全的估计，比速率单调分析更准确，但比实现和分析更便宜。几位作者[2，3，7，6]提出了调度分析的动态方法，使用时间自动机[1]对任务进行建模，并使用Uppaal和HyTech等模型检查工具进行分析。其中第一个是由Corbett [6]开发的。 这里有一个程序自动机是专为多任务程序设计的然后用模型检查器HyTech分析自动机。案例研究表明，程序自动机的位置的数量变得相当大。 布拉德利等人[3]展示了如何构建一个单一的时间自动机，它模拟了周期性任务和具有消息依赖性的任务的混合交互，在多个处理器上执行。Ericsson等人[7]考虑了由事件触发的具有固定执行时间和截止日期的任务调度在一个单一的处理器上。 在Braberman和Felder [2]中，过程通过为每个任务构建自动机来建模。延迟被添加到模型的任务的干扰。这些动态分析方法都有一个共同的缺点，即生成调度任务的时间自动机模型是复杂的，因此耗时且容易出错。我们试图通过引入通用自动机来表示特定调度策略下的典型任务的行为来降低成本。通用时间自动机是可以用参数实例化的时间自动机模板。程序语句被抽象为由在自动机位置上花费的时间表示的耗时动作。调度策略由控制自动机转换的守卫和同步来定义。 对于要分析的程序的每个任务，程序语句的定时、优先级、周期和截止日期作为参数传递给通用任务自动机。然后，可以使用模型检查器自动分析预定程序的属性，以探索其任务集的所有可能行为本文的主要贡献是展示了如何不同的调度策略可以方便地定义一般的时间自动机，这些一般的自动机可以用来分析不同的调度策略下的一组任务的属性我们专注于分析一组任务的预定行为的活动我们的动态分析方法的时间表使用时间自动机和模型检查，Uppaal。我们假设代码执行时间、任务周期、截止日期和任何触发事件的时间都是预先计算好的。格兹迈尔和卡德尔-奥利弗145第二节介绍了Uppaal时间自动机和调度策略。在第3节中，两个对比的调度算法，即时上限优先协议（ICPP）（没有共享变量）和最早截止日期优先（EDF）（抢占式），每个都使用通用时间自动机定义。我们证明了通用模型是正确的。例如，确保互斥（一次只能运行一个进程）和优先级（当有一个更高优先级的进程准备就绪或被抢占时，任何进程都不应该开始执行）。由于空间的原因，本文对ICPP调度进行了简化。我们没有对任务通信进行建模，但在[8]中，我们演示了如何分析一组通过受保护对象进行通信的任务。任务同步没有考虑，因为我们以Ravenscar profile [4]为指导。第4节展示了自动机如何被实例化以分析一个特定的程序：Burns和Welling第5节展示了如何使用UPPAAL规范来分析性能属性。在第6节中，我们将讨论我们的工作，并解释如何在模型中处理共享资源2时间自动机从调度分析的角度来看，任务可以处于三种可能的状态之一：准备运行，运行或等待。最初，每个任务都将处于就绪状态。在某些情况下，它可以从就绪变为运行，然后如果被抢占，则从运行再次变为就绪，或者一旦执行完成，则从运行变为等待。当由周期或事件触发时，任务从等待状态返回到准备执行状态。这是模型的最一般形式。某些状态可能与某些策略无关。例如，在循环调度和最早期限优先下，没有等待状态，任务仅在运行和就绪状态之间交替。调度算法由控制状态之间的转换何时以及如何发生的规则定义为了对任务进行建模以进行调度，因此，我们需要一种特定的语言，其中包含由时间和数据约束控制的状态和转换。时间自动机语言[1]正好满足这些要求。时间自动机有许多版本。我们使用UPPAAL时间自动机模型[11]。UPPAAL版本是一个有限状态自动机，配备了实值时钟、整数值数据变量和同步动作。转换对时钟和数据变量有保护和重置操作。在任何时候，自动机都可以通过跟随转换来改变它的位置，只要当前的时钟和数据变量满足使能保护。转变是瞬间发生的，时间只在特定的位置上流逝。所有时钟的值随时间同步增加一个不变量与每个位置相关联，确定该位置的有效时钟值自动机通过通道和共享变量相互同步。我们格兹迈尔和卡德尔-奥利弗146≤∗ −在UPPAAL中没有积分器，我们使用简单的整数变量。UPPAAL使用密集的时间模型，但在本文中报告的工作离散时间模型检查器也会做。Uppaal时间自动机控制位置变化的规则有三个不同的组成部分。三个规则组件中的任何一个都可以为空。保护对时钟值和全局变量值的约束，在该约束下进行转换。例如，mypri== 1，w mypri 2 1表示我的时钟的值为1，全局变量w的值至多为mypri2− 1。同步使得两个不同的任务在指定的信道上同步。 例如，同步信道用于确保诸如(i) 抢占任务从运行状态变为就绪状态，(ii) 具有较高优先级任务的任务从就绪状态变为运行状态同时发生赋 值 重 置 时 钟 变 量 并 更 新 全 局 变 量 。 例 如 ， mypri ： =0 ， w ：=w+mypri描述了将一个任务添加到等待任务集合中，并将任务的时钟设置为0，准备测量下一个在Uppaal [10]的最新版本中，自动机模板可以使用其任何常数、时钟、数据变量和同步通道的参数来定义。一个网络的自动机，然后可以构造instan- tiating参数化自动机与实际参数。过程参数可以包括数据变量数组[10]。3调度策略我们解释我们的方法，通过引入两个对比的调度策略：ICPP和EDF的通用模型。在这两种情况下，我们假设使用单个处理器。在ICPP调度中，我们假设任务具有固定的周期。任务开销，如上下文切换，进入和退出时间的保护操作，- tions，进入和退出时间处理延迟语句，定时器中断和重新调度时间包括在执行时间。 不考虑时钟抖动。3.1立即上限优先协议关于ICPP调度的介绍，读者可以参考[5，9]。为了安排ICPP下的任务，我们需要以下数据。对于每个任务：• 任务的优先级，对于优先级0... n我们通过mypri = 2 i定义优先级为i的任务的优先级。空闲任务的优先级为0。格兹迈尔和卡德尔-奥利弗147• 任务的周期，每次调用任务之间经过的时间• 每个任务的功能代码的最坏情况执行时间，以一定数量的原子操作给出。对于整个系统：• 系统时钟中断之间的间隔我们假设理想的时钟中断模型，其中时钟中断可以在任何时间发生，而不仅仅是在某些周期性时间。 一个处于就绪状态的任务可以立即开始，如果没有更高优先级的任务正在运行。• 对于原子动作的时间片，为了简单起见，在本文中我们将始终假设1个时间单位的连续性。此外，每个任务都被分配了一个本地时钟，一个测量其周期的时钟，以及一个跟踪已经执行了多少个原子动作或等效地已经执行了多少个功能代码的时间片的计数器。ICPP调度下典型任务TaskICPP的定义见图1。如果相应的任务准备好运行，则自动机TaskICPP处于位置就绪状态，如果任务正在执行，则自动机TaskICPP处于位置运行状态一个原子动作，如果任务在执行完成和下一次调用之间暂时不活动，则在位置等待。位置runwait是出于技术原因而引入的，它对应于实际程序的无状态。全局整数变量w总是等于不在位置wait中的所有任务的优先级之和。如果没有更高优先级的任务处于运行或就绪位置，则任务可以将其位置从就绪更改为运行。 这由守卫w =2*mypri-1检查。如果守卫被满足，任务就可以开始执行。我们假设一个单处理器架构，其中只有一个任务可以运行在同一时间。因此，对于一个任务开始执行另一个任务必须抢占或完成执行。这是通过同步动作变化来实现的，同步动作变化导致同时进行两个转换：每个参与任务一个。只有一个任务总是在执行，因为我们包括了一个空闲任务和程序任务。如果在位置运行中的任务还没有完成其原子操作的所有mymax，则如果所有较高优先级的任务都是不活动的，则可以重新进入运行，或者如果较高优先级的任务是活动的，则可以进入位置就绪。从位置就绪，一旦所有更高优先级的任务都变得不活动，任务就可以返回运行在任务完成所有mymax原子操作的执行后，它通过输入locationwait使自己处于非活动状态，直到它的周期再次触发任务，任务自动机返回到就绪状态，等待被调度再次运行。调度策略的验证我们现在可以检查我们定义的通用自动机是否正确，因为它们确保了单个处理器上ICPP调度的特性格兹迈尔和卡德尔-奥利弗148运行准备process TaskICPP（clock myclock;const mydelay，mypri，mymax）gc==1，mycountermymax，w=2*mypri-1gc：=0，mycounter：=mycounter+1w =2*mypri-1gc==1，gc =1，myclock=mydelay runw：=w-mypri改变！gc：=0mycountermymax，w>2*mypri-1mycounter：=mycounter+1运行就绪改变？gc==1，mycounter==mymax运行等待改变？ready myclock=mydelaymycock ==mydelayw：=w+mypri，mycock：=0，mycounter：=0等待myclock =mydelayprocess Idle（）改变？改变！w==0Fig. 1. 通用自动机在ICPP调度中的应用属性1：任何时候都只有一个任务在运行证明：设r为正在运行的任务数。a) 在初始状态下，只有空闲任务在运行，因此r= 1。b) 当一个任务开始运行时，另一个任务必须停止运行。当一个任务开始运行时，它必须采取准备就绪->运行的过渡。这些转变是同步的变化！.因此，另一个任务必须与变化同步进行转换？.这只可能在run-> runready和run -> runwait之后的runready -> ready和runwait -> wait的转换中发生。 如果一个任务从就绪状态进入运行状态，另一个任务必须停止运行-格兹迈尔和卡德尔-奥利弗149−≤−−≤∗ −≤−−∗−≥− ∗−≤−∗−宁，所以r：=r+11。对于所有其他跃迁，r不变。因此，我们总是要求r= 1最终证明属性2：如果任何具有更高优先级的任务处于位置就绪状态，则任何任务都不能进入运行状态。校样：我们假设优先级为2k的任务k是位置就绪时优先级最高的任务。假设具有较低优先级（j k）的任务j进入位置运行。任务j只能在转换ready ->run和run -> run时进入run。 这些转换仅在w2 2j 1时启用。无论何时任务k处于就绪或运行状态，k都在w的因此，如果任务k处于位置就绪状态：w >2 2J1，对于所有j k，因为：w2 k>=2 j+1>2 j+11个= 2个2J1. 因此，如果更高优先级的任务k处于位置就绪状态，则没有任务j可以进入run。最终证明属性3：对于n+1个任务0.. n永远为真：w2 n+11。校样：诱导基础病例：n=0任务级别0上的一个空闲任务和一个TaskICPP进程我们只在转换wait -> ready时增加w。从ready开始，没有跟踪等待，而不采取转换run ->runwait，其中我们将w减少相同的值。它遵循w≤20+1−1 = 1。诱导步骤情况：n -> n+1我们添加一个优先级为（n+1）的任务第0层的任务... n永远不能将w的值改变为大于2n+11的值，如我们所假设的。对于级别n+1上的任务，我们只在转换wait-> ready时增加w。在这个跃迁中，我们将w增加2 n+1。 从ready开始，如果不执行run->runwait转换并将w减少2n+1，则没有跟踪等待。它遵循这个过程，w的增加永远不会超过2 n+1。我们得出：w = 2 n+11+2 n+1= 2 n+21。最终证明属性4：具有最高优先级的任务永远不会被抢占。校样：具有最高优先级的任务，比如说2n，只能通过执行run -> runready和runready -> ready的转换来抢占。 这种转变只能采取，如果w >2 2n 1。但这是不可能的，因为从性质3总是w2 n+11。最终证明格兹迈尔和卡德尔-奥利弗150−3.2最早截止期优先为了在EDF下安排任务，我们需要关于每个任务的以下信息• 用于原子动作的时间片：时间片是1在本文给出的例子中，• 每个任务的功能代码的最坏情况和最好情况执行时间，以时间片的倍数给出• 完成每项任务的最后期限用于最早期限调度的通用自动机如图2所示任务自动机只有两个位置，运行和就绪，这些位置的含义与ICPP自动机相同。 我们假设每个任务都有一个固定的最后期限。最早期限调度的目的是确保没有任务超过它的最后期限。因此，对于一个具有最后期限maxwait和最大执行时间execmax的任务，myclock在位置ready中不应该超过maxwait。实际上，我们将该条件作为不变条件添加到就绪状态。应该如果一个特定的实例化不可验证，模型检查器Uppaal将警告用户出现了死锁在这种情况下，必须选择新的截止日期，直到任务集是可调度的添加不变量是安全的，因为它不会引入任何新的行为，除了可能的死锁。在每个时间片之后（即当时钟gc为1时），再次检查下一个任务正在运行。选择的任务必须是具有最近的截止日期的任务：即具有截止日期deadk和时钟ck的k，使得deadk ck在所有用户任务1到n上都是最小的。由于Uppaal中的数据表达式语言不允许直接计算该函数，因此我们引入了一个支持自动机Calculate，每当需要最早的截止日期计算时，任务自动机都会调用该如果mycounter在execmin和execmac的范围内，则mycounter和myclock被重置，并且位置就绪被输入。这对应于完成任务的执行。当可以进行这种转换时，mycounter的可能值的范围引入了一些不确定性。如果mycounter低于execmac，则mycounter增加1，并进入locationready。如果任务具有最早的截止日期，即earliest==myid，则可以从locationready转换为locationrun调度策略的验证我们在单个处理器上检查EDF的两个属性。属性1：从不运行多个用户任务校样：用户 任务在位 置运行时正 在运行。 最初 ，所 有任务都 已就位（r=0），S 0-go！- S2增加r：=r+1，留下r=1，则S2-calc？S1格兹迈尔和卡德尔-奥利弗151calc？走！S2S1S0c2 =c1+（d2-d1），c3 =c1+（d3-d1），c4 =c1+（d4-d1），c5 =c1+（d5-d1），c6=c1+（d6-d1）最早：=1c1 =c2+（d1-d2），c3 =c2+（d3-d2），c4 =c2+（d4-d2），c5 =c2+（d5-d2），c6 =c2+（d6-d2）最早：=2c1 =c3+（d1-d3），c2 =c3+（d2-d3），c4 =c3+（d4-d3），c5 =c3+（d5-d3），c6 =c3+（d6-d3）最早：=3c1 =c4+（d1-d4），c2 =c4+（d2-d4），c3 =c4+（d3-d4），c5 =c4+（d5-d4），c6 =c4+（d6-d4）最早：=4最早：=5process TaskEDF（const myid，execmin，execmax，maxwait;clock myclock;int mycounter）最早的==我的ID去？gc：=0，mycounter：=mycounter+1准备gc==1，运行gc =1myclock =maxwaitmycounter=execmax，mycounter>=execmincalc！myclock：=0，mycounter：=0gc==1，mycounterexecmax calc！processCalculate6（）c1 =c6+（d1-d6），c2 =c6+（d2-d6），c3 =c6+（d3-d6），c4 =c6+（d5-d6），c5 =c6+（d5-d6）最早：=6图二. EDF六任务格兹迈尔和卡德尔-奥利弗152⇔−减少r：=r-1在任何其他任务可以就绪之前离开r=0最终证明属性2：开始执行的任务具有最早的截止日期.校样：变量early等于i，如果任务i有最早的截止日期：= i i = min j（d j cj）。 (We调用任务jc j的myclock）。 用户任务只能开始运行，如果最早等于它的任务标识。最终证明4Ada95矿用泵程序我们现在可以分析特定调度策略的给定实现的行为。我们使用在Ada 95[9][第3章]中实现的Burns和Wellings的矿井泵程序来说明我们的方法。4.1使用ICPP调度的矿用泵矿井泵程序[9]由六个用户任务组成：甲烷监测器、空气监测器、CO监测器和安全监测器是周期性任务，高传感器和低传感器是零星任务。作为速率单调分析中的标准，两个偶发过程，高传感器和低传感器表示为：[9]一个周期性的过程。分析此程序所需的任务数据，时间单位为100微秒，已在表1中再现的[9]中预先计算。低传感器和高传感器的零星任务周期从原来的10000减少到1000。这是悲观但安全的，并减少了模型检查的计算时间。时钟中断每50个时间单位发生一次。然而，在下文中，我们假设理想的时钟中断：进程可以在任何整数时间被中断或开始。每个任务的WCET都是C1。WCET加上上下文切换（由环境进行）是C2，我们将此时间用作调度分析的任务执行时间。每个任务的执行时间包括两次上下文切换。C1和C2包括在受保护对象上花费的时间。最后期限是计算任务必须完成的时间在Uppaal中，完整的规范由图1所示的通用自动机以及以下声明给出。时钟c1，c2，c3，c4，c5，c6，gc; int [0，63]w：=0;紧急变化;Methane_Monitor：=TaskICPP（c1，200，32，58）;Air_Monitor：=TaskICPP（c2，300，16，37）;格兹迈尔和卡德尔-奥利弗153任务名称优先期间C1C2截止日期甲烷监测仪322005458100空中监视器163003337200CO监测仪83003337200安全防护43503539300低传感器210002933750高传感器1100029331000表1Ada95矿用泵项目CO_Monitor：=TaskICPP（c3，300，8，37）;Safety_List：=TaskICPP（c4，350，4，39）;Low_Sensor：=TaskICPP（c5，1000，2，33）;High_Sensor：=TaskICPP（c6，1000，1，33）;系统甲烷监测器、空气监测器、一氧化碳监测器、安全监测器、高传感器、低传感器、空闲;4.2采用EDF调度的矿用泵与EDF调度相关的任务参数如表2所示。由于我们没有最佳情况执行时间的数据，因此我们对两者都使用了WCET。我们选择了[9]中公布的EDF截止日期。任务名称taskID执行截止日期甲烷监测仪158200空中监视器237250CO监测仪337300安全防护439350低传感器533800高传感器6331000表2Ada95矿用泵项目的EDF调度数据在Uppaal中，完整的规范由图2的自动机以及下面的系统信息给出。和前面一样，我们假设理想的时钟中断可以在任何时候发生const d1 200;格兹迈尔和卡德尔-奥利弗154const d2 250;const d3 300;const d4 350;const d5 800;const d6 1000;clock c1，c2，c3，c4，c5，c6，gc;int earliest，mycount1，mycount2，mycount3，mycount4，mycount5，mycount5;chancalc，go;Methane_Monitor：=TaskEDF（1，58，58，d1，c1）; Air_Monitor：=TaskEDF（2，37，37，d2，c2）;CoMonitor：=TaskEDF（3，37，37，d3，c3）;Safety_Qs：=TaskEDF（4，39，39，d4，c4）;HighSensor：=TaskEDF（5，33，33，d5，c5）;LowSensor：=TaskEDF（6，33，33，d6，c6）;系统甲烷监测器，空气监测器，CO监测器，安全监测器，高传感器，低传感器，计算6;5调度分析在第3节中，我们使用归纳推理证明了ICPP和EDF调度的通用规范的正确性。在本节中，我们将演示如何使用模型检查来分析特定调度策略下给定任务集的性能。一组任务是可调度的，除非违反了最后期限约束。这些可扩展性的约束被表述为通用规范的状态不变量。Uppaal模型检查器将期限冲突标记为死锁，如果没有标记死锁，则任务集是可调度的。已在Uppaal检查了表1和表2参数的矿用泵程序，以分别符合ICPP和EDF的要求我们可以使用任务时钟来导出某些性能界限。一个任务的响应时间是从任务第一次准备就绪到完成执行所花费的时间。ICPP调度的最坏情况响应时间可以通过为每个TaskX选择R来找到，使得：A[]（TaskX.runwait）暗示mycock<= R-1失败 A[]（TaskX.runwait）暗示mycock<= R成功ICPP调度的最佳情况响应时间可以类似地通过选择S来找到，使得A[] TaskX.runwait imply mycock>= S+1失败 A[]TaskX.runwait imply mycock>= S成功格兹迈尔和卡德尔-奥利弗155EDF下调度的任务的最大等待时间可以类似地找到：A[]（TaskX.ready implement myclock = W-1）失败A[]（TaskX.ready implement myclock = W）成功在ICPP下的矿用泵响应时间分析结果和EDF在表3和表4中给出。可以看出，所有任务都满足其dealines。在矿用泵的例子中，关于响应时间的知识为我们提供了关于测量的传感器数据的年龄的信息任务名称最佳情况响应最差情况响应任务响应截止日期甲烷监测仪5859100空中监视器3796200CO监测仪74133200安全防护39172300低传感器91263750高传感器1242951000表3ICPP响应时间任务名称最大等待观察到任务截止日期甲烷监测仪201200空中监视器203250CO监测仪298300安全防护335350低传感器769800高传感器9591000表4EDF响应时间6讨论我们已经介绍了通用的时间自动机分析ICPP和EDF调度策略。自动机可以用参数格兹迈尔和卡德尔-奥利弗156例如表征被分析程序的WCET。我们已经通过使用公布的截止日期和WCET分析Ada95矿井泵程序来演示该技术。我们没有使用共享资源。在[8]中，我们假设一个基于Ravenscar [4]的调度器，其中任务通信可以通过受保护的对象而不是通过rendevous：本文介绍的模型扩展了受保护的对象。我们建议每一个受保护的对象是由一个自动机建模。任务通过 与 相 应 的 自 动 机 同 步 来 调 用 受 保 护 对 象 。 当 自 动 机 TaskEDF 或TaskICPP的mycounter的值具有某些值（调用受保护对象的时间）时我们的模型主要是确定性的，因此状态空间不会迅速爆炸。我们使用具有800 Mhz和768 MB RAM的Pentium III进行分析。 表3和表4的要求已在小于每人一分钟。[8]中的模型检查相同的要求也需要不到一分钟的时间。 如果我们改变两个LowSensor的周期，和HighSensor从1000到10000，检查每个要求大约需要一个小时。然而，我们可以使用几种技术来减少状态空间，从而减少模型检查时间。在我们的例子中，我们假设理想时钟每毫秒检查一次。 这是理想的，但不现实。 在实际系统中，可以预期每10毫秒进行一次检查。 这种粗糙的时间颗粒在我们的例子中，所有的时间都除以10。其次，我们可以结合我们的模型与调度理论，通过计算一些任务的响应时间与功能分析和整合这些结果在我们的模型。减少状态空间的第三种方法是使用谐波值（具有公因子的周期）作为任务的延迟时间，如Corbett和Bradley等人所做的。[6，3]。在本文中，我们分析了任务响应时间的矿井水泵计划。类似的技术可以用于检查调度任务的进一步属性。矿用泵项目的两个典型要求是• 当水位高时打开泵有100毫秒的界限• 甲烷值读数高后紧急关闭30毫秒。为了验证这些属性，首先确定感兴趣的起点和终点（点可能在不同的任务中），引入一个新的时钟，在离开起点时重置时钟，并检查当我们到达终点时时钟是否始终低于其所需的最大值。 其他性质 因为可以类似地确定调度长度和任务被中断的频率。最后，对于不同的调度算法，用新的通用时间自动机规范进行实验将是有趣的。格兹迈尔和卡德尔-奥利弗157引用[1] 巴尔河和D. L. Dill，A theory of timed IO automata，Theoretical ComputerScience126（1994），pp. 183-235[2] Braberman，VA。和M. 实时设计的验证：结合调度理论和自动形式验证，在：O。Nierstrasz和M. Lemoine，编辑，Software Engineering-ESEC/FSE494-510[3] 布拉德利，S.，W. Henderson和D. 应用时间自动机进行分布式实时系统的响 应 时 间 分 析 。 H. Frigeri ， W. A. Halang 和 S. H. Son ， editors ， 24thIFAC/IFIP Workshop on Real-Time Programming WRTP143比148[4] Burns，A.，B. Dobbing和G. Romanski，Ravenscar tasking profile for highintegrity real time programs ， in ： Reliable Software Technologies-Ada-Europe263-275。[5] Burns，A.和A.Wellings，[6] Corbett ， J.C. ， Ada 任 务 程 序 的 时 序 分 析 ， IEEE 软 件 工 程 学 报 22（1996），pp. 1-23号。[7] Ericsson，C.，A. Wall和W.李明，以时间自动机作为事件驱动系统的任务模型，载于：RTSCA99（1999）.[8] Gerdsmeier，T.和R. Cardell-Oliver，时间自动机保护对象的调度行为分析，技术报告CSM-339，计算机科学系，埃塞克斯大学（2000年10月）。[9] 约瑟夫，M.，编辑，[10] Larsen，K.G. 和p.Pettersson，Uppaal2k，Newsletter 10，BRICS（1999）.[11] Larsen，K. G.，Pettersson和W. Yi，UPPAALin a Nutshell，Int. Journal onSoftware Tools for Technology Transfer1（1997），pp. 134-152。[12] Liu，C. L.和J.Layland，在硬实时环境中多道程序设计的调度算法。ACM20（1973年），第20页。46比61