一种PLC程序语言指称语义及函数的形式化定义方法

肖力田^{1, 2}，顾明¹，孙家广¹

(1. 清华大学 软件学院 信息科学与技术国家实验室，

信息系统安全教育部重点实验室，计算机科学与技术系，北京，100084；

2. 北京特种工程设计研究院，北京，100028)

摘要：为了使用形式化方法对PLC程序的正确性验证奠定基础，研究PLC程序语言的指称语义定义, 以实现对PLC形式化定义和检测验证。基于程序建模，定义了PLC 程序指称语义的格局、程序语言的语义函数及函数，为其模型检测和定理证明提供了基础。

关键词：PLC程序；扩展λ-演算；程序建模；指称语义

中图分类号：TP301.2          文献标志码：A         文章编号：1672-7207(2011)S1-1107-07

Formal definition method of denotational semantics and functions for PLC program language

XIAO Li-tian^{1, 2}, GU Ming¹, SUN Jia-guang¹

(1. National Laboratory for Information Science and Technology,

Key Laboratory for Information System Security of Ministry of Education,

Department of Computer Science and Technology, School of Software, Tsinghua University, Beijing 100084, China;

2. Beijing Special Engineering Design and Research Institute, Beijing 100028, China)

Abstract: In order to verify the correctness of PLC programs by formal methods, the definition of denotational semantics on PLC program language was studied to achieve PLC programs modeling and model checking. Based on the extended λ-calculus definition, the configuration of PLC program architecture, denotational semantics of PLC programs and functions of denotational semantics were defined, which proves the basis of model checking and theorem.

Key words: PLC program; λ-calculus definition; program modeling; denotational semantics

随着嵌入式应用需求的不断增加，PLC 程序日益变得复杂，其规模也变得愈加庞大。嵌入式系统在安全攸关领域有着广泛的应用，因此，对其正确性保障有较高需求。虽然就 PLC 本身而言，其底层的硬件逻辑可靠性高，但由于其程序功能的复杂性，PLC的正确性难以保证。

为了尽可能的排除程序的缺陷和验证程序正确性，目前主要采用的是测试方法^[1-3]和形式化验证方法。虽然测试技术是一种有效的发现程序错误的手段，但是，这种方法具有不完全性，很难使用有限的测试用例完全覆盖程序所有的(可达)代码。因此，研究人员试图使用形式化方法对程序进行正确性验证。一类是模型检测方法，即在抽象模型上针对指定性质(例如安全性、活性等)，通过状态空间搜索进行验证的方法， 这类方法是可靠和完全的，但它面临的最大问题在于“状态空间爆炸”^[4-6]。另外一类是基于定理证明的验证方法，用一系列的逻辑公式来刻画系统的行为特征，而后借助于逻辑系统(或者证明工具)提供的推理规则，通过演绎的方法证明或者证伪既定的目标。还有一类是定理证明方法，十分适合于无穷状态系统的验证。因为多数的证明工具(例如PVS^[7]，Coq^[8]和Nqthm^[9]等)所提供的基础逻辑是高阶逻辑，它们具有刻画无穷数据结构的能力，即对于状态空间的规模不敏感，只是这类方法对于验证人员的要求相对较高。

对于 PLC 程序而言，其验证问题具有以下特点：

(1) PLC 程序大多数用于嵌入式硬件环境，因此其逻辑结构相对简单，程序中语句种类少，程序相对短小。

(2) PLC 程序采用硬件机器指令编写(或者使用梯形图表示)，因此便于模型的抽象过程，甚至有些时候直接可以作为模型进行验证(类似于汇编语言、Verilog和VHDL等)。

(3) PLC 程序虽然简单，但是它仍然具有高级程序设计语言的大部分机制。

(4) PLC 程序在一个扫描周期内顺序执行完毕，而后刷新输出映像，进而执行下一个扫描周期。从1个扫描周期内部看，它具有顺序程序的特征；从全扫描周期看，PLC 展示的是对于不同输入信号的输出响应，并且这种响应不是固定的。由于各种定时器、计数器的累积是跨扫描周期的，1个PLC程序不能单纯的看作是固定的输入-输出转化逻辑。

因此，与普通的高级语言程序/汇编语言的验证相比，PLC 程序的验证有其优势，即规模相对较小，结构相对简单，控制逻辑更加清晰，更贴近数学表示。

为了对PLC程序进行正确性验证，检验PLC跨扫描周期的时序性质，本文作者开展了基于定理证明器Coq的验证方法研究，对PLC程序进行建模，利用扩展的λ-演算定义典型PLC 程序的指称语义，即从输入格局到输出格局的映射函数，从而实现从 PLC 程序到符号迁移系统的转化和针对 PLC 程序的 Coq 验证。

