Lustre语言可信代码生成器研究进展

第27卷 第5期

2020年5月

仪器仪表用户

INSTRUMENTATION

Vol.27

2020 No.5

Lustre语言可信代码生成器研究进展

兰 林，马 权，侯荣彬，蒋 维，杨 斐

（中国核动力研究设计院 核反应堆系统设计技术重点实验室，成都 610213）

安全攸关的嵌入式领域广泛使用基于Lustre语言描述的图形化逻辑。工程师通过图形化逻辑建模工具编写

摘 要：

控制逻辑，再通过代码生成器把控制逻辑转换成可执行代码下装到嵌入式设备中运行。因此，如何保证代码生成器

生成代码的正确性成为关注的焦点。通过测试等传统方法来确保代码生成器的正确性，其覆盖率有限，无法完全解

决误编译的问题；而把形式化方法用于开发代码生成器，通过逻辑推理的方式证明代码生成的正确性，将最大限度

地解决误编译的问题，使其成为一个可信代码生成器。本文首先分析了同步数据流语言Lustre的语法特征，然后介

绍了Lustre语言可信代码生成器的研究进展和形式化开发方法，为开发应用于嵌入式安全攸关领域的Lustre可信代

码生成器提供借鉴。

关键词：可信代码生成；Lustre；形式化验证；定理证明；翻译验证；安全攸关

中图分类号：TP273 文献标志码：A

DOI:10.3969/.1671-1041.2020.05.018

文章编号：1671-1041(2020)05-0068-05

Research and Progress of Lustre Trusted Code Generator

Lan Lin，Ma Quan，Hou Rongbin，Jiang Wei，Yang Fei

（Science and Technology on Reactor System Design Technology Laboratory Nuclear Power Institute of China,

Chengdu, 610213, China）

Abstract：Graphical logic based on the description of the Lustre language is widely used in security-relevant embedded fields.

The engineer develop the control logics through a code generator and downloads it to the embedded device to run. Therefore, how

to ensure the reliability of the Lustre code generator has become the focus of attention. Traditional development methods such as

testing have limited coverage and cannot solve the problem of mis-compilation. However, using formal methods to develop trusted

code generators and proving the correctness of the code through logical reasoning will maximize the resolution of mis-compilation.

This article briefly analyzes the characteristics of the synchronous date flow language Lustre, mainly introduces the research pro-

gress of the Lustre trusted code generator, Provides a new idea for developing a Lustre trusted code generator.

Key words：trusted code generation；lustre；formal methods；theorem proof；translation validation；safety-critical

0 引言

控制逻辑翻译为C代码。这些领域对软件的安全性要求非

安全攸关的嵌入式控制领域（如核仪控、轨道交通等

领域）常使用基于Lustre语言描述的图形化逻辑建模工具

（如SCADE等）来开发控制逻辑，然后使用代码生成器将

常严格（如在核仪控领域中必须满足核电标准IEC60880）。

因此，为保证嵌入式软件的可靠运行，必须考虑代码生成

器（编译器）的可靠性。如果代码生成器存在潜在的错误，

收稿日期：

2020-03-09

作者简介：

兰林（1996-），男，四川南充人，硕士，从事安全级DCS技术研究与应用。

Copyright©博看网 . All Rights Reserved.

第5期兰 林·Lustre语言可信代码生成器研究进展

69

将会有产生不安全代码的风险，由此可能带来巨大的灾难

和损失。目前，主要是通过反复的测试和严格的过程管理

等传统方法来保证代码生成器的可靠性。但代码生成器在

开发过程中引入的错误通常是很难发现的，采用传统的方

法无法杜绝代码生成器的误编译。经过传统方法开发的编

译器如GCC、LLVM，通过Csmith工具发现了多个错误，

即使工控领域广泛使用的SCADE Suite也不能证明它不会

出现误编译。而通过形式化方法开发的代码生成器，能够

在开发的同时，对其翻译前后语言语义一致性进行逻辑推

