第二节介绍了
Uppaal
时间自动机和调度策略。在第
3
节中,两个对比
的调度算法,
即时上限优先协议
(
ICPP
)(没有共享变量)和
最早截止
日期优先
(
EDF
)(抢占式),每个都使用通用时间自动机定义。我们
证明了通用模型是正确的。例如,确保互斥(一次只能运行一个进程)
和优先级(当有一个更高优先级的进程准备就绪或被抢占时,任何进程
都不应该开始执行)。由于空间的原因,本文对
ICPP
调度进行了简化。
我们没有对任务通信进行建模,但在
[8]
中,我们演示了如何分析一组通
过 受 保 护 对 象 进 行 通 信 的 任 务 。 任 务 同 步 没 有 考 虑 , 因 为 我 们 以
Ravenscar profile [4]
为指导。第
4
节展示了自动机如何被实例化以分析一
个特定的程序:
Burns
和
Welling
第
5
节展示了如何使用
UPPAAL
规范来分
析性能属性。在第
6
节中,我们将讨论我们的工作,并解释如何在模型
中处理共享资源
2
时间自动机
从调度分析的角度来看,任务可以处于三种可能的状态之一:准备运
行,运行或等待。最初,每个任务都将处于就绪状态。在某些情况下,
它可以从就绪变为运行,然后如果被抢占,则从运行再次变为就绪,或
者一旦执行完成,则从运行变为等待。当由周期或事件触发时,任务从
等待状态返回到准备执行状态。这是模型的最一般形式。某些状态可能
与某些策略无关。例如,在循环调度和最早期限优先下,没有等待状
态,任务仅在运行和就绪状态之间交替。
调度算法
由控制状态之间的转换何时以及如何发生的规则定义为了对
任务进行建模以进行调度,因此,我们需要一种特定的语言,其中包含
由时间和数据约束控制的状态和转换。
时间自动机
语言
[1]
正好满足这些
要求。
时间自动机有许多版本。我们使用
UPPAAL
时间自动机模型
[11]
。
UPPAAL
版本是一个有限状态自动机,配备了实值时钟、整数值数据变
量和同步动作。转换对时钟和数据变量有保护和重置操作。在任何时
候,自动机都可以通过跟随转换来改变它的位置,只要当前的时钟和数
据变量满足使能保护。转变是瞬间发生的,时间只在特定的位置上流
逝。所有时钟的值随时间同步增加一个不变量与每个位置相关联,确定
该位置的有效时钟值自动机通过通道和共享变量相互同步。我们