随着实时系统应用的不断扩大,对实时系统的研究越来越受到关注。实时系统与一般系统的差别在于,实时系统的运算正确性不仅依赖运算结果的正确,还依赖于运算结束时间。实时系统能够在指定或者确定的时间内完成系统功能和外部或内部、同步或异步时间做出响应的系统。在传统概念上,实时系统分为硬实时系统和软实时系统。在硬实时系统中,若一项操作在截止时间之后才完成,那么运算结果就被认为是无用的,更进一步地说,这项错过截止时间的操作可能会导致整个系统的失败。而软实时系统却可以容忍这样的延迟,但是却会降低服务质量。在可调度性分析中,我们主要关心的是硬实时系统。可调度性分析在实时系统的设计中占有重要位置。任务是否可调度决定了该实时系统是否可以应用在实际中。早期的实时系统功能简单,如单板机、单片机,以及简单的嵌入式实时系统等,其调度过程也相对简单。随着实时系统应用范围的不断扩大,系统复杂性不断提高,实时系统具备了一些新的特点,比如多核处理器的引入。近年来模型检测的方法成功地应用于可调度分析研究中。基于时序自动机衍生出的各式自动机具有较强的表达能力,可以很好地刻画出时间这个在实时系统中最重要的维度。其中任务自动机扩展了时序自动机,引入了由时间事件触发的计算任务,适用于为任务发生时间无规律的实时系统建模。如果存在一种调度策略使得这个任务自动机所能产生的一系列任务都能调度成功,即它们能在截止时间前完成,则这个任务自动机是能调度的。实时系统上的调度策略可以分为不可抢占式调度与抢占式调度两种。本文将讨论基于任务自动机的多核系统的可调性分析,提出这两类调度策略的建模方法及其相应模型的分析。