计算机科学

计算机科学 ›› 2026, Vol. 53 ›› Issue (6): 388-395.doi: 10.11896/jsjkx.250400014

• 计算机软件 • 上一篇    下一篇

L2C可信编译器中的时钟分析/检查及其验证框架探讨

甘元科, 王蕾, 王生原   

  1. 清华大学计算机系 北京 100084
  • 收稿日期:2025-04-02 修回日期:2025-06-14 出版日期:2026-06-15 发布日期:2026-06-09
  • 通讯作者: 王生原(wwssyy@tsinghua.edu.cn)
  • 作者简介:(anshuer@foxmail.com)
  • 基金资助:
    国家重点研发计划(2022YFB3305204)

Clock Analysis and/or Check in L2C Trusted Compiler and Investigation on Its Verification Framework

AN Yuanke, WANG Lei, WANG Shengyuan   

  1. Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China
  • Received:2025-04-02 Revised:2025-06-14 Published:2026-06-15 Online:2026-06-09
  • About author:GAN Yuanke,born in 1983,master,engineer.His main research interests include compiler and formal verification.
    WANG Shengyuan,born in 1964,Ph.D,associate professor,is a senior member of CCF(No.06117S).His main research interests include programming languages and systems,compiler and formal methods.
  • Supported by:
    National Key R & D Program of China(2022YFB3305204).

PDF (PC)

66

摘要： Scade是一种广泛用于安全关键嵌入式控制软件开发的著名商业工具,其建模语言是一种同步语言,扩展自同步数据流语言Lustre。L2C可信编译器是经过形式化验证的类Scade建模语言到C语言高可信编译器长线项目之一。与同类工作相比,其源语言特性更接近于Scade建模语言。对于L2C可信编译器前端设计的一个重要环节,即时钟分析/检查过程的构造与验证,主要介绍分析/检查过程所采用的时钟分析/检查规则,并探讨其验证框架。

关键词: Scade, 同步语言, 可信编译器, 形式化验证的编译器, 时钟分析/检查, Coq

Abstract: Scade is a well-known commercial tool widely used in developing safety-critical embedded control software.Its mode-ling language is a synchronous language,which extends from Lustre,a synchronous data-flow language.The L2C trusted compiler is one of the long-term projects on the highly trusted compilers from a Scade-like modeling language to C,developed with formal verification.Compared to other similar works,the source language features of the L2C trusted compiler are closer to those in the Scade modeling language.An important aspect of the front-end design in the L2C trusted compiler is involved,that is,the construction and verification of the clock analyzer or checker.This paper focuses on introducing the clock analyzing or checking rules adopted in the analyzer or checker,and briefly describes the investigation on its verification framework.

Key words: Scade, Synchronous languages, Trusted compilers, Formally verified compilers, Clock analysis and/or check, Coq

中图分类号: 

  • TP314
