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

摘要：

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

关键词：同步数据流语言、经过验证的编译器、翻译确认、Lustre、Signal

所属期刊栏目：46

分类号：TP314(计算技术、计算机技术)

资助基金：国家民用飞机重大专项项目基金MJ-2015-D-066;核高基重大专项2017ZX01030-301-003

在线出版日期：2019-06-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：21-28