 |
|
|
|
 |
 |
 |
|
 |
|
 |
|
|
| 刘洋,甘元科,王生原,董渊,杨斐,石刚,闫鑫.同步数据流语言高阶运算消去的可信翻译.软件学报,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) |
|
| 摘要点击次数: 4497 |
| 全文下载次数: 3165 |
| 中文摘要: |
| 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阅读器 |
|
|
|
|
|
|
 |
|
|
|
|
 |
|
 |
|
 |
|
