实时系统在国防、金融、电信、航空等重要应用领域中发挥了至关重要的作用,近年来实时系统大量用于我们的日常与工业生产。实时系统不仅要保证逻辑正确性,还要保证时间正确性。可调度性分析是用于验证实时系统在某个调度策略下所有的任务是否能在其相对截止期内完成的一个方法。因此,在实时系统的开发和分析过程中,可调度性是重要的问题之一。在形式化验证领域,时间自动机(timed automata(TAs))通常被用于建模实时系统。90年代末期,Elena Fersman等人拓展了时间自动机提出任务自动机(task automta),基于此模型进行可调度性分析。与一般的可调度性分析方法类似,基于任务自动机的可调度性分析方法中,任务被抽象成相对截止时间(relative deadline),最好执行时间(best-case execution time(BCET))和最差执行时间(worst-case execution time(WCET))。获知最差执行时间是实时系统调度及很多可调度性分析方法的前提,然而在实际情况下,任务通常很复杂,导致最差执行时间很难预估。就算将复杂任务抽象成形式化模型,比如时间自动机,依然很难计算出每个任务的最差执行时间。就算得到最差执行时间,通常都是在实际情况下永远不可能达到的一个值,是一种悲观预估。基于这样的困难,本文拓展了任务自动机,提出了一个称为时间正则任务自动机(timed regular task automata(TRTAs))的模型对实时任务系统进行建模。由于时间正则任务自动机本质上是一个时间自动机,因此可以控制任务到达的行为。在时间正则任务自动机中,状态可以关联一个任务,每个任务被抽象成一个时间自动机、相对截止时间以及任务的状态。其中时间自动机用于描述任务的行为,任务的状态可以是触发、运行、被抢占等。因此,该模型支持可抢占的调度策略。时间正则任务自动机模型有较强的表达能力,可以对很多复杂的实时系统进行建模。基于时间正则任务自动机,本文提出了一个不需要最差执行时间的可调度性分析方法。我们对每个时间自动机做测试,得到每个时间自动机的运行时间,作为最差执行时间的下逼近时间。由于每个可调度的任务系统,其任务队列都是有界的,根据上述每个时间自动机的运行时间和任务的相对截止时间,可以得到任务队列长度的上界。如果超过上界,则立即可以判断该系统不可调度。如果不超过上界,则需要进一步研究。进一步地,我们将可调度性问题编码到嵌套时间自动机的可达性问题,嵌套时间自动机的可达性问题已被证明是可判定的,因此,可以证明本文提出的可调度性分析方法是可判定的。