同步数据流语言可信编译器的构造

• 作者: 嵇智源 张煜承 张玲波 杨斐 王生原 王蕾 甘元科 石刚 董渊
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 同步数据流语言 经过验证的编译器 形式化验证 形式语义 定理证明
• 年，卷（期）: 2014,（2）
• 所属期刊栏目: 嵌入式系统软件设计方法与技术专刊
• 页码范围: 341-356
• 页数: 16页
• 分类号: TP314
• 字数: 12374字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004542

摘要

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发,综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.