微信服务号

微信订阅号

2025-6-2- 17
Home > Archive>Volume 36, Issue 8, 2025 >3554-3569. DOI:10.13328/j.cnki.jos.007350
PDF HTML XML Export Cite reminder
Trusted Compilation for Synchronous Dataflow Language Based on Pushdown Automata
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [20]
    • |
  • Related [20]
    • | | |
  • Comments
    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 not been formally verified, and their inner workings remain opaque to users. In recent years, translation validation methods that indirectly verify compiler correctness by proving the equivalence between source and target code have proven successful. This study proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. The proposed method successfully implements a trusted compiler from Lustre to C and rigorously proves the translation process’s correctness using Isabelle.

    Reference
    [1] Benveniste A, Caspi P, Edwards SA, Halbwachs N, Le Guernic P, De Simone R. The synchronous languages 12 years later. Proc. of the IEEE, 2003, 91(1): 64–83.
    [2] Caspi P, Pilaud D, Halbwachs N, Plaice JA. Lustre: A declarative language for real-time programming. In: Proc. of the 14th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. Munich: ACM, 1987. 178–188. [doi: 10.1145/41625.41641]
    [3] Halbwachs N, Caspi P, Raymond P, Pilaud D. The synchronous data flow programming language Lustre. Proc. of the IEEE, 1991, 79(9): 1305–1320.
    [4] Berry G, Gonthier G. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 1992, 19(2): 87–152.
    [5] Berry G. The foundations of Esterel. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner. Cambridge: The MIT Press, 2000. 425–454.
    [6] Le Guernic P, Gautier T, Le Borgne M, Le Maire C. Programming real-time applications with SIGNAL. Proc. of the IEEE, 1991, 79(9): 1321–1336.
    [7] Le Guernic P, Talpin JP, Le Lann JC. Polychrony for system design. Journal of Circuits, Systems and Computers, 2003, 12(3): 261–303.
    [8] Lustre V6 home. http://www-verimag.imag.fr/Lustre-V6.html?lang=en
    [9] McCarthy J, Painter J. Correctness of a compiler for arithmetic expressions. In: Mathematical Aspects of Computer Science 19: Proc of Symposia in Applied Mathematics. American Mathematical Society, 1967. 33?41.
    [10] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115.
    [11] CompCert. http://compcert.inria.fr/
    [12] Yang XJ, Chen Y, Eide E, Regehr J. Finding and understanding bugs in C compilers. In: Proc. of the 32nd ACM SIGPLAN Conf. on Programming Language Design and Implementation. San Jose: ACM, 2011. 283–294. [doi: 10.1145/1993498.1993532]
    [13] Paulin C, Pouzet M. Certified compilation of SCADE/Lustre. 2006. https://www.lri.fr/~paulin/lustreincoq.pdf
    [14] Bourke T, Brun L, Dagand Pé, Leroy X, Pouzet M, Rieg L. A formally verified compiler for Lustre. ACM SIGPLAN Notices, 2017, 52(6): 586–601.
    [15] 尚书, 甘元科, 石刚, 王生原, 董渊. 可信编译器 L2C 的核心翻译步骤及其设计与实现. 软件学报, 2017, 28(5): 1233–1246.
    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
    [16] Pnueli A, Siegel M, Singerman E. Translation validation. In: Proc. of the 4th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Lisbon: Springer, 1998. 151–166. [doi: 10.1007/BFb0054170]
    [17] Pnueli A, Shtrichman O, Siegel M. Translation validation for synchronous languages. In: Proc. of the 25th Int’l Colloquium. Aalborg: Springer, 1998. 235–246. [doi: 10.1007/BFb0055057]
    [18] van Ngo C, Talpin JP, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychromous equations. In: Latella D, Treharne H, eds. Proc. of the 2012 Int’l Conf. on Integrated Formal Methods, 2012. 113–127.
    [19] van Ngo C, Talpin JP, Gautier T, Le Guernic P. Translation validation for clock transformations in a synchronous compiler. In: Proc. of the 18th Int’l Conf. on Fundamental Approaches to Software Engineering, 2015. 171–185.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 26,2024
  • Revised:October 14,2024
  • Online: December 10,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2049861Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063