基于下推自动机的同步数据流语言可信编译方法
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

罗杰,E-mail:luojie@buaa.edu.cn;杨溢龙,E-mail:yilongyang@buaa.edu.cn;吕江花,E-mail:jhlv@buaa.edu.cn;马殿富,E-mail:dfma@buaa.edu.cn

中图分类号:

TP311

基金项目:

国家重点研发计划(2022YFB4501900)


A Trusted Compilation Method for Synchronous Dataflow Language Based on Pushdown Automata
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    同步数据流语言Lustre是安全关键系统开发中常用的开发语言,其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证,对用户也处于黑盒状态.近年来,通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法被证明是成功的.基于下推自动机的编译方法和基于语义一致性的验证方法,提出了Lustre语言可信编译方法, 能够将Lustre语言转换为C语言并进行形式化验证以保证编译的正确性,并使用Isabelle对翻译转换过程进行严格的正确性证明.

    Abstract:

    The synchronous dataflow language Lustre is commonly used in the development of safety-critical systems. However, existing official code generators and the SCADE KCG code generator have neither been formally verified nor are they transparent to users. In recent years, translation validation methods that indirectly verify the correctness of compilers by proving the equivalence of source and target codes have been shown to be successful. This paper proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. It successfully implements a trusted compiler from Lustre to C and rigorously proves the correctness of the translation process using Isabelle.

    参考文献
    相似文献
    引证文献
引用本文

于涛,王珊珊,徐芊卉,董晓晗,胡代金,罗杰,杨溢龙,吕江花,马殿富.基于下推自动机的同步数据流语言可信编译方法.软件学报,2025,36(8):0

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2024-08-26
  • 最后修改日期:2024-10-14
  • 录用日期:
  • 在线发布日期: 2024-12-10
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号