Computer Science

Computer Science ›› 2026, Vol. 53 ›› Issue (6): 388-395.doi: 10.11896/jsjkx.250400014

• Computer Software • Previous Articles     Next Articles

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 Online:2026-06-15 Published: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)

40

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

CLC Number: 

  • 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.
[1] YU Liu, LI Shuo, KUANG Ping, ZHOU Fan, JIANG Tao. Causal Intervention-based Mitigation of Spurious Correlations in Information Cascade PopularityPrediction [J]. Computer Science, 2026, 53(6): 304-314.
[2] JIANG Lei, WANG Zi, YANG Rong, HAN Wanglin. Human Motion Recognition Algorithm Based on Wearable Sensors [J]. Computer Science, 2026, 53(2): 342-348.
[3] HAN Lei, SHANG Haoyu, QIAN Xiaoyan, GU Yan, LIU Qingsong, WANG Chuang. Constrained Multi-loss Video Anomaly Detection with Dual-branch Feature Fusion [J]. Computer Science, 2026, 53(2): 236-244.
[4] CHEN Zhangyuan, CHEN Ling, LIU Wei, LI Bin. Method for Selecting Observers Based on Doubly Resolving Set in Independent Cascade Model [J]. Computer Science, 2025, 52(4): 280-290.
[5] ZHANG Cong, CHEN Zhe, WANG Huijie, WEI Yiyang. SCADE Model Checking Based on Implicit Predicate Abstraction and Property-directedReachability [J]. Computer Science, 2025, 52(12): 24-31.
[6] HU Peng, XIA Xiaohua, ZHONG Yuquan. Road Crack Detection Method for Embedded Applications [J]. Computer Science, 2025, 52(12): 175-188.
[7] WANG Qian, HE Lang, WANG Zhanqing, HUANG Kun. Road Extraction Algorithm for Remote Sensing Images Based on Improved DeepLabv3+ [J]. Computer Science, 2024, 51(8): 168-175.
[8] SHAO Wenxin, YANG Zhibin, LI Wei, ZHOU Yong. Natural Language Requirements Based Approach for Automatic Test Cases Generation of SCADE Models [J]. Computer Science, 2024, 51(7): 29-39.
[9] DENG Ziwei, CHEN Ling, LIU Wei. Continuous Influence Maximization Under Independent Cascade Propagation Model [J]. Computer Science, 2024, 51(6): 161-171.
[10] LI Yu, YANG Xiangli, ZHANG Le, LIANG Yalin, GAO Xian, YANG Jianxi. Combined Road Segmentation and Contour Extraction for Remote Sensing Images Based on Cascaded U-Net [J]. Computer Science, 2024, 51(3): 174-182.
[11] HU Shaoru, WANG Juanwei, WANG Shengyuan. Implementation of Retargeting CompCert Trusted Compiler for Loongson Processors [J]. Computer Science, 2024, 51(11A): 240200115-9.
[12] WANG Yuchen, GAO Chao, WANG Zhen. Survey of Inferring Information Diffusion Networks [J]. Computer Science, 2024, 51(1): 99-112.
[13] BAI Mingli, WANG Mingwen. Fabric Defect Detection Algorithm Based on Improved Cascade R-CNN [J]. Computer Science, 2023, 50(6A): 220300224-6.
[14] SHEN Nan, CHEN Gang. Formalization of Inverse Matrix Operation Based on Coq [J]. Computer Science, 2023, 50(6A): 220400108-7.
[15] ZHANG Zelun, YANG Zhibin, LI Xiaojie, ZHOU Yong, LI Wei. Machine Learning Based Environment Assumption Automatic Generation for Compositional Verification of SCADE Models [J]. Computer Science, 2023, 50(6): 297-306.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.