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

• 作者: 康跃馨 王生原 甘元科
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 同步数据流语言 形式化验证的编译器 Lustre语言
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 2003-2017
• 页数: 15页
• 分类号: TP314
• 字数: 13432字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005755

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
2	甘元科	清华大学计算机科学与技术系	5	24	4.0	4.0
3	康跃馨	清华大学计算机科学与技术系	1	1	1.0	1.0