Page 131 - 《软件学报》2025年第8期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3554−3569 [doi: 10.13328/j.cnki.jos.007350] [CSTR: 32375.14.jos.007350] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
基于下推自动机的同步数据流语言可信编译

于 涛 1 , 王珊珊 1 , 徐芊卉 1 , 董晓晗 1 , 胡代金 2 , 罗 杰 1 , 杨溢龙 2 , 吕江花 1 , 马殿富 1

1
(北京航空航天大学 计算机学院, 北京 100191)
2
(北京航空航天大学 软件学院, 北京 100191)
通信作者: 罗杰, E-mail: luojie@buaa.edu.cn; 杨溢龙, E-mail: yilongyang@buaa.edu.cn;
吕江花, E-mail: jhlv@buaa.edu.cn; 马殿富, E-mail: dfma@buaa.edu.cn

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

中文引用格式: 于涛, 王珊珊, 徐芊卉, 董晓晗, 胡代金, 罗杰, 杨溢龙, 吕江花, 马殿富. 基于下推自动机的同步数据流语言可信编
译. 软件学报, 2025, 36(8): 3554–3569. http://www.jos.org.cn/1000-9825/7350.htm
英文引用格式: Yu T, Wang SS, Xu QH, Dong XH, Hu DJ, Luo J, Yang YL, Lyu JH, Ma DF. Trusted Compilation for Synchronous
Dataflow Language Based on Pushdown Automata. Ruan Jian Xue Bao/Journal of Software, 2025, 36(8): 3554–3569 (in Chinese). http://
www.jos.org.cn/1000-9825/7350.htm

Trusted Compilation for Synchronous Dataflow Language Based on Pushdown Automata
1 1 1 1 2 1 2
YU Tao , WANG Shan-Shan , XU Qian-Hui , DONG Xiao-Han , HU Dai-Jin , LUO Jie , YANG Yi-Long ,
1
LYU Jiang-Hua , MA Dian-Fu 1
1
(School of Computer Science and Engineering, Beihang University, Beijing 100191, China)
2
(School of Software, Beihang University, Beijing 100191, China)
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.
Key words: synchronous dataflow language; verified compiler; formal verification; Lustre language

同步数据流语言是建模语言的一种, 主要被应用于开发实时控制系统 [1] , 如飞控系统、车载系统等. 同步数据
流语言具有数据流特性和同步特性, 因此特别适合实时控制系统的开发. 近年来出现了一些同步数据流语言, 包
括 Lustre [2,3] 、Esterel [4,5] 、Signal [6,7] 等. 其中的 Lustre 目前已经更新到 Lustre V6 版本 [8] .

* 基金项目: 国家重点研发计划 (2022YFB4501900)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-26; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-04-17