实时系统不仅要求逻辑上是正确的，而且要求时间上也是正确的，这类系统在设计阶段需要进行严格的分析和验证。时间自动机是使用最为广泛的对实时系统进行规范验证的形式化方法之一。 实时系统验证主要分为安全性验证和活性验证，系统的活性可以通过位置的不变式和转移的约束条件保证，验证也比较容易，本文对此不作过多讨论。安全性验证问题可归结为时间自动机的可达性分析，基于状态空间搜索的方法主要不足在于状态空间的大小随着过程数目的增加呈指数级递增，这就导致了状态空间爆炸问题。为了解决这个问题，我们必须构造时间自动机状态空间的有穷表示。 本文主要研究了Alur提出的域自动机方法、带自动机方法以及Inhye Kang等提出的状态空间最小化方法，并在此基础上提出了时间段转换系统以及对状态空间的极小化方法。该方法用位置和进入位置的最大最小时钟值集合来表示状态而得到时间段转换系统，同时通过转换分析保留有效转换来简化这个转换系统。对简化后的系统，使用转换互模拟进行最小化。文中对该方法进行了可行性分析，通过与其它方法进行比较阐述了该方法的优点和不足，并建立了铁路交叉口控制门系统的最小化过程。 在规范验证应用方面，本文研究了两种典型实时系统——道岔自动控制系统和自动筛选器系统。通过对系统进行分析和规范，给出了系统的时间自动机模型，并使用UPPAAL对模型进行验证，证明了系统的安全性、有效性和可控性。