随着计算机科学的发展，工业界越来越重视系统的正确性和可靠性，这样使得形式化的模型验证方法得到了广泛地应用。通过可达性分析，模型检测可以完成对实时系统的安全性和活性的验证。它的思想是搜索描述系统行为的转换系统，然后分析可达状态集合，从而确定系统是否满足规格说明。时间自动机是包含时间约束的有限状态转换系统，它是使用最为广泛的形式化验证方法之一。　　 在理论研究部分，首先分析了时间自动机的概念，然后给出了时间自动机的一些扩展形式。实时系统中的事件能否发生对应着时间自动机某个状态从初始状态开始能否可达，因此模型验证主要任务是状态可达性分析。验证需要采用了一些符号化的方法来描述状态，文中首先对时钟区域和时钟带两种方法进行了分析，然后介绍了可达性分析的两种主要的方法。我们重点介绍了基于二元决策图的模型验证方法，而使用它的前提是在时间自动机的整数语义下。详细地解释了如何把整数语义下的状态和转换关系表示成二元决策图的形式。我们给出了在这种数据结构下的可达性分析算法的改进，对该算法进行了时间复杂度分析，并结合一个具体的验证实例对空间复杂度进行了分析，表明改进后的算法的时间复杂度基本不变，同时又降低了可达性分析的空间复杂度。　　 在应用研究部分，首先是介绍了基于时间自动机的验证工具UPPAAL，然后是结合该工具给出了模型验证的步骤和建模的标准，最后构造了飞机着陆控制系统的时间自动机模型，检测了系统是否安全可靠，避免了系统运行时出现错误。通过使用验证工具UPPAAL，我们可以方便地为系统构造模型，有利于设计人员认清系统的运行过程，及时发现系统中存在的一些问题。