同步数据流语言可信编译器的研究进展

• 作者: 杨萍 王生原
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 同步数据流语言 经过验证的编译器 翻译确认 Lustre Signal
• 年，卷（期）: 2019,（5）
• 所属期刊栏目: 综述
• 页码范围: 21-28
• 页数: 8页
• 分类号: TP314
• 字数: 9178字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2019.05.003

摘要

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注.同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade).构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等.近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点.文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
2	杨萍	北京语言大学信息科学学院	5	10	3.0	3.0