相较于单处理器的执行平台,多处理器的执行平台由于可以提供更强大的处理能力而正在被越来越广泛的应用到各类实时系统中。例如,越来越多的嵌入式系统使用多处理器的平台来执行实时的应用程序,而这些应用程序又被分割为一个个的实时任务在平台上执行。又如,在有些系统上,实时的任务在系统运行时生成,继而在有时间限制的条件下被执行,如一系列由事件触发的中断需要在它们的截止时间内可抢占的执行。多处理器的实时系统的设计是一件十分复杂工作,需要考虑众多的因素,如处理器的数目,处理器的类型和结构,任务的分配,操作系统的选择等等。由于在系统设计时各部分的选择(如以上提及的选择)具有一定的自由性,要设计一个正确的,有效的系统就成了一项不小的挑战。这需要设计者对各部分如何独立运作以及它们之间如何协同运作都要精心设计,这通常通过对系统进行建模来实现,而建模之后往往要对系统的正确性和有效性进行验证,由于各个系统的运行机制各不相同,要验证的系统属性常常不一样,但有一个重要的问题往往在系统设计时就需要解决,那就是确保系统中的任务能在它们的截止时间内执行完毕,这就是所谓的可调度性分析。目前存在着一些解决实时系统的可调度性分析问题的方法,如传统的可调度性测试方法,它基于处理器的利用上界(processor utilization bounds),如果测试值低于上界,则系统可调度,如果高于上界,则无法判断。任务自动机(task automata)是一类扩展了的时间自动机,它被专门用来进行可调度性分析。Times是一个基于任务自动机理论的工具,这个工具被用来在单处理器平台上面进行可调度性分析。尽管实时系统的可调度性分析已经有了众多方法,但是,目前没有一种通用且有效的方法适用于多处理器平台,也没有一种方法将系统的各个部分完整的指定,分层次的建模,并且整体的看待系统的可调度性分析和形式化验证。在这样的背景下,如何在时间自动机理论的基础上提出一种系统模型,这个模型能支持多处理器平台上的形式化的验证和模拟,并且支持系统的正确性分析,如可调度性,就是一个值得我们研究的问题。在这篇文章里,我们首先将一个典型的实时系统划分成以下几个模块:硬件环境,任务系统和多处理器的执行平台,然后,我们在模型校验工具Uppaal中用时间自动机对各个模块建模,用以刻画它们独立和交互的行为,这样,我们可以在一个统一的框架当中对系统进行形式化验证和可调度性分析。同时,我们在提出的模型中留下了可供设计者修改的接口,使得此模型具有一定的通用性和可伸缩性,设计者们可以根据现实的实时系统进行修改,以适应系统的具体要求。在对拥有较少数量的任务和处理器的系统建模和验证之后,结果表明,我们的建模方法是可适应和可扩展的,系统设计者可以利用它来为特定的系统进行设计和验证。