1  PLC程序体系结构的定义

1.1  工作模式、系统组成和PLC主要编程指令

PLC 采用循环扫描的工作方式。在运行时，每个扫描周期分为内部处理、编程器通信、输入扫描、程序执行和输出处理共5个阶段。其内中部处理阶段和编程器通信阶段是2个辅助的阶段。在输入采样阶段，CPU 会依次从各个输入端口进行数据采集，并存入映像区单元中。在该阶段，映像区的寄存器状态被刷新，而后将输入、输出端口的状态锁存。

PLC的程序执行阶段与普通程序相同，外部输入信号的改变不会对程序的执行产生影响。因为在输入采样阶段的末尾，已经将输入端口的状态锁定。在输出处理阶段，用输出元件寄存器的状态将对应的输出锁存器进行刷新，从而改变输出端的状态，驱动控制与之连接的电子器件。

PLC系统硬件设备组成的主要单元^[10]有输入继电器单元(X)、输出继电器单元(Y)、辅助继电器单元(M)、状态寄存器(S)、定时器(T)、计数器(C)、数据寄存器(D)和PLC 指针(P)等。主要指令^[10]有常开/常闭触点与母线连接(输入输出：LD/LDI)、与常开/常闭触点进行串联连接(AND/ANDI)、与常开/常闭触点进行并联连接(OR/ORI)、块操作(ANDB/ORB)、取反(INV)、特定元件置 1/0并保持(SET/RST)、空操作(NOP)、主程序结束(END)、步进(STL或RET)、压栈/读栈/弹栈操作(MPS/MRD/MPP)、条件跳转(CJ)、循环(FOR…NEXT)、子程序调用/返回(CALL/SRET)、算术运算(ADD，SUB，MUL，DIV，INC，DEC)、按位逻辑运算(WAND，WOR，WXOR，NEG)、比较(CMP)和数据传送(MOV)等。

详细的硬件和PLC指令可参考相关手册。PLC  中还提供了若干其他的命令，例如编译、高速处理等，但与验证关系不大，在此不进行讨论。

1.2  PLC程序的体系结构

对PLC 程序体系结构进行精确的数学描述如下。

(1) 为每个输入/输出继电器单元、辅助继电器单元、状态寄存器 Z引入一个变元V_z∈{0,1}。例如，输入单元 X0 对应V_X0，输出单元 Y2 对应V_Y2，辅助继电器 M2 对应V_M2 等。

(2) 为每个数据寄存器单元、每个计数器单元D引入一个对应的变元 V_D∈N(自然数域)。

(3) 将指针值(例如子程序跳转入口地址，条件跳转语句地址)视为常量。

(4) 由于本文的验证技术不涉及实时问题，因此不考虑定时器的数学描述问题。

(5) 上述变元分为两类：全局变元和局部变元。其中，被SET/RST 命令作用的单元以及计数器单元作为全局变元，其余作为局部变元。分别记GV和LV 为全局变元和局部变元构成的集合。

(6) 此外，对于计数器单元，由于需要一个预定的计数值，并且该值可以多次设置，因此为每个计数器 C设置一个临时变元E_c。该变元的值受OUT指令影响。例如：OUT C0 K200，则E_c 被赋为200。

(7) 由于存在栈操作，需要一个用来记录目前母线栈变化的结构 S_M∈{0,1}^*。考虑下列代码：

假设V_X0=1, V_X1=1, V_X2=0, V_X3=1，那么，在执行完上述代码处栈的值分别为：ε, 1, 1, 1, 1, 1, 1.0, 1.0, 1。其中，空串ε表示的意义为栈为空。

此外，有大量类似于AND/OR/ANDB/ORB/ANDI/ ORI指令的执行结果依赖于当前母线的连通状况；同时，这些指令的执行本身也会改变当前母线的连通。并且块并联/串联命令依赖于若干步之前的母线连通状况。因此，有必要为母线的当前连通状况设置一   个栈。

用一个四元偶CF=<ω_M, ω_T, σ_G, σ_L>来表示当前的一个格局。其中，ω_M和ω_T分别为母线栈和当前连通栈；σ_G和σ_L分别为全局变量和局部变量赋值(指派)函数，即每个全局变量V的当前值被指派为 σ_G(V)；每个局部变量V的值被指派为σ_L(V)。

