李雨真

摘  要： C语言具有良好的可移植性，适合于可编程控制器（Programmable Logical Controller，PLC）的嵌入式系统实现和研发;而定时器在PLC系统负责时序逻辑描述，具有很重要的作用。文章着重研究如何将PLC结构化文本（Structured Text，ST）语言中的定时器转换为C语言程序的问题。介绍了ST定时器时间自动机模型的构建，以及将该时间自动机描述为C程序，并采用UPPAAL模型检测工具进行验证，从而保证转换前后功能的一致性。

关键词： 结构化文本; 定时器; 时间自动机; UPPAAL

中图分类号：TP301.6          文献标志码：A     文章编号：1006-8228（2019）06-12-04

Abstract： Having good portability， C language is suitable for realizing and developing the embedded system of programmable logical controller. And timer is responsible for sequential logic description and plays an important role in PLC system. This article focuses on how to convert the timer in PLC structured text （ST） language into C language. The construction of ST timer time automata model is introduced， and the model is described with C language program. The model checker UPPAAL is used for verification to ensure the consistency of functions before and after the conversion.

Key words： structured text; timer; timed automata; UPPAAL

0 引言

随着电子技术的发展，嵌入式处理器的性能日益增强，逐渐达到PLC的性能要求。凭借着易于设计开放式硬件架构的优点，以嵌入式处理器为核心的嵌入式可编程控制器（embedded Programmable Logic Control， ePLC）成为一种新型的PLC形态[1]。ePLC具有灵活的硬件结构，使用简单且开发周期短[2]，受到国内外诸多研究人员的关注。C语言具有可移植性强的特点，且广泛适用于嵌入式设备[3]，ST语言是一种类似于PASCAL的高级编程语言[4]，将ST语言转换为C语言能够为ePLC的实现和研发提供一种参考和借鉴意义。然而，ST语言支持时间类型，且其中的定时器在PLC系统中负责时序逻辑描述，起着关键的作用。因此，本文着重研究ST语言中定时器转换为C语言的问题。

国内外有关PLC中定时器的建模和验证工作在文献[5-9]中提出，推进了定时模块在国内外的研究进展，但仍存在不足之处。文献[5-6]提出基于时间自动机的定时器建模方法，但验证复杂不易理解。文献[7]提出一种基于特定布尔代数的验证方法。文献[8]采用Coq工具验证定时器，该方法对用户要求较高。文献[9]采用普通Petri网对定时器建模，只分析逻辑错误，未考虑时间信息。

综上，本文提出一套针对定时器的ST程序与C程序到时间自动机的转换方法。方法的研究思路是采用时间自动机分别对ST中定时器功能块与转换后的定时器C函数进行建模，并使用UPPAAL工具验证转换前后的一致性。

1 ST语言中定时器建模

对ST语言中的定时器功能块，本文通过对定时器特性的分析，提取出定时器的通性，抽象成一个含有时间信息的通用模型，再结合各个定时器特性，将其转换成符合的时间自动机。

根据IEC61131-3标准规定，定时器主要分为以下三种：接通延迟定时器（TON）、断电延迟定时器（TOF）和定时脉冲定时器（TP），且分辨率有1ms、10ms、100ms。定时器的时序图如图1所示。

通过分析定时器时序图可知，当定时器开始工作时，当前已计时间ET从0开始线性增长，当达到预设时间PT时，保持ET等于PT。因此，可以根据当前已计时间ET的变化将定时器抽象成时间自动机，定时器可以分为三种状态：初始状态（ET=0）、工作状态（0

⑴ 初始状态Init。表示定时器不工作，初始化定时器各参数。

⑵ 工作状态Work。表示定时器处于运行时，时钟开始计时，且在该状态下始终满足ET处于范围（0，PT）。

⑶ 输出状态Tout。表示ET=PT，改变定时器输出值Q。

再将定时器内部计算过程模拟为变迁，通过改变变迁使能的顺序，达到定时器输入/输出动作切换的目的，从而實现ST语言中定时器到时间自动机的转换。

基于上述对ST定时器建模原理的阐述，结合IEC61131-3标准对定时器的定义，在建模实现过程中将定时器定义为结构体类型，如表1所示。IN为输入的使能变量，PT为输入的预设时间变量，ET为输出的当前已计时间变量，Q为输出的输出值变量。

针对不同功能的定时器具体建模，从而得到各类定时器的时间自动机模型。本文以TON为例构建的定时器模型如图2所示。

2 C语言中定时器函数建模

