主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫.同步数据流语言高阶运算消去的可信翻译.软件学报,2015,26(2):332-347
同步数据流语言高阶运算消去的可信翻译
Trustworthy Translation for Eliminating High-Order Operation of a Synchronous Dataflow Language
投稿时间:2014-07-05  修订日期:2014-10-31
DOI:10.13328/j.cnki.jos.004785
中文关键词:  同步数据流语言  形式化验证  高阶运算  定理证明
英文关键词:synchronous dataflow language  formal verification  high-order operation  theorem proving
基金项目:国家自然科学基金(61272086); 国家科技支撑计划(2013BAB05B05)
作者单位E-mail
刘洋 清华大学 计算机科学与技术系, 北京 100084 13893759002@139.com 
甘元科 清华大学 计算机科学与技术系, 北京 100084  
王生原 清华大学 计算机科学与技术系, 北京 100084  
董渊 清华大学 计算机科学与技术系, 北京 100084  
杨斐 清华大学 计算机科学与技术系, 北京 100084  
石刚 清华大学 计算机科学与技术系, 北京 100084
新疆大学 信息科学与工程学院, 新疆 乌鲁木齐 830046 
 
闫鑫 清华大学 计算机科学与技术系, 北京 100084
太原理工大学 计算机学院, 山西 太原 030021 
 
摘要点击次数: 2970
全文下载次数: 2376
中文摘要:
      Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.
英文摘要:
      Lustre is a synchronous dataflow language widely used in safety critical industrial control system. Formal verification is efficient to improve the reliability of the compiler which translates Lustre to C. Based on this approach, this paper conducts a research on the trustworthy compiler for translating Lustre*(a Lustre-like language) to Clight (a subset language of C). The entire compiling process is divided into different stages to tackle the large difference between Lustre* and Clight. Each stage performs a specific translation task. This paper describes a translation algorithm which eliminates high-order operations. The implementation of translation process is assisted by theorem proving tool Coq, and a strict proof of correctness of the process is also provided.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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