[1]CASPI P,PILAUD D,HALBWACHS N,et al.Lustre:a declarative language for programming synchronous systems[C]//Proceedings of the 14th ACM Symposium on Principles of Programming Languages.1987:178-188.
[2]HALBWACHS N,CASPI P,RAYMOND P,et al.The synchronous dataflow programming language LUSTRE[J].Proceedings of the IEEE,1991,79(9):1305-1320.
[3]LE GUERNIC P,GAUTIER T,LE BORGNE M,et al.Pro-gramming real time applications with SIGNAL[C]//Procee-dings of the IEEE,1991,79(9):1321-1336.
[4]BENVENISTE A,LE GUERNIC P,JACQUEMOT C.Synchronous Programming with Events and Relations:the SIGNAL Language and Its Semantics[J].Science of Computer Programming,1991,16(2):103-149.
[5]BOUSSINOT F,DE SIMONE R.The ESTEREL language[J].Proceedings of the IEEE,1991,79(9):1293-1304.
[6]BERRY G,GONTHIER G.The Esterel synchronous programming language:Design,semantics,implementation[J].Science of Computer Programming,1992,19(2):87-152.
[7]XAVIER L.Verified Squared:Does Critical Software DeserveVerified Tools[C]//Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.2011.
[8]BOURKE T,BRUN L,DAGAND P E,et al.A Formally Verified Compiler for Lustre[C]//Proceedings of the Programming Language Design and Implementation.2017:586-601.
[9]BOURKE T,BRUN L,POUZET M.Mechanized Semantics andVerified Compilation for a Dataflow Synchronous Language with Reset[C]//Proceedings of the 47th ACM SIGPLAN Sympo-sium on Principles of Programming Language.2020.
[10]SHI G,ZHANG Y C,SHANG S,et al.A formally verifiedtransformation to unify multiple nested clocks for a Lustre-like language[J].Science China Information Sciences,2019,62(1):12801.
[11]PNUELI A,SHTRICHMAN O,SIEGEL M.Translation validation for synchronous languages[C]//Proceedings of ICALP'1998.1998:235-246.
[12]NGO V C,TALPI J P,GAUTIER T.Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler[C]//International Conference on Formal Techniques for Distributed Objects,Components and Systems(FORTE'15).2015.
[13]RYABTSEV M,STRICHMAN O.Translation validation:From Simulink to C[C]//Proceedings of the 21st International Conference on Computer Aided Verification(CAV 2009).2009:696-701.
[14]YANG Z B,BODEVEIX J P,FILALI M,et al.Towards a Verified Compiler Prototype for the Synchronous Language SIGNAL[J].Frontiers of Computer Science,2016,10(1):37-53.
[15]Scade-suite[EB/OL].http://www.esterel-technologies.com/products/scade-suite.
[16]JEAN-LOUISC,BRUNO P,MARC P.Scade 6:A Formal Language for Embedded Critical Software Development[C]//Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering(TASE 2017).2017:4-15.
[17]BERTOT Y,CASTÉRAN P.Interactive Theorem Proving and Program Development-Coq'Art:The Calculus of Inductive Constructions[C]//Texts in Theoretical Computer Science.An EATCS Series,Springer,2004.
[18]The Coq Development Team.The Coq Proof Assistant Refe-rence Manual[EB/OL].http://coq.inria.fr/.
[19]LEROY X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.
[20]LEROY X.Formal certification of a compiler back-end or:programming a compiler with a proof assistant[C]//Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.2006:42-54.
[21]CompCert[EB/OL].http://compcert.inria.fr.
[22]BLAZY S,LEROY X.Mechanized semantics for the Clight subset of the C language[J].Journal of Automated Reasoning,2009,43(4):263-288.
[23]MORRISETT G.Technical Perspective:A Compiler's Story[J].Communications of the ACM,2009,52(7):106.
[24]BOURKE T,PESIN B,POUZET M.Verified Compilation of Synchronous Dataflow with State Machines[C]//Proceedings of EMSOFT 2023:23rd International Conference on Embedded Software.2023.
[25]Vélus[EB/OL].https://velus.inria.fr.
[26]SHANG S,GAN Y K,SHI G,et al.Key translations of the trustworthy compiler L2C and its design and implementation[J].Ruan Jian Xue Bao/Journal of Software,2017,28(5):1233-1246.
[27]KANG Y X,GAN Y K,WANG S Y.Comparison of two trustworthy compilers Vélus and L2C for synchronous languages[J].Ruan Jian Xue Bao/Journal of Software,2019,30(7):2003-2018.
[28]L2C Team.Open source version of L2C(1.0)[EB/OL].ht-tps://github.com/wwssyy/Open-L2C/blob/master/open-l2c-1.0.zip,2021.
[29]JOURDAN J H,POTTIER F,LEROY X.Validating LR(1)parsers[C]//Proceedings of 21st European Symposium on Programming.2012:397-416.
[30]PNUELI A,SIEGEL M,SINGERMAN E.Translation Validation[C]//Proceedings of TACAS'98,Lecture Notes in Compu-ter Science.1998:151-166.
[31]Scade Language Reference Manual[M].ANSYS,Inc.,2020.
[32]BERTAILS A,BIERNACKI D,PAULIN C,et al.A CertifiedCompiler for the Synchronous Language Lustre[C]//Presentation of TYPES 2007.2007.
[33]BIERNACKI D,COLACO J L,HAMON G,et al.Clock-directed modular code generation for synchronous data-flow languages[C]//Proceedings of LCTES.2008.
[34]AUGER C,COLACO J L,HAMON G,et al.A formalization and proof of a modular lustre compiler[EB/OL].http://www.di.ens.fr/~pouzet/cours/mpri/cours4/scp12.pdf.
[35]AUGER C.Compilation certifiée de SCADE/LUSTRE[EB/OL].https://theses.hal.science/file/index/docid/818169/file-name/VD2_AUGER_CEDRIC_07022013.pdf.
[36]JEAN-BAPTISTE T,GOVEREAU P,MORRISETT G.Evaluating value-graph translation validation for LLVM[C]//Proceedings of the 32nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2011:295-305.
[37]KANADE A,SANYAL A,KHEDKER U.A PVS based framework for validating compiler optimizations[C]//Proceedings of the 4th Software Engineering and Formal Methods.IEEE Computer Society,2006:108-117.
[38]NECULA G C.Translation validation for an optimizing compiler[C]//Proceedings of the 31nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2000:83-95.
[39]TRISTAN J B,LEROY X.Formal verification of translationvalidators:A case study on instruction scheduling optimizations[C]//Proceedings of the 35th Symposium Principles of Programming Languages.ACM,2006:17-27.
[40]TRISTAN J B,LEROY X.Verified validation of lazy code motion[C]//Proceedings of the 37nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2009:316-326.
[41]TRISTAN J B,LEROY X.Verified validator for software pipelining[C]//Proceedings of the 38nd ACM SIGPLAN Conference on Programming and Language Design Implementation.2010:83-92.
[42]NGO V C,TALPIN J P,GAUTIER T,et al.Verification of Compiler Transformations on Polychronous Equations[C]//Proceedings of IFM.2012:113-127.
[43]NGO V C,TALPIN J P,GAUTIER T,et al.Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools[C]//Proceedings of the 18th Internatio-nal Workshop on Software and Compilers for Embedded Systems(SCOPES'15).ACM,2015:109-112.
[44]Lustre-V6[EB/OL].http://www-verimag.imag.fr/Lustre-V6.html.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市两江新区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发