理证明，能够最大限度地消除误编译。本文将在阐述可信

代码生成器形式化开发方法的基础上，介绍同步数据流语

言Lustre的特征及相关可信代码生成器的形式化研究进展。

二元fby算子：相当于pre算子和->算子的结合

体。若表达式E和F的值序列分别为（e

1

,e

2

,...,e

n

,...）和

（f

1

,f

2

,...,f

n

,...），且它们的逻辑时钟都相同，那么E fby F

的时钟也和E、F的时钟相同，对应的值序列为（e

1

,

f

1

,f

2

,...,f

n

,...）。

三元fby算子：若表达式E和F的值序列分别为

（e

1

,e

2

,...,e

n

,...）和（f

1

,f

2

,...,f

n

,...），且它们的逻辑时钟都相同，

那么fby(E,n,F)的时钟也和E、F的时钟相同，对应的值序

列（e

1

,e

2

,...,e

n

,f

1

,f

2

,...,f

n

,...）

when算子：用于过滤某些周期的值。若E是一个算术

表达式，B是一个布尔表达式，它们具有相同的时钟。那

么，表达式E when B 的逻辑时钟就是B对应的布尔值序列，

它的值序列就是当B为true时，E的取值。

1 Lustre语言

Lustre作为一种同步数据流语言，最早出现在

的论文中

[1]

，多用于嵌入式控制系统和信号处理系统。它

在工控领域主要用于描述实时控制逻辑，核仪控、航天航

空、轨道交通等安全攸关领域广泛使用的SCADE Suite就

是基于Lustre语言描述实现的。Lustre语言具有数据流特

征和确定性语义

[1]

，适用于反应式控制系统编程、模块化

的代码生成

[2]

2 可信代码生成器形式化开发方法

广义的讲，形式化方法是使用数方法来解决软件工程

领域中遇到的问题，主要内容是建立数学模型以及对其进

行充分、合理的分析；狭义的讲，形式化方法是使用形式

化语言对规则进行描述，然后进行逻辑推理和证明的方法。

经过形式化开发的可信代码生成器，其最大的特点是生成

的目标代码的行为是严格符合源语言语义的，即源程序与

目标代码之间语义具有一致性，不会产生有歧义的代码，

从而保证了代码生成的可靠性。用于开发可信代码生成器

的形式化方法主要有对代码生成器本身的证明和翻译验证，

接下来分别对这两种形式化开发方法进行介绍。

以及程序的形式化验证

[3-5]

。Lustre程序是由

一系列的node或 function声明、常量声明和数据类型声明

组成，node或function是用于处理输入流并输出的函数，

node体是由一系列等式组成。与串行命令式语言（如C语

言）相比，具有许多独有的特征，如下所示：

1）数据流和时钟

Lustre语言的变量、等式都是一个数据流（Stream）。

一个数据流由相同类型的数据值序列和逻辑时钟两部分组

成，默认情况下逻辑时钟都为true，叫作基本时钟。Lustre

程序具有周期性循环执行的特点，对应着无穷多个周期，

循环作用在数据流上。一个有基本时钟的数据流，在程序

执行的第n个周期，取值为数据流的第n个值。另外，可

以利用布尔值自定义一个时钟，使用时态算子对数据流进

行过滤等处理。

2）时态算子

pre算子：用于访问前一周期的值。若表达式E的无穷

多个周期对应的值序列为（e

1

,e

2

,...,e

n

,...）,则表达式pre(E)

的逻辑时钟与E相同，且当周期n=1时，它的值为nil（nil

表示一个未定义的值）；n>1时，它各周期的值为表达式E

前一个周期的值。即最后结果为pre(E)=（nil,e

1

,e

2

,...,e

n-1

,...）。

->算子：用于初始化，可以和pre算子结合使用，以

消除pre算子使用过程中第一个周期可能出现的nil。若表

达式E和F的值序列分别为（e

1

,e

2

,...,e

n

,...）和（f