由于格局中存在栈结构，下面给出其上的若干操作和相关函数定义：给定字母表Σ，其上的一个栈是该字母表上的一个有穷字ω∈Σ^*。用空字母ε表示空栈。用ω⁰表示ω的首字母，称为ω 的栈顶；若ω= a₁·a₂·…·a_n，则用ω′表示栈a₂·…·a_n，即ω′是ω将栈顶元素弹出后得到的栈，以此类推；用 a₀·ω表示向ω压入a₀后得到的新栈，引入缩写ω¹=(ω′)⁰, ω²=(ω′)¹= (ω″)⁰, …，等等。

习惯上，一般用V等符号(可能带有下标)表示变元；用 C 等符号(可能带有下标)表示常元。为了给出 PLC 程序的指称语义，引入下列以BNF 范式表示的表达式：

e::=V|C|e+e|e-e|e×e|e÷e|ee|ee|ee|

?e|e&e|e|e|e^e|ē

其中：符号 +，-，×和÷分别对应算术运算加、减、乘、除；符号，，和?分别对应逻辑运算与、或、非；符号&，|，^和?分别对应于位运算的位与、位或、位异或。

给定格局 CF=<ω_M, ω_T, σ_G, σ_L>，一个表达式 e 在该格局下的语义值，记作?e?_CF，归纳定义如下：

(1)?C?_CF=C。

(2)?V?_CF=。

(3)?e₁*e₂?_CF=e₁?_CF*e₂?_CF，其中 *∈{+，-，×，÷，，，，&，|，^}，其运算定义同常。

(4)?!e?_CF =!?e?_CF，其中!∈{?，?}，其运算定义同常。

2  PLC程序的指称语义定义

2.1  PLC程序语句块的划分与定义

将数据域限定为自然数域N，用C和C_i(i=1，2，…) 表示自然数常量(有符号)，用 V和V_j (j=1, 2, …)表示值为自然数的变量/变元；用c和c_i (i=1, 2, …)等表示常向量(序偶)，用V和V _j (j=1, 2, …)等表示变向量(序偶)。

引入一个常量⊥，它表示“未定义值”。此外，定义一个“平板偏序”，并且规定：对于任意的自然数 C，都有⊥AC成立；但是，两个自然数之间关于该偏序不可比，如图1所示。这里的关系是自反的。该偏序关系可以自然的提升至序偶(元组)、串、以及函数上。例如，对于序偶，有(⊥, 5)A(3, 5), (3,⊥)A(3, 5), (⊥,⊥)A(⊥, 5), (⊥,⊥)A(3,⊥)等。对于串，有0·⊥·3<0·1·3等。对于函数而言，F₁AF₂ 当且仅当X. F₁(X) AF₂ (X)成立。

图1  自然数上平板偏序

Fig.1  Flat partial order on natural number

用N_⊥表示集合N∪{⊥}，可以进一步将A提升至由N_⊥上的表、(多元)函数构成的序偶上。一般用 X, X_i (i=1, 2, …)表示这样的一个序偶。显然，每个格局都是一个这样的序偶。

将一个完整的PLC语句按照语句块进行结构划分(总是假设子程序调用语句已经被等价的展开，步进指令已经转化为等价的母线操作指令)，将其归为4类：

(1) 基本语句块：只包含1条 PLC 指令的语句块；

(2) 顺序合成语句块：由若干语句块顺序合成构成的语句块；

(3) 分支语句块：由JC 语句引导的指令块(如图2的形式)，其中Cod₁和Cod₂都是指令块；

(4) 循环语句块：由FOR语句引导的指令块(如图3的形式)，其中Cod是1个指令块。

对于每个(合式的)语句块Cod而言，其指称语义M(Cod)是一个函数，它将一个格局映射为另一个格局。即：若语句块Cod在执行之前的格局为CF，则其执行后(若能正常结束)的格局为 M(Cod)(CF)。为给出M(Cod)的形式定义，使用扩展的λ-演算为工具，该演算的语法定义如下：

F::=X|Φ|[λX.F]|F○F|F(F)|X?F:F|μΦ.F

式中：Ф是函数变元，[λX.F]为λ-抽象，F₁○F₂为函数的合成，这里假定F₂的输出类型与F₁的输入类型匹配；F₁(F₂)为函数的应用，这里只允许F₂的类型与F₁的输入类型相同的情况；X?F₁:F₂为带条件选择函数，这里只允许XN_ω的情况, 即：若XN\{0}，则函数等价于F₁，否则，函数等价于F₂；μΦ.F为最小不动点，这里一般要求Φ在F 中有出现。

图2  分支语句块

Fig.2  Branch statement block

图3  循环语句块

Fig.3  Loop statement block

