微信服务号

微信订阅号

2025年4月4日 23:18 星期五
首页 > 过刊浏览>2025年第36卷第8期 >0-0. DOI:10.13328/j.cnki.jos.007350
PDF HTML阅读 XML下载 导出引用 引用提醒
基于下推自动机的同步数据流语言可信编译方法
作者:
通讯作者:

罗杰,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:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [21]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    同步数据流语言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.

    参考文献
    [1] Benveniste A, Caspi P, Edwards S A, et al. The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91(1): 64-83.[doi: 10.1109/JPROC.2002.805826]
    [2] Caspi P, Pilaud D, Halbwachs N, Plaice JA. LUSTRE: A declarative language for real-time programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '87). Association for Computing Machinery, New York, NY, USA, 1987, 178-188. [doi: 10.1145/41625.41641]
    [3] Halbwachs N,Caspi P,Raymond P,et al.The synchronous dataflow programming language lustre.Proc.of the IEEE,1991,79(9):1305-1320.[ doi: 10.1109/5.97300]
    [4] Berry G,Gonthier G.The esterel synchronous programming language : Design, semantics, implementation.Science of Computer Programming,1992,19(2):87-152.[doi: 10.1016/0167-6423(92)90005-V]
    [5] Berry G.The foundations of esterel.In:Proc.of the Proof,Language and Interaction : Essaysin Honour of Robin Milner.Cambridge:The MIT Press,2000:425-454.
    [6] Le Guernic P,Gautier T,Le Borgne M,et al.Programming real time applications with signal.Proc.of the IEEE,1991,79(9):1321-1336.[doi: 10.1109/5.97301]
    [7] Le Guernic P,Talpin J,Le Lann J.Polychrony for system design.Journal for Circuits,Systems and Computers,2003,12(3):261-304.[doi: 10.1142/S0218126603000763]
    [8] Lustre-v6 home.http://www-verimag.imag.fr/Lustre-V6.html?lang=en.
    [9] McCarthy J, Painter J. Correctness of a compiler for arithmetical expressions.Mathematical Aspects of Computer Science 19: Proc of Symposia in Applied Mathematics, 1967: 33-41.
    [10] Stepney S, Whitley D, Cooper D, et al. A demonstrably correct compiler. Formal Aspects of Computing, 1991, 3(1): 58-101.[doi: 10.1007/BF01211435]
    [11] LEROY X.Formal verification of a realistic compiler.Communications of The ACM,2009,52(7):107-115.[doi: 10.1145/1538788.1538814 ]
    [12] CompCert Main Page.http://compcert.inria.fr/.
    [13] Yang, Xuejun et al.Finding and understanding bugs in C compilers.ACM-SIGPLAN Symposium on Programming Language Design and Implementation (2011).[doi: 10.1145/1993316.1993532]
    [14] BERTOT Y,CASTRAN P.Interactive Theorem Proving and Program Development - Coq’Art:The Calculus of Inductive Constructions.Texts in Theoretical Computer Science.An EATCS Series,Springer Verlag,2004.
    [15] PAULIN C,POUZET M.Certified compilation of scade/lustre.https://www.lri.fr/~paulin/lustreincoq.pdf,2006.
    [16] Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017. A formally verified compiler for Lustre. SIGPLAN Not. 52, 6 (June 2017), 586-601. [doi: 10.1145/3140587.3062358]
    [17] Pnueli A, Siegel M Singerman E. Translation validation. In: Proc. of the TACAS’98. LNCS 1384, Springer-Verlag, 1998.151-166.
    [18] Pnueli A, Shtrichman O, Siegel M. Translation validation for synchronous languages. In: Proc. of the ICALP’98. LNCS 1443,Springer-Verlag, 1998. 235-246. [doi: 10.1007/BFb0055057]
    [19] Shang S, Gan YK, Shi G, Wang SY, Dong Y. Key translations of the trustworthy compiler L2C and its design and implementation. Ruan Jian Xue Bao/Journal of Software, 2017,28(5):1233-1246 (in Chinese with English abstract). http://www.jos.org.cn/1000 9825/5213.htm [doi: 10.13328/j.cnki.jos.005213]
    附中文参考文献:
    [19] 尚书,甘元科,石刚,王生原,董渊.可信编译器 L2C 的核心翻译步骤及其设计与实现.软件学报,2017,28(5):1233-1246. http://www. jos.org.cn/1000-9825/5213.htm [doi: 10.13328/j.cnki.jos.005213]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:70
  • 下载次数: 122
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2024-08-26
  • 最后修改日期:2024-10-14
  • 在线发布日期: 2024-12-10
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19788010位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号