对于定时器转换后的C函数，本文采用中间形式的表示方法，将相应的定时函数转换为时间自动机。C语言中的定时器函数是根据定时器特性所实现的，这里以TON函数为例，该函数实现的伪代码如表2。由于ST中功能块的输出结果是可以存取的，因此在C函数中输出变量的类型为指针数据类型。函数体中的CurTime（）函数返回系统当前时间。

2.1 建模原理

C程序到时间自动机的转换采用中间表示（Intermediate Representation， IR）的形式。根据时间自动机语法和语义，IR具有满足条件Ci（TA中的guard）和赋值Ai（TA中的迁移）两个表达式。赋值表达式Ai具有“v：=e”形式，其中v是变量，e是表达式。条件C和表达式e定义如下（其中◇为比较操作）：

每一个IR的表示形式及其相应的平行分支形式如下。

IR用来表示指令的语法，可以翻译为两个位置l与l'之间的迁移，翻译如表3所示。

如果对于所有的i≠j，，但是，所有条件构成的一个全集，即，从而所有的条件互斥。

2.2 建模结果

根据建模原理可知，当遇到分支语句时，将分支语句的判断条件作为迁移的guard值，条件成立后的赋值语句作为迁移的update值。从表2描述的TON函数伪代码可以看出，函数体共有2个IF语句，根据IR方法可以得出TON的平行分支表达形式如下：

读取TON平行分支表达，并将其转换为时间自动机。根据上述原理，所构建的C函数中TON的时间自动机如图3所示。

3 定时器验证

UPPAAL工具提供了强大的模拟器和验证器[10]，可以在验证器中利用时序逻辑TCTL来验证一些关注的性质。因此，本文采用该工具验证定时器转换前后功能的一致性，验证标准为：当C程序中定时器函数所对应的时间自动机到达（未到达）最终状态T时，ST定时器对应的时间自动机也到达（未到达）最终状态Tout。所使用的性质验证语句如表4所示。

在UPPAAL的验证器中分别输入表4中的验证语句，结果如图4所示。结果表明，针对定时器的ST语言程序与C语言程序所建立的时间自动机模型等价。

4 小结

本文针对PLC中的定时器展开研究，提出定时器中ST程序和C程序到时间自动机的转换方法，并采用UPPAAL工具进行验证，结果表明两种语言描述的定时器是一致的。以UPPAAL为工具对时间自动机做模型检测时，随着时间自动机数量、时钟变量的增多，验证过程的复杂性将提高、耗时增加，甚至可能会导致验证无法顺利完成。因此，下一步工作重点是刻画出ST语言转时间自动机的优化方法，使得在功能等价的情况下，状态尽可能精简，从而提高正确性验证的效率。此外，我们还将进一步研究ST语言中其他功能块的验证及实际应用。

参考文献（References）：

[1] Ahmed I， Obermeier S， Sudhakaran S， et al. Programma-ble Logic Controller Forensics[J]. IEEE Security & Privacy，2017.15（6）：18-24

[2] Alves T， Das R， Morris T. Embedding Encryption and Machine Learning Intrusion Prevention Systems on Programmable Logic Controllers[J]. IEEE Embedded Systems Letters， 2018.10（3）：99-102

[3] Bispo J， Cardoso J M P. A MATLAB subset to C compilertargeting embedded systems[J]. Software： Practice and Experience，2017.47（2）： 249-272

[4] 彭瑜，何衍庆.智能制造工业控制软件规范及其应用[M].机械工业出版社，2018.

[5] Mader A， Wupper H. Timed automaton models for simpleprogrammable logic controllers[C]// Euromicro Conference on Real-time Systems. CiteSeer，1999.

[6] Zhou M， He F， Gu M， et al. Translation-Based Model Checking for PLC Programs[C]// 2009 33rd Annual IEEE International Computer Software and Applications Conference. IEEE Computer Society，2009.

[7] Roussel J M ， Faure J M . An algebraic approach for PLC programs verification[C]// International Workshop on Discrete Event Systems. IEEE，2002.

[8] Wan H， Chen G， Song X， et al. Formalisation andverification of programmable logic controllers timers in Coq[J]. IET software，2011.5（1）：32-42

[9] 溫世刚，罗继亮，倪会娟等.基于普通Petri网的梯形图中接通延时定时器的建模方法[J].计算机科学，2014.41（7）：153-156

[10] David A， Larsen K G， Legay A， et al. Uppaal SMC tutorial[J]. International Journal on Software Tools for Technology Transfer，2015.17（4）：397-415