实时系统是一种带有时间约束的计算系统，这些系统的许多动作的完成是与时间相关的，即要满足一定的时间限制。为了确保实时系统的正确性和可靠性，需要对其进行严格的分析和验证。实时系统的验证不仅要求逻辑上是正确的，而且要求时间上也是正确的。现在网络协议的复杂性日益增加。协议中的每一处错误和缺陷都将给网络系统的稳定性、可靠性等带来巨大的危害。协议的验证中往往也需要验证一些时间性质。 对实时系统和协议通常采用形式化的方法来进行验证。有限自动机是最为重要的一种形式描述与验证技术，它是很多形式化方法的基础。它直观性强，可实现与其它形式化方法的组合和转换。但是由于其没有清楚的时间的概念，只能处理事件的序列，而不能准确地描述事件发生的时间，因此在模型验证上的应用受到很大的限制。为解决这个问题，R．Alur等人提出了时间自动机模型。时间自动机存有穷自动机的基础上加入了时钟变量，通过时钟变量和时钟值的比较来约束状态的转移，因此时间自动机可以准确地描述带有时间的系统。 时间自动机的状态空间的大小随着问题规模的增大呈指数级递增。当系统规模较大时，基于时间自动机的验证就会变得非常复杂。所以需要对时间自动机的模型验证方法进行优化。 本文主要研究了域自动机方法、带自动机方法以及基于历史等价和转换互模拟的最小化方法。文中对时钟域及其上的操作给出了一种符号化的表示方法，从而便于域自动机在实际操作中的实现。本文还提出了基于状态转移时间关系的优化方法。该方法通过计算状态转移的最早可能发生时间和最晚可能发生时间来判断转移是否是有效的，通过保留有效转移来简化转换系统。 基于时间自动机已经开发出了多种自动验证工具。这些工具已经在实时系统和协议验证中得到了广泛应用。本文使用Kronos验证了FDDI协议来说明了基于时间自动机的验证过程。