1

,f

2

,...,f

n

,...），

且它们的逻辑时钟相同，那么，E->F 的时钟也和E、F的

时钟相同，且当n=1时，其值为E第一个周期的值；当

n>1时，其各周期的值分别为F对应的各周期的值。即最

后结果为E->F =（e

1

, f

2

,f

3

,...,f

n

,...）。

[6]

2.1 翻译验证

在可信代码生成器形式化验证领域，John Mccarthy等

人已经做了大量工作

[7-10]

，但仍然无法自动证明给定的优

化编译器的目标语言和源语言语义的一致性。如果不能证

明代码生成器本身的正确性，也许可以检查每个编译过程

的正确性。这启发了翻译验证技术，翻译验证的概念最早

由Pnueli等人于90年代提出

[11-13]

，作为一种形式化验证

代码生成器正确性的技术，用于避免代码在转换过程中引

入语义的歧义。翻译验证属于等价性验证的一种，它通过

验证源程序和目标代码的语义等价性来证明代码生成器的

正确性

[14,15]

。从而避免了对代码生成器本身的证明，只需

要对验证器进行定理证明，具有较好的可重用性。带有翻

译验证的代码生成过程如图1所示，与普通代码生成器的

编译过程是一样的，只是从源程序到目标代码翻译完成后，

没有立刻输出目标代码，而是增加了一个形式化开发的验

证器，用于验证源程序和目标代码的语义是否具有一致性。

把验证器看做一个函数Validate(S,C)，代码生成过程看作函

数Comp，验证语义等价性S≈C。如果由源程序S翻译生

成了目标代码C，即Comp(S)=OK(C)，并且通过了验证器的

验证，即Validate(S,C)=true。那么，生成的目标代码C就被

认为是可信的。因此验证器是翻译验证方法的核心，目标

代码通过了验证器的验证后，才输出目标代码，否则编译

Copyright©博看网 . All Rights Reserved.

70

仪器仪表用户

INSTRUMENTATION

第27卷

图1 带有翻译验证的代码生成过程

Fig.1 Code generation process with translation validation

报错。随着翻译验证技术的逐渐成熟，在商用代码生成器

中也得到了应用，Michael等人

[16]

为商用RTW代码生成器

开发了一个翻译验证工具TVS(RTW

[20]

代码生成器实现了从

Simulink模型转换到C代码过程)。文献[17]中，基于翻译

验证技术为GNU C优化编译器实现了一个验证器。

图2 对代码生成器本身进行证明的开发流程图

Fig.2 The process of theorem proving method to develop

trusted code generator

2.2 对代码生成器本身进行证明

另一种形式化开发可信代码生成器的方法是对代码生

成器本身进行证明。这是一种将源语言的语法、语义模型

及其满足规范的性质抽象为逻辑公式，然后使用逻辑推理

技术来证明其语义一致性的技术，是最严格的开发方式。

这种方法和数理逻辑相联系，常使用高阶逻辑系统进行形

式化描述，可通过Coq、Isabel/HOL等辅助定理证明工具

进行证明。该形式化开发方法贯穿整个可信代码生成器的

开发过程，为了降低形式化验证的难度，整个开发过程一

般会划分为包含不同中间语言的多个翻译阶段，逐步翻译

到目标代码。第一个形式化证明在1967年

对其进行了机械证明。Xavier

[20]

[8]

[18]

3 Lustre语言的可信代码生成器

学术界做了许多关于Lustre语言特性的形式化研究，

Jakubiec L

[24]

等人在Coq中使用归纳类型定义了Lustre语言

的一个子集；G. Hamon

[25]

等人研究了同步数据流语言Lucid

的高阶特性，并完成了Lucid时钟演算；E. Gimenez 等人

在开发Scade3代码生成器过程中，完成了Lustre语言的语

义和时钟的定义

[26]

。基于前人对Lustre语法语义及性质的

研究基础上，法国INRIA的Poute团队和清华大学计算机

