同步数据流语言可信编译器Vélus与L2C的比较

来源：软件学报杂志2019年第7期北京时间：

作者：康跃馨,甘元科,王生原

单位：康跃馨，清华大学 计算机科学与技术系, 北京 10008411,甘元科，清华大学 计算机科学与技术系, 北京 10008402,王生原，清华大学 计算机科学与技术系, 北京 10008403

摘要：同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如，适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具，特别是编译器的安全性问题也自然受到高度关注.近年来，基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一，也取得了瞩目的成果，如CompCert项目实现了产品级的可信C编译器.同样，人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目，二者均研发面向基于Lustre的同步数据流语言编译器，分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.

关键词：同步数据流语言;形式化验证的编译器;Lustre语言

基金资助：国家科技重大专项（MJ-2015-D-066）