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

3566 软件学报 2025 年第 36 卷第 8 期

表 10 编译各阶段耗时与代码运行时间

编译阶段 运行时间 (ms)
下推自动机生成 30.100
词法分析 (每100行平均) 18.200
代码生成 (每100行平均) 80.010
目标代码运行时间 (1 000万周期) 120.000

6 局限性与扩展性讨论

Lustre 语言到 C 语言的目标码转换模式和转换动作支持 Lustre V6 语言中 99% 的文法单元和语言特性, 且涵
盖了 SCADE 中所有和 Lustre 相关的语言特性. 利用下推自动机生成、下推自动机识别和代码生成的算法, 以及
Lustre 到 C 的目标码转换模式, 实现了由 Lustre 语言到 C 语言的编译系统. 编译系统支持类型检查和 Lustre 语言
特有的始终检查、拓扑排序功能. 该编译器符合 DO-178C 开发规范, 且主要算法和模块独立于 Lustre 语言和 C
语言, 具有较好的可扩展性. 该方法已经应用于 SCADE 语言的编译器开发中, 目前已经完成了对时钟算子、时态
算子、数组与结构体算子、算术逻辑运算、函数调用、状态机和条件块等相关文法的代码生成, 并对某一大型飞
机的刹车系统和主飞行显示器系统 (primary flight display, PFD) 进行案例研究, 最终转换得到的 C 目标码与原系
统 SCADE 模型的运行结果一致, 充分验证了其在 SCADE 语言上的扩展性.
该编译系统并未涉及编译优化相关内容, 而编译优化在编译器当中是重要的一部分. 未来将主要从这几个方
面进行优化: 1) 消除无用的代码, 采用数据流分析, 找出没有影响输出的变量或表达式并删除; 2) 常量传播, 如果
某些输入或中间变量的值在编译时已经是常量, 运用值分析技术进行替换, 减少运行时的计算开销; 3) 循环优化,
实施循环不变代码提升, 将循环中不变的部分移到循环外, 减少循环次数, 并结合循环展开技术减少循环控制
开销.

7 总结与未来工作

本文针对安全关键系统开发过程中编译的可靠性问题, 研究了基于下推自动机的编译方法和基于语义一致性
的验证方法. 提出了 Lustre 语言可信编译方法, 实现了基于下推自动机的 Lustre 语言到 C 语言的可信编译, 并使
用 Isabelle 对编译方法进行了验证. 本文的研究成果如下.
(1) 下推自动机的生成算法: 该算法能够自动将符合一定格式的上下文无关文法转换为对应的下推自动机, 该
算法分 4 步得到了完整的由开始状态到中间状态最后到终止状态的下推自动机. 且由该算法生成的下推自动机具
有扩展性, 可以独立地生成下推自动机再进行合并.
(2) 下推自动机的识别算法: 该算法独立于下推自动机的具体结构, 将下推自动机作为输入的一部分. 该算法
接受下推自动机生成算法产生的下推自动机和源程序经过词法分析得到的词法单元流作为输入, 模拟下推自动机
的运行, 对源程序进行语法分析和语义分析.
(3) 基于下推自动机的识别算法的代码生成方法: 该方法通过将代码的编译过程抽象为源文法单元和目标码
转换模式, 将目标码转换模式编写为转换动作嵌入下推自动机识别过程当中, 从而在下推自动机识别的过程中完

成源语言到目标语言的编译过程.
(4) 由 Lustre 语言到 C 语言的编译系统: 该编译系统支持类型检查和 Lustre 语言特有的始终检查、拓扑排序
功能. 该系统符合 DO-178C 开发规范, 且主要算法和模块独立于 Lustre 语言和 C 语言, 具有较好的可扩展性.
(5) 基于语义一致性的形式化验证方法: 该方法将编译过程的正确性转化为编译前后程序的语义一致性. 而编
译前后程序的一致性又可规约为编译前后程序所包含的文法单元的一致性, 由此可以利用 Isabelle/HOL 的自动推
导能力自动地证明程序的一致性.