系的L2C团队利用对代码生成器本身进行证明的方式，各

开发了一款用于学术研究的Lustre到Clight的代码生成器。

Poute团队于2006年启动了Lustre语言代码生成器的形式

化验证的研究工作，使用定理证明技术，在Coq中开发

得到了Lustre到Clight的可信代码生成器Velus。Velus的

架构如图3所示，主要由两部分内容构成，包括对源程序

Lustre的预处理和代码生成及优化。该团队成员BERTAILS

A等人

[27]

完成了Lustre程序的预处理过程，包括把源程序

解析成没有注入时钟和类型的抽象语法树（parsing）；对

程序注入时钟和类型（elaboration）以对程序进行静态检

查；简化程序中的复杂等式（normalization）；对程序进行

因果分析和拓扑排序，使并行程序串行化（scheduling）等

工作。该团队成员Bourke等人

[28]

，完成了中间代码生成

及优化和目标代码生成，以及语义一致性的证明。包括

从源程序到中间语言Obc的翻译（translation），该阶段消

去了Lustre程序中的fby等时态算子；对Obc代码的优化

（Fusion optimization）；从Obc到目标程序Clight的代码生成

手工完成的，

用于将算术表达式的编译成堆栈机器码，并在1972年

[19]

等人使用定理辅助证明工

具Coq，使用定理证明方式开发的CompCert编译器，实现

了从结构化的命令式语言到汇编代码的生成。CompCert由

两部分组成，编译器前端：把C语言子集Clight

[21]

转换成一

[22,23]

种低级的、结构化的中间语言Cminor；编译器后端：

把中间语言Cminor生成为汇编代码。定理证明方法开发

可信代码生成器的基本流程如图2所示，Language1和

Language 2分别代表可信代码生成器翻译过程中的两个中

间语言，首先分别定义好源语言和目标语言的形式化语法、

语义，然后证明翻译前后对应Language 1和Language 2的

语义是否具有一致性，如果一致，则说明这个过程是可信

的，利用Coq的抽取功能（Extraction）把翻译算法抽取成

Ocaml代码。否则，迭代修改其形式化语法、语义的形式

化定义，直到证明得到翻译前后语义具有一致性，再抽取

翻译算法。把各翻译阶段的可信翻译算法抽取出来与代码

生成器前端结合起来，最后就得到了一个经过证明的可信

代码生成器。

Copyright©博看网 . All Rights Reserved.

第5期兰 林·Lustre语言可信代码生成器研究进展

表1 Velus、L2C和SCADE的特性比较

Table 1 The comparison of Velus, L2C and SCADE

71

图3 Velus架构图

Fig.3 The architecture of Velus compiler

（generation）等工作。由图3中虚线连接的部分表示，经

Velus生成的Clight代码可直接在CompCert中编译，生成

能在嵌入式设备中运行的可执行代码。为了简化证明过程，

Vleus定义了一个中间语言Obc，这是在Lustre语言可信代

码生成器的开发过程中常用的手段，一种中间语言对应了

一个翻译阶段，一个翻译阶段只完成部分Lustre算子的消

去工作。

清华大学L2C项目组于2010年开始着手研究Lustre

到Clight的可信代码生成器(简称L2C)，经过形式化验证

的L2C单时钟版本

[29]

代码生成器，成为Lustre可信代码生成器真正用于安全攸

关领域的关键一步。

参考文献：

[1]

Caspi P , Pilaud D , Halbwachs N , et al. LUSTRE: a declarative

language for real-time programming[C]// Proceedings of the

14th ACM SIGACT-SIGPLAN symposium on Principles of

programming ,1987.

Biernacki D , Jean-Louis Cola

ç

o, Gr

é

goire Hamon, et al.

Clock-directed modular code generation for synchronous data-

flow languages[C]// Proceedings of the 2008 ACM SIGPLAN/

SIGBED Conference on Languages, Compilers, and Tools for

