同步数据流语言在航空、高铁和核电等安全攸关领域得到了广泛的应用。其中基于一种类Lustre语言的Scade工具适合这些领域实时控制系统的建模和开发,这些语言编译器的安全性也受到了高度的关注。近些年基于形式化验证的方法实现可信编译器取得了很大的进展,如基于C语言的Compcert项目实现了产品级的可信编译器。清华大学L2C项目组也采用了这种形式化验证的方法开发了一个基于扩展的Lustre语言的可信编译器,该编译器以Lustre*作为源语言,以Compcert编译器使用的C语言子集Clight作为目标语言。因为Lustre*语言所编写的程序具有嵌套时钟的特性,所以对其静态检查的过程分为两个方面。一方面是在不考虑表达式和变量时钟的情况下对Lustre*的抽象语法树做传统的类型检查。另一方面是对抽象语法树进行时钟检查,即检查Lustre*程序中表达式和变量的时钟匹配与否。本文主要是对L2C编译器中静态检查的时钟检查进行介绍。本文介绍了以下工作——首先,定义了时钟演算规则,时钟演算规则指定了时钟检查器需要检查的内容;其次,通过Coq证明工具实现了L2C可信编译器的时钟检查器;最后,证明了能够通过时钟检查器的Lustre*程序一定是时钟良好的。