计算形如μΦ.F 的过程一般采用Kleen 迭代，即计算方程Φ≡F(Φ)的最小不动点(相对于偏序A)，其过程如下：

(1) 令F₀=F_⊥，即整个函数值为⊥的函数；

(2) 令F_i+1=F[Φ/F_i]，即将F中的Φ用F_i代入；

(3) 若F_k=F_k+1，则停止迭代，令μΦ.F= F_k。

对于平板偏序而言，由于每个链都是有穷链，可以证明上述迭代必然在有穷步内终止。

此外，由于语义函数是从格局到格局的转换映射，因此函数的输入都是一个格局<ω_M, ω_T, σ_G, σ_L>。λ-表达式采用简写：λ<ω_M, ω_T, σ_G, σ_L>.F=λx.let x:=<ω_M, ω_T, σ_G, σ_T>.in F

下面给出 M(Cod)的定义。首先讨论顺序合成语句、条件分支以及循环语句的情形：

(1) 顺序合成：若Cod=Cod₁Cod₂，则M(Cod)= M(Cod₂)○M(Cod₁)；

(2) 分支语句：若Cod=JC L; Cod₁; L: Cod₂，则 M(Cod)=ω_T⁰?M(Cod₂):M(Cod₁ Cod₂)。

(3) 循环语句：若Cod=FOR D; Cod₁; NEXT, 且 D为(数据)寄存器名时，有：

M(Cod)=μΦ.(λCF.?V_D?_λCF?

Φ○M(DEC D)○M(Cod₁)(<ω_M, ω_T, σ_G, σ_L>):

<ω_M, ω_T, σ_G, σ_L>)

当D为常数时，有：M(Cod)=(M(Cod₁))^D, 即：M(Cod₁)自身合成D次。

2.2  基本语句块的指称语义函数

下面研究基本语句块的指称语义函数，对各种语句进行分情况讨论。

2.2.1  输入输出指令LD/LDI

若 Cod=LD   Z  (Z=X0，X1，M0，M1，…，下同)，则

M(Cod)=

即将V_Z的当前值压入连通栈。

若Cod=LDI   Z，则

M(Cod)=

即将V_Z的当前值取反后压入连通栈，上述是Z不为计数器单元的情形。否则，需要将σ_G(V_z)替换为。以下在讨论串联/并联指令时，均依此处理。

2.2.2  串联指令AND/ANDI

若Cod=AND Z，则

M(Cod)=

即将连通栈的栈顶值与V_Z进行与操作后的值压栈。这里需要说明的是如果ω_T是空栈，则的值视为1(下同)。

若Cod=ANDI  Z，则

M(Cod)=

2.2.3  并联指令OR/ORI

若Cod=OR  Z，则

M(Cod)=

若Cod=ORI  Z，则

M(Cod)=

 

2.2.4  块操作指令ANDB/ORB

若Cod=ANDB，则：

M(Cod)=

若Cod=ORB，则：

M(Cod)=

2.2.5  取反指令INV

若Cod=INV，则：

M(Cod)=

2.2.6  输出指令OUT

当Cod为输出指令OUT  Z时，它的情况比较复杂，需要区分目标寄存器的类型。

(1)     若V_Z是局部变元，则：

M(Cod)=

即将当前连通栈的值置为母线栈的栈顶值，将Z的值设为当前连通栈的栈顶值。这里，是一个新的函数，满足：

=

(2) 若V_Z是非计数器全局变元，则

M(Cod)=

这是因为这种单元由SET/RST指令作用，OUT指令并不能改变其值。

(3) 若Cod=OUT  Z  C，其中Z为增计数器单元，C为某个常量，则

M(Cod)=

(4) 若Cod=OUT  Z  C，其中Z为某减计数器单元，C为某个常量，则

M(Cod)=

式中：Z'是Z对应的辅助寄存器。

2.2.7  置1/0并保持指令SET/RST

若Cod=SET   Z，则

若Cod=RST  Z，则

2.2.8  空操作/主程序结束指令NOP/END

若Cod=NOP，则

M(Cod)=

 

若Cod=END，则

M(Cod)=

即END 指令具有恢复母线栈和连通栈的功能。

2.2.9  栈操作指令MPS/MRD/MPP

若Cod=MPS，则

M(Cod)=

即将当前连通栈的栈顶值压入母线栈。

若Cod=MRD，则

M(Cod)=

即将当前连通栈的内容替换为母线栈的内容。

若Cod=MPP，则

M(Cod)=

即该命令与MRD唯一的不同之处在于还要对母线栈执行一次弹栈操作。

2.2.10  算术运算指令ADD/SUB/MUL/DIV/INC/DEC与逻辑运算指令WAND/WOR/WXOR/NEG

