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

康跃馨; 甘元科; 王生原

首页> 中文期刊> 《软件学报》 >同步数据流语言可信编译器Vélus与L2C的比较

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《软件学报》 |2019年第7期|2003-2017|共15页
作者
康跃馨; 甘元科; 王生原;
展开▼
作者单位

清华大学计算机科学与技术系;

北京 100084;

清华大学计算机科学与技术系;

北京 100084;

清华大学计算机科学与技术系;

北京 100084;

展开▼
原文格式 PDF
正文语种 chi
中图分类编译程序、解释程序;
关键词
同步数据流语言; 形式化验证的编译器; Lustre语言;

相似文献

中文文献
外文文献
专利

1. 同步数据流语言可信编译器的研究进展 [J] . 杨萍 ,王生原 . 计算机科学 . 2019,第005期
2. 同步数据流语言可信编译器的构造 [J] . 石刚 ,王生原 ,董渊 . 软件学报 . 2014,第002期
3. 可信编译器L2C的核心翻译步骤及其设计与实现 [J] . 尚书 ,甘元科 ,石刚 . 软件学报 . 2017,第005期
4. 同步数据流语言高阶运算消去的可信翻译∗ [J] . 刘洋 ,甘元科 ,王生原 . 软件学报 . 2015,第002期
5. 同步数据流语言时态消去的可信翻译 [J] . 张玲波 ,甘元科 ,石刚 . 计算机工程与设计 . 2014,第001期
6. Googlev8编译器在气象数据同步中的应用 [C] . 蔡由昌 ,周艳岳 . 第十三届泛珠三角区域气象学术论坛 . 2016
7. 基于即时编译器的Java语言同步优化研究 [A] . 史成荣 . 2009

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

摘要

著录项

相似文献

相关主题

期刊订阅