实时系统时间验证主要包括可调度性分析和最坏情况执行时间(WCET)分析。其中WCET分析的目的是计算实时任务在最坏情况下的执行时间,其结果是可调度性分析的重要输入。在硬实时系统中,为保证分析结果的安全性,通常采用静态方法分析程序的WCET。静态分析主要包括处理器行为分析、程序流分析和WCET计算三个子任务。目前在WCET计算技术方面,隐式路径枚举技术是主导技术,但是该技术的主要问题是描述复杂程序控制流程信息的能力很有限,进而也限制了处理器行为分析所能采用的技术。在处理器行为分析方面,Cache分析一直是一个难度较大的任务。目前基于抽象解释技术的分析方法在分析LRU替换策略中占有主导地位,但是对于基于FIFO等其他替换策略的Cache行为的分析尚不成熟。随着处理器体系结构向多核发展,共享Cache成为了主要的设计趋势之一。不同核心上的程序在共享Cache中相互干涉,给Cache分析带来了极大的挑战。此外,随着WCET分析技术的不断发展,相关技术在实际系统中的可用性问题也逐渐受到越来越多的关注。基于上述研究现状,本文针对WCET静态分析中的WCET计算、单核与多核Cache行为分析、实时操作系统WCET分析等课题进行了深入研究。主要工作包括如下几点：(1)提出了一种全新的基于模型检测技术的WCET计算方法,设计了从程序到对应自动机模型的转换语义。该方法作为静态WCET分析的基础性框架,充分利用了模型检测技术搜索最优解的能力,使得分析结果具有更高的精度。探索了采用不同工作原理的模型检测器用于WCET计算的时间可伸缩性和空间可伸缩性,给出了基于模型检测技术的WCET计算方法的适用范围。(2)提出了一种基于剪枝思想的单核系统Cache分析方法。在基于模型检测技术的WCET计算框架的基础上,研究了利用这一技术对单核系统中采用FIFO替换策略的Cache进行分析的方法。针对模型检测技术在WCET分析中可能出现的状态空间爆炸问题,提出了基于剪枝思想的分析方法。该方法通过削减程序模型中符合特定条件的程序分支,能够在不损失分析精度的前提下,有效提高分析的性能以及可伸缩性。(3)提出了一种面向多核共享Cache的处理器行为分析方法。分析多核系统的共享Cache,关键在于对程序间的干涉情况进行精确的分析。现有的方法在分析这一问题的过程中只考虑了不同核心上的程序在地址上的冲突情况,导致分析结果的过度估计过高。本文采用模型检测技术对多核共享Cache的行为进行建模,模型能够在更细的粒度上挖掘冲突发生的时间关系,从而大大提高了分析的精确性。(4)对工业界广泛使用的μC/OS-Ⅱ实时操作系统进行了WCET分析。实时操作系统以控制密集型代码为主,其代码结构和时间行为特性与普通应用程序有很大区别。本文对μC/OS-Ⅱ实时操作系统的系统调用和禁止中断区间进行了静态WCET分析,详细分析了传统技术在分析实时操作系统代码时的精度以及尚存在的主要问题。同时,实验结果本身就是对μC/OS-Ⅱ实时操作系统实时特性的一个完整的量化描述,它对于使用者了解该系统的时间特性,以及对于系统开发者改善系统的实时性能都具有重要的应用价值。(5)本文在新加坡国立大学开发的Chronos工具的基础上,设计并实现了一个支持多核体系结构的静态WCET分析工具,实现了本文所提出的基于模型检测技术的WCET计算方法、基于FIFO替换算法的单核Cache行为分析、面向多核共享Cache的处理器行为分析、实时操作系统WCET分析等具体技术和方法,并验证了这些方法的正确性和有效性。总之,本文研究了采用模型检测技术进行静态WCET分析的问题,实验表明采用这种技术能够有效的提高静态分析的精确性。同时还探讨了采用静态WCET分析方法分析实时操作系统的可行性及主要问题。本文的研究对于静态WCET分析以及WCET分析可用性等领域的研究具有一定的参考价值。