(1) 若Cod=ADD Z1 Z2 Z，则

(2) 若Cod=SUB Z1 Z2 Z，则

(3) 若Cod=MUL Z1 Z2 Z，则

(4) 若Cod=DIV Z1 Z2 Z，则

。

(5) 若Cod=INC  Z，则

(6) 若Cod=DEC Z，则

(7) 若Cod=WAND Z1 Z2 Z，则

(8) 若Cod=WOR Z1 Z2 Z，则

(9) 若Cod=WXOR Z1 Z2 Z，则

(10) 若Cod=NEG Z，则

上述只讨论Z1和Z2对应的变元均为局部变元的情形，为全局变元时，只要将相应的σ_L替换为σ_G即可。但是，在Z相邻的后2个寄存器单元为Z′ 和Z′′情况下，要求V_Z，和一定是局部变元，否则它的值不会在这种语句中发生变化。

此外，应当注意算术/逻辑操作能够执行的前提是当前处于使能状态，也就是连通栈栈顶为1。最后，所有的算数/逻辑操作一定是梯形图中行结束时的命令，因此它兼有OUT指令的功能，将当前连通栈的内容更新为当前母线栈的栈顶元素的值。

2.2.11  比较/数据传输指令CMP/MOV

若Cod=CMP Z1 Z2 Z，且与Z相邻的后2个寄存器单元为Z′和Z″，则

若Cod=ZCP Z1 Z2 Z3 Z，且与Z相邻的后两个寄存器单元为Z′和Z″，并且，则

这里只写出了V_Z1，V_Z2和V_Z3为局部变元的情况。但是同样要求V_Z，V_Z′和V_Z″一定是局部变元。

若Cod=MOV C Z，且C为常数，则

若Cod=MOV Z′ Z，且Z′是存储单元，则

 

同样，当V_Z′是全局变元时，只需将式中的σ_L(V_Z′)替换为σ_G(V_Z′)即可。

3  结论

(1) 以典型的 PLC 为例，抽象描述 PLC 的系统组成、体系结构和工作方式等，以及主要的PLC 命令的语法、语义和程序的主要构成。

(2) 基于扩展的λ-演算，给出PLC 程序的指称语义，是PLC程序验证和定理证明的基础。在给出 PLC 程序的指称语义之后，进一步研究将其转化成为其他的数学模型，以及基于Coq定理证明中需要的Gallina描述等。

参考文献：

[1] Zipori H, Yossovitch A. Approaches and implementation of software test and development system for embedded computer systems[J]. Embedded System Design, 2005, 35(6): 30-39.

[2] Lee E A. Computing for embedded systems[C]//Proceeding of IEEE Instrumentation and Measurement Technology Conference. Budapest, Hungary: Piscataway, N.J.: IEEE, 2001: 100-105.

[3] Kang B, Kwon Y J, Lee R Y. A design and test technique for embedded software[C]//Proceedings of the 2005 Third ACIS Int’l Conference on Software Engineering Research, Management and Applications, Washington D C, US: IEEE Computer Society, 2005: 160-165.

[4] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic [C]//Kozen D, eds. Logic of Programs. London, UK: Springer- Verlag. 1982, 131: 52-71.

[5] Queille J P, Sifakis J. Specification and verification of concurrent systems[C]//LNCS: International Symposium on Programming. London, UK: Springer-Verlag. 1982, 137: 216-230.

[6] Lamport L. Proving the correctness of multiprocess programs[J]. IEEE Trans on Software Engineering, 1977, 3(2): 125-143.

[7] Owre S, Rajan S P. Rushby J M, et al. PVS: combining specifications, proof checking and model checking[C]//Alur R, Henzinger T A, ed. LNCS: CAV’96. London, UK: Springer- Verlag. 1996: 411-414.

[8] The Coq toolkit. http://coq.inria.fr/.

[9] Boyer R S, Moore J S. Proving theorems about lisp functions[J]. Journal of the ACM, 1975, 22(1): 129-144.

[10] Karl-Heinz John, Michael Tiegelkamp. IEC 61131-3: Programming Industrial Automation Systems. Berlin Heidelberg: Springer-Verlag, 2001.

(编辑 方京华)

收稿日期：2011-04-15；修回日期：2011-06-15

基金项目：国家自然科学基金资助项目(90718039, 91018015, 60811130468)；国家重大基础研究计划(“973”计划)项目(2010CB328003)

通信作者：肖力田(1961-)，男，上海人，研究员，从事软件验证研究；电话: 010-66358506；E-mail: xlt05@mails.tsinghua.edu.cn