实时系统是一类能够及时处理事务或执行计算并对外部环境做出响应的计算机系统，它不仅要求系统计算结果是正确的，而且要求结果产生的时间也是正确的。在这样的系统中，控制程序和外界环境经常会使用不同的时间度量，当用时间自动机对这样的系统建模，然后运用符号模型检测技术进行验证时，会产生严重的片段问题，造成验证速度下降，使得模型检测所需的时间和空间增加。精确加速技术可以有效地解决实时系统中由于不同的时间度量而出现的片段问题，它的关键技术在于向时间自动机添加了一个附加环，构造了加速模型，有效地加速了前向符号可达性分析，并且不改变时间自动机的可达性。由于这种技术能够有效解决片段问题，目前在模型检测可达性分析过程中得到了广泛应用。虽然加速技术在不断地发展进步，然而精确加速技术还是存在一些问题的，比如构造附加环的大小依赖可加速环窗口，这个条件限制了精确加速在实际中的应用。本文对精确加速原理进行了分析，提出了一种基于控制结构分析的精确加速方法。通过对时间自动机的控制结构进行静态分析，可以计算出覆盖状态集，把这些状态中的控制位置作为添加附加环的候选位置，在进行可达性分析时只存储覆盖状态，这种方法在加速的同时有效减少了状态空间。本文形式化地证明了这种方法的正确性和有效性。此外，在有些情况下，添加附加环之后带来的加速效果并不明显，在更极端的情况下，附加环的存在甚至会降低验证速度。为了实现有效的精确加速，本文对基于附加环的精确加速技术进行了分析，研究了其在不同条件下的加速效果，通过分析加速过程中的主要参数，推导出了有效加速所应满足的条件，进一步完善了精确加速技术。实验结果表明，这个判定条件在大多情况下可以准确地判断模型是否需要加速。