实时系统在军事和民用领域都有着广泛的应用，如何保证这类系统的安全性和可靠性是研究人员广泛关注的问题。模型检测方法是分析和验证实时系统的一种形式化验证方法，而时间自动机是模型检测方法的一个有效工具。时间自动机是对自动机理论的扩展，提供了形式化的方法来建立和分析实时系统的行为，在模型检测方面有着重要的应用。时间自动机已经成为计算机科学理论研究的一个热点。带自动机是经典时间自动机的一种有穷状态构造，它的状态是由时钟带和位置构成的偶对，因此如何有效的表示和操作时钟带是实现带自动机的一个关键问题。目前已经提出了几种有效的表示方法并应用于实践，如DBM、CDD等，DBM是应用比较广泛的一种数据结构。本文研究时间自动机理论及时钟带的表示和范式化，主要工作如下：首先，系统的分析时间自动机理论及其相关性质，介绍区域自动机和带自动机。其次，通过对时钟带DBM表示方式的分析，本文分离出一类时钟带，针对这类时钟带的特点，提出一种DBM的范式化算法。这种范式化算法相比经典的Floyd算法在时间性能上有较大的提高。基于这类时钟带范式化速度较快的特点，其存储空间也可以进行压缩，减少其空间消耗。理论证明及实验结果表明了这种方法的有效性。最后，本文在理论研究的基础上对一个铁路交叉口控制系统建模并验证其安全性和可靠性。