随着硬件和软件系统的规模和功能的迅速的增长，设计的复杂性和设计中所包含微小错误的可能性也随之增长，这就给软件和硬件产品的可靠性带来了重大的挑战。计算机辅助验证的目标在于提供验证工具，在产品设计的早期阶段帮助设计人员发现逻辑错误。当今，计算机辅助验证研究主要关注的是实时系统的建模，规约和分析。通常使用形式化语言描述系统的模型和规约，而分析由专门的验证工具进行。验证工具用所有可能的输入对模型穷尽式地仿真，判断模型是否满足规约，这称为模型检验。对于实时系统模型检验的研究已经取得了很好的成果。这些成果已经在工业界的设计开发过程中得到了很好的应用。当今象Lucent, IBM, Intel, Motorola和Siemens之类的半导体公司都在设计流程中应用形式化验证。而CAD工具生产商如Cadence和Synopsis都在探索添加验证功能到设计工具的方法。 时间自动机理论是实时系统模型检验中的一种有力的理论工具。时间自动机在思想上是稠密时间模型和ω-自动机的结合，它可以为实时系统在时问上的行为建模，在建模时引入有限的实值时钟来描述带有时间约束的状态转换。由于时钟取值可以是实数，时间自动机具有无穷状态空间。而模型检验要求系统的空间时有穷的。为了解决这个问题，引入了时钟取值region等价的概念。而time zone包含了更多的兼容的时钟取值，带有time zone的符号化状态合并了更多的时间自动机的具体状态，因此使用time zone的模型检验算法具有更好的效率。在对系统模型进行可达性分析时，实现算法的关键问题之一是存储time zone的数据结构──差额界限矩阵（DBM）。本文详细地介绍了在DBM上的一些操作，也介绍了两个基于时间自动机理论的验证工具──UPPAAL和Kronos。 时间自动机网络是多个时间自动机的并行组合，在模型检验中可用于并发实时系统的建模。网络中的每个时间自动机对应于实时系统中的一个主动组件或进程，它们之间通过同步信道或共享变量交互。时间自动机网络的状态中包含了共享变量的取值。如果两个状态的共享变量取值不同，那么这两个状态也不同。当共享变量的个数比较多，或者取值范围比较大的时候，共享变量就成为状态空间爆炸的重要原因之一。本文定义了在共享变量取值之间的兼容性关系，并提出了寻找符号化状态中共享变量取值所能兼容的取值的算法。随后本文还进一步对这种兼容性关系的检测进行增强，以更好地提高算法效率。算法找到的共享变量取值以一种紧凑的数据结构来记录。案例研究表明，这两种优化技术能显著地降低可达性分析对于存储空间的需求，因此它们是其它针对时间假设和约束的优化技术的一个有用的补充。