Embedded Systems (LCTES'08), Tucson, AZ, USA, June 12-

13,,2008.

Champion A , Mebsout A , Sticksel C , et al. The Kind 2 Model

Checker[C]// International Conference on Computer Aided

Verification. Springer International Publishing,2016.

Halbwachs N , Lagnier F , Ratel C . Programming and

verifying real-time systems by means of the synchronous data-

flow language LUSTRE[J]. IEEE Transactions on Software

Engineering,1992,18(9):0-793.

Kahsai T , Tinelli C . PKIND: A parallel k-induction based model

checker[J]. 2011.

Caspi P , Pilaud D , Halbwachs N , et al. LUSTRE: a declarative

language for real-time programming[C]// Proceedings of the

14th ACM SIGACT-SIGPLAN symposium on Principles of

programming ,1987.

Chirica L M , Martin D F . An approach to compiler correctness[J].

Acm Sigplan Notices,1975,10(6):96-103.

John Mccarthy J P . Correctness of a compiler for arithmetic

expressions[J]. Proc. Sympos. Appl. Math. Vol. XIX, 1967:33--

41.

Moore J S . A mechanically verified language implementation[J].

Journal of Automated Reasoning,1989,5(4):461-492.

Wand M ,Oliva D P . Proving the correctness of storage represe-

已经实现了开源，在此基础上又为国

内某核电企业开发了多时钟版本

[30]

。Velus和L2C都是参

考了CompCert成功的技术路线，在Coq中利用定理证明技

术来进行形式化的开发。它们的目标语言Clight的形式化

定义也都是借鉴CompCert的定义。因此，L2C（开源版本）

的架构跟Velus非常相似，这里不再赘述。但它们还是存

在许多的不同，主要体现在支持的Lustre语言特性上。为

了结合实际工业控制领域的需要， L2C、SCADE等工具在

前述的Lustre语言特性的基础上，为了满足工业控制的需

要，又增加了一些如用于处理数组的高阶算子等特性。如

表1所示，为Velus、L2C（开源版本）和SCADE特性上的

比较。

[2]

[3]

[4]

4 结束语

Lustre的可信代码生成器的形式化开发方法包括翻译

验证和对代码生成器本身进行证明，翻译验证开发的核心

在验证器，开发方式较简单、重用性好，多用于代码生成

器的优化；定理证明是对代码生成器本身进行证明，是最

严格的形式化开发方式，经过此方式开发的代码生成器能

够达到人们所期望的最高的可信程度。未来在Lustre可信

代码生成器的形式化开发中，可考虑把两种开发方式结合

起来，把翻译验证作为对代码生成器本身进行证明的一种

补充，如在CompCert编译器开发中，就混合使用了这两种

方法，可以很好地平衡可靠性和工作量的问题。通过形式

化方法开发的Velus和L2C代码生成器还未真正实现商用，

主要用于学术研究。结合现有的学术成果和工业控制的需

求，完善适用于工业控制的算子，优化Lustre到C的可信

[9]

[10]

[7]

[8]

[5]

[6]

Copyright©博看网 . All Rights Reserved.

72

仪器仪表用户

INSTRUMENTATION

第27卷

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

ntations[J]. ACM SIGPLAN Lisp Pointers,1992,V(1):151-160.

Pnueli A .Translation validation[C]// International Conference on

Tools & Algorithms for the Construction & Analysis of Systems.

Springer Berlin Heidelberg,1998.

Li A P. Translation Validation: From SIGNAL to C[M].1999.

Pnueli A .Translation validation[C]//International Conference on

Tools &Algorithms for the Construction & Analysis of Systems.

Springer Berlin Heidelberg,1998.

Necula, George C .Translation validation for an optimizing

compiler[J].ACM SIGPLAN Notices,2000,35(5):83-94.

Pnueli A , Shtrichman O, Siegel Code Validation Tool

(CVT)[J]. International Journal on Software Tools for Technology

Transfer,1998, 2(2):192-201.

Ryabtsev M , Strichman O. Translation validation: from Simulink

to C.[C]// International Conference on Computer Aided

er-Verlag, 2009.

Necula,George ation validation for an optimizing

compiler[J]. ACM SIGPLAN Notices,2000,35(5):83-94.

Coq development team. The Coq proof ble at

/,1989{2009.

Yonezawa A , Hale R . Proving Compiler Correctness in a

Mechanized Logic R. Milner and R. Weyhrauch[J].Information

and Control,1974,26(4):396-397.

Leroy X . Formal verification of a realistic compiler[M].

ACM,2009.

Blazy S,Leroy ized Semantics for the Clight

Subset of the C Language[J].Journal of Automated

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

Reasoning,2009,43(3):263-288.

Leroy X .Formal certification of a compiler back-end, or:

programming a compiler with a proof assistant[J].Acm Sigplan

Notices,2006,41(1):42-54.

Leroy X .A formally verified compiler back-end[J]. Journal of

Automated Reasoning,2009,43(4):363.

Coupet-Grimal S , Jakubiec L . Hardware Verification Using Co-

induction in COQ[C]// Proceedings of the 12th International

Conference on Theorem Proving in Higher Order Logics.

Springer, Berlin, Heidelberg,1999.

S. Boulmé and G. Hamon. Certifying synchrony for free. In R.

Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th

International Conference on Logic for Programming, Artificial

Intelligence, and Reasoning (LPAR 2001) , volume 2250 of

Lecture Notes in Computer Science , pages 495–506, Havana,

Cuba, Dec. er.

E. Gimenez and E. Ledinot. Certification de SCADE V3. Rapport

final du project GENIE II, Verilog SA,Jan.2000.

BERTAILS A , BIERNACKI D , PAULIN C , et al. A certified

compiler for the synchronous language Lustre [EB/OL].

Bourke T , Lélio Brun, Dagand P E , et al. A Formally

Verified Compiler for Lustre[C]// Acm Sigplan Conference on

Programming Language Design & ,2017.

石刚,王生原,董渊,等.同步数据流语言可信编译器的构造[J].软

件学报, 2014(02):169-184.

尚书,甘元科,石刚,等.可信编译器L2C的核心翻译步骤及其设

计与实现[J].软件学报,2017(5).

（上接第31页）

2.4.13 服务器冗余切换检查

2.4.14 其它功能测试

在检修期间所有备用卡件都要上机测试。

4）如果某一通道出现故障，更换到备用通道，并更改

组态，做好记录。通道正常，将原接线复原。

3 结束语

霍尼韦尔DCS控制系统随着运行时间周期的加长，或

多或少都会出现软件及硬件的故障，但所有故障都万变不

离其中，只要在日常维护工作中做到细致谨慎、学习积累，

对所出现的系统故障进行分析、总结及归纳，就能够最大

化地实现控制系统的长周期稳定运行。

2.4.15 系统打点测试

对输入/输出卡件的精度进行检查测试，每卡按测量

点数20%的比例进行抽检。

1）模拟输入/输出点：拆除被测点接线，依次送入

量程的0%、50%、100%对应的信号，在操作站的点细目

画面、流程图画面观察并记录PV值，将结果填入记录单，

以测试卡的精度。

2）数字输入点：拆除被测点接线，用短接线短接槽路

或断开槽路，在操作站上观察记录状态值（ON或OFF），

将结果填入校验单。

3）数字输出点：拆除被测点接线，在操作站上置数字

输出点为ON或OFF状态，用万用表测通或断，将结果填

入校验单。

参考文献：

[1]

梁新光.DCS控制系统在调试和运行中出现的问题及处理方法

[J].大化科技,2010(01): 47-48.

[2]

崔守志.Experion PKS系统在净化装置中的应用[J].内蒙古石油

化工,2012(12):30-32.

[3]

霍尼韦尔中国自动化学院.Experion PKS中文参考手册[Z].2009.

Copyright©博看网 . All Rights Reserved.