实时系统是一类需要在规定的时间内响应外部事件并完成对外部事件处理的系统，这类系统常见于与生命财产密切相关的领域，一旦这类系统出现设计上的缺陷，将会导致非常严重的后果，因此，如何保证实时系统的正确性和安全性成为人们日益关切的问题。模型检测是验证系统模型是否满足所期望性质的一种形式化方法，以其自动化的验证过程以及反例信息能对系统修正带来巨大帮助的特质获得了人们越来越多的青睐。在实时系统的模型检测中，时间自动机是一种被广泛使用的用来描述实时系统的数学模型，同时线性时序逻辑LTL也是一种非常常用的针对实时和并发系统的规范语言。　　 Echecker和CTAV是中科院软件所近年来相继开发的两款用来验证时间自动机LTL性质的模型检测工具，前者使用离散语义，生成的反例信息直观易懂，但由于要展开的状态空间较大，其检测效率较低;后者使用了连续语义下的符号化抽象技术，其检测效率较高，但由于其反例信息是抽象后的状态序列，失去了直观性。为了综合CTAV工具的高效性和离散语义下反例信息的直观性，本文提出了利用CTAV反例路径信息快速生成离散语义下反例路径的方法，并对实现该方法的工具DCFG进行了详细介绍，实验表明该方法具有预期的效果。　　 为了更好的利用反例信息帮助系统修正，使反例信息可被更直观地观察，本文实现了一个关于时间自动机的simulator工具，它可以图形化地显示各个进程的时间自动机模型，并且能模拟系统模型沿着反例路径的运行过程，因此可以有效利用离散语义下具体反例的直观性，为系统修正提供快捷有效、更加直观的反例信息，帮助提高系统的正确性及安全性。