主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
石刚,王生原,董渊,嵇智源,甘元科,张玲波,张煜承,王蕾,杨斐.同步数据流语言可信编译器的构造.软件学报,2014,25(2):341-356
同步数据流语言可信编译器的构造
Construction for the Trustworthy Compiler of a Synchronous Data-Flow Language
投稿时间:2013-05-04  修订日期:2013-12-17
DOI:10.13328/j.cnki.jos.004542
中文关键词:  同步数据流语言  经过验证的编译器  形式化验证  形式语义  定理证明
英文关键词:synchronous data-flow language  verified compiler  formal verification  formal semantics  theorem proving
基金项目:国家自然科学基金(61170051, 61272086, 90818019)
作者单位E-mail
石刚 清华大学 计算机科学与技术系,北京 100084
新疆大学 信息科学与工程学院,新疆 乌鲁木齐 830046 
shigang1022@163.com 
王生原 清华大学 计算机科学与技术系,北京 100084  
董渊 清华大学 计算机科学与技术系,北京 100084  
嵇智源 科技部 高技术研究发展中心,北京 100044  
甘元科 清华大学 计算机科学与技术系,北京 100084  
张玲波 清华大学 计算机科学与技术系,北京 100084  
张煜承 清华大学 计算机科学与技术系,北京 100084  
王蕾 清华大学 计算机科学与技术系,北京 100084  
杨斐 清华大学 计算机科学与技术系,北京 100084  
摘要点击次数: 3360
全文下载次数: 3328
中文摘要:
      同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.
英文摘要:
      Synchronous data-flow languages have been widely used in safety-critical industrial areas such as airplanes, high-speed railways, nuclear power plants, and so on. However,the safety of development tools themselves for this kind of languages has become one of the potential safety problems which have been highly focused on. It has proved to be successful to implement the construction and verification of a conventional language compiler using an assistant theorem prover, and it is expected to have the opportunity in solving the miscompilation problem to the utmost extent. Based on such an approach, the key technologies for a trustworthy compiler from a synchronous data-flow language (Lustre as the prototype) to a sequential imperative language (C as the prototype) have been studied. The challenge lies in the great difference between the source and target languages, where the source language has the features of clock synchrony, data-flow, concurrency, stream data object, etc., while the target language is instead with the sequential and control-flow features. Among the similar researches, there is no reported result so far for the key translation stages. Recently, this research completed a formal verification for the whole compilation stages in the case of single clock. The related technologies will be taken into the development of a safety-level compiler in the country’s nuclear power system. The paper presents a survey on the trustworthy compiler with the research background, the architecture, the key technologies, the current status, and the future work.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利