凭借着高性能、低功耗的特点,多核处理器在嵌入式实时系统中的应用越来越广泛。然而,由多核实时系统造成的一个最大问题是人们无法对此系统的时间属性做出比较精确的预测。在多核系统中,访存总线通常作为一个非常重要的共享资源。通过共享访存总线,多核系统中的处理器核心可以对主存进行访问。但是多个处理核心对共享总线并行访问时会产生冲突,从而导致访存延迟时间难以预测。基于这一背景,本文主要研究的内容是通过模型检测技术来分析共享总线对多核实时系统WCET的影响。本文所研究的多核系统模型是每个处理器核心都拥有一个私有的Cache,并且这些处理器核心可以通过共享访存总线来对主存进行访问。本文首先利用基于抽象解释技术的Cache分析方法来对此系统中指令Cache的行为进行分析,从而可以得到运行在每个处理器核心上的程序指令在Cache中是否命中的信息。根据这些信启、,本文采用模型检测器UPPAAL来对程序的执行过程进行时间自动机建模。这些程序时间自动机模型能够准确地模拟出程序在执行过程中访问总线的时间行为。在本文中,共享总线的行为也通过时间自动机进行建模。最后,通过运行UPPAAL对由上述时间自动机模型构成的多核系统模型进行检测,从而可以得到程序WCET值。基于上述WCET分析技术,本文设计并实现了一个能够对基于共享总线的多核实时系统WCET进行分析的工具,此WCET分析工具能够自动生成程序时间自动机模型和总线时间自动机模型,并自动分析出程序WCET值。通过此WCET分析工具,本文分别对基于TDMA总线和FCFS总线的多核实时系统进行了WCET分析实验,并得到了相应的实验结果。这些实验结果表明与假设最坏访存延迟时间相比,本文所提出的WCET分析方法对于TDMA总线和FCFS总线的分析精度可以分别最高提高240%和82%。