项目简介：实时系统是指带有时间约束的并发反应系统，多数情况下它们是作为子系统嵌入在一个较大的系统之中，负责对外部事件的响应和处理，而且这些响应和处理要在一定的时限内完成。由于外部事件的随机性和不确定性，致使测试和仿真等传统手段很难完全发现系统在功能以及在时序和时限等方面存在的潜在缺陷。而实时系统又大量用在航空、航天、金融及生产过程控制、调度等对安全性有较高要求的领域，故使用有效的形式化分析和验证工具对提高实时系统的可靠性至关重要。 模型检测（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性质进行模型检测的工具。

产品性能：由于实数时间的稠密性和无穷性，实时系统基于时间自动机模型的模型检测工具基本都采取了基于zone的符号化方法，其影响工具效率的关键是基于zone的抽象方法的使用，不同的抽象得到不同大小的状态空间。由丹麦Aalborg大学计算机科学家(丹麦科学院院士)Kim Larsen等人于2004年提出的LU－抽象是至今已知的一个最为有效的基于zone的抽象方法，他们证明了LU－抽象保持时间自动机的可达性，即LU－抽象可用于时间自动机的可达性分析（已在Uppaal工具中使用）。2006年Tripakis提出了一个开问题：“LU－抽象是否保持时间Büchi自动机的空性”, 即LU－抽象是否可用于时间自动机的LTL性质和活性的模型检测直到2009年我们在《Formal Modeling and Analysis of Timed Systems》国际会议上给出了这个问题一个肯定的回答，同时使用LU－抽象实现了时间自动机关于LTL性质的模型检测工具CTAV。 由于CTAV使用了高效的基于zone的符号化抽象技术LU-抽象，因而具有较高的验证效率。我们已经使用CTAV对文献中众多的应用实例（如Gear box controller、FDDI协议、CSMA/CD协议等）进行了验证，CTAV可以在30分钟内对10多个进程的FDDI协议和CSMA协议等进行整个状态空间的穷尽搜索。 CTAV现可运行于Linux和Windows操作系统之上，并有基于eclipse图形编辑框架（GEF）的图形化建模界面。 CTAV得到了Uppaal工具的主要提出者之一、丹麦科学院院士Kim Larsen教授的肯定，他在2010年4月邀请CTAV提出者对丹麦Aalborg大学嵌入式软件系统中心进行了访问并作了介绍CTAV的学术报告和工具演示。

应用行业：电子与信息

专利情况： 已有专利2个