模型检测是自动化地验证系统行为满足给定性质的一种技术。它的基本做法是通过对系统所有可能的行为进行探索来证明系统满足给定的性质。模型检测面临“状态爆炸”问题，即系统的状态个数往往随系统的规模呈指数增加，验证规模较大的系统需要消耗大量的计算资源，从而使得很多验证任务在实际中很难完成。反例制导抽象精化技术是缓解状态爆炸的重要技术之一。这种技术通过生成比原系统简单的抽象模型，对抽象模型进行验证以得到原系统的性质。在验证过程中会按照需要对抽象模型进行精化，使之更逼近原系统，直到得到满意的结果为止。　　时间自动机是一种重要的实时系统模型，它的验证同样面临着状态爆炸问题。我们针对时间自动机的安全性验证进行研究，提出了两种验证方法。我们将近年来出现的迹抽象精化技术应用于时间自动机安全性验证中，以有限自动机作为时间自动机行为的上近似，利用时间自动机中基于zone的符号化技术和LU抽象技术来构建新的有限自动机，对已有的上近似进行精化。通过实例分析说明了该方法在某些情况下的优势。我们提出了时间自动机的差分约束抽象，并结合懒惰抽象提出了新的验证算法。与基于LU抽象的算法相比，基于差分约束抽象的算法能够更多地利用时间自动机结构中的信息进行更粗粒度的抽象。实例分析和实验表明该方法在某些情况下具有一定的优势。　　近年来，Horn子句和形式化验证的关系受到一些研究人员的关注，Horn子句可以作为形式化验证的中间语言。我们沿着这个思路，将模型检测中的迹抽象精化方法应用于Horn子句可解性中，提出了基于迹抽象精化的Horn子句可解性验证方法。我们利用树自动机来作为Horn子句可能的推导树的上近似，并利用树插值和约束求解器来构建新的树自动机，以对已有的上近似进行精化。我们实现了该算法，通过实验与其他方法进行了对比，并对实验结果进行了分析。