实时系统是指带有时间约束的并发反应系统，多数情况下它们是作为子系统嵌入在一个较大的系统之中，负责对外部事件的响应和处理，而且这些响应和处理要在一定的时限内完成。由于外部事件的随机性和不确定性，致使测试和仿真等传统手段很难完全发现系统在功能以及在时序和时限等方面存在的潜在缺陷。而实时系统又大量用在航空、航天、金融及生产过程控制、调度等对安全性有较高要求的领域，故使用有效的形式化分析和验证工具对提高实时系统的可靠性至关重要。 模型检测（model checking）是实时系统的分析与验证领域内最重要的形式化技术，它使用算法方法穷举搜索系统的状态空间以找出系统可能存在的缺陷，从而提高系统的可靠性。十多年来，实时系统的模型检测技术得到快速发展，所能分析和验证的系统规模有了很大的提高，已在协议分析、实时调度算法分析等多方面取得成功，并被工业界和学术界普遍重视。 现今实时系统领域最主要的模型检测工具是Uppaal，由瑞典Uppsala大学和丹麦Aalborg大学联合研制，在国际上得到广泛使用。Uppaal使用时间自动机（Timed automata）模型表示实时系统，可以验证实时系统的可达性、有界响应性等安全性性质，但不能验证实时系统的公平性等活性性质。为此我们开发了实时系统的一个基于线性时序逻辑LTL的模型检测工具CTAV，它既能验证实时系统的安全性，又能验证实时系统的活性。 线性时序逻辑LTL是已故图灵奖得主Pnueli教授提出的一个针对并发反应系统的性质描述语言，它直观易用，表达能力强，可表示可达性、安全性、公平性、活性等众多类型的性质，得到了广泛地使用，现有的关于硬件系统的性质描述语言的IEEE工业标准PSL和SVA都是基于LTL的。 CTAV使用时间自动机模型表示实时系统(与Uppaal相同)，使用LTL公式和带时间约束的LTL公式表示实时系统的性质（与Uppaal不同，Uppaal使用分支时序逻辑CTL表示系统性质）。CTAV可验证实时系统众多类型的、可使用LTL公式或带时间约束LTL公式表示的性质，如可达性、安全性、（有界）响应性、公平性、活性、non-Zeno性等等，是国际上目前唯一的可直接对时间自动机的LTL性质及带时间约束LTL性质进行模型检测的工具。