李雨真

摘? 要： C語(yǔ)言具有良好的可移植性，適合于可編程控制器（Programmable Logical Controller，PLC）的嵌入式系統(tǒng)實(shí)現(xiàn)和研發(fā);而定時(shí)器在PLC系統(tǒng)負(fù)責(zé)時(shí)序邏輯描述，具有很重要的作用。文章著重研究如何將PLC結(jié)構(gòu)化文本（Structured Text，ST）語(yǔ)言中的定時(shí)器轉(zhuǎn)換為C語(yǔ)言程序的問(wèn)題。介紹了ST定時(shí)器時(shí)間自動(dòng)機(jī)模型的構(gòu)建，以及將該時(shí)間自動(dòng)機(jī)描述為C程序，并采用UPPAAL模型檢測(cè)工具進(jìn)行驗(yàn)證，從而保證轉(zhuǎn)換前后功能的一致性。

關(guān)鍵詞： 結(jié)構(gòu)化文本; 定時(shí)器; 時(shí)間自動(dòng)機(jī); UPPAAL

中圖分類(lèi)號(hào)：TP301.6? ? ? ? ? 文獻(xiàn)標(biāo)志碼：A? ? ?文章編號(hào)：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 引言

隨著電子技術(shù)的發(fā)展，嵌入式處理器的性能日益增強(qiáng)，逐漸達(dá)到PLC的性能要求。憑借著易于設(shè)計(jì)開(kāi)放式硬件架構(gòu)的優(yōu)點(diǎn)，以嵌入式處理器為核心的嵌入式可編程控制器（embedded Programmable Logic Control， ePLC）成為一種新型的PLC形態(tài)[1]。ePLC具有靈活的硬件結(jié)構(gòu)，使用簡(jiǎn)單且開(kāi)發(fā)周期短[2]，受到國(guó)內(nèi)外諸多研究人員的關(guān)注。C語(yǔ)言具有可移植性強(qiáng)的特點(diǎn)，且廣泛適用于嵌入式設(shè)備[3]，ST語(yǔ)言是一種類(lèi)似于PASCAL的高級(jí)編程語(yǔ)言[4]，將ST語(yǔ)言轉(zhuǎn)換為C語(yǔ)言能夠?yàn)閑PLC的實(shí)現(xiàn)和研發(fā)提供一種參考和借鑒意義。然而，ST語(yǔ)言支持時(shí)間類(lèi)型，且其中的定時(shí)器在PLC系統(tǒng)中負(fù)責(zé)時(shí)序邏輯描述，起著關(guān)鍵的作用。因此，本文著重研究ST語(yǔ)言中定時(shí)器轉(zhuǎn)換為C語(yǔ)言的問(wèn)題。

國(guó)內(nèi)外有關(guān)PLC中定時(shí)器的建模和驗(yàn)證工作在文獻(xiàn)[5-9]中提出，推進(jìn)了定時(shí)模塊在國(guó)內(nèi)外的研究進(jìn)展，但仍存在不足之處。文獻(xiàn)[5-6]提出基于時(shí)間自動(dòng)機(jī)的定時(shí)器建模方法，但驗(yàn)證復(fù)雜不易理解。文獻(xiàn)[7]提出一種基于特定布爾代數(shù)的驗(yàn)證方法。文獻(xiàn)[8]采用Coq工具驗(yàn)證定時(shí)器，該方法對(duì)用戶要求較高。文獻(xiàn)[9]采用普通Petri網(wǎng)對(duì)定時(shí)器建模，只分析邏輯錯(cuò)誤，未考慮時(shí)間信息。

綜上，本文提出一套針對(duì)定時(shí)器的ST程序與C程序到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換方法。方法的研究思路是采用時(shí)間自動(dòng)機(jī)分別對(duì)ST中定時(shí)器功能塊與轉(zhuǎn)換后的定時(shí)器C函數(shù)進(jìn)行建模，并使用UPPAAL工具驗(yàn)證轉(zhuǎn)換前后的一致性。

1 ST語(yǔ)言中定時(shí)器建模

對(duì)ST語(yǔ)言中的定時(shí)器功能塊，本文通過(guò)對(duì)定時(shí)器特性的分析，提取出定時(shí)器的通性，抽象成一個(gè)含有時(shí)間信息的通用模型，再結(jié)合各個(gè)定時(shí)器特性，將其轉(zhuǎn)換成符合的時(shí)間自動(dòng)機(jī)。

根據(jù)IEC61131-3標(biāo)準(zhǔn)規(guī)定，定時(shí)器主要分為以下三種：接通延遲定時(shí)器（TON）、斷電延遲定時(shí)器（TOF）和定時(shí)脈沖定時(shí)器（TP），且分辨率有1ms、10ms、100ms。定時(shí)器的時(shí)序圖如圖1所示。

通過(guò)分析定時(shí)器時(shí)序圖可知，當(dāng)定時(shí)器開(kāi)始工作時(shí)，當(dāng)前已計(jì)時(shí)間ET從0開(kāi)始線性增長(zhǎng)，當(dāng)達(dá)到預(yù)設(shè)時(shí)間PT時(shí)，保持ET等于PT。因此，可以根據(jù)當(dāng)前已計(jì)時(shí)間ET的變化將定時(shí)器抽象成時(shí)間自動(dòng)機(jī)，定時(shí)器可以分為三種狀態(tài)：初始狀態(tài)（ET=0）、工作狀態(tài)（0

⑴ 初始狀態(tài)Init。表示定時(shí)器不工作，初始化定時(shí)器各參數(shù)。

⑵ 工作狀態(tài)Work。表示定時(shí)器處于運(yùn)行時(shí)，時(shí)鐘開(kāi)始計(jì)時(shí)，且在該狀態(tài)下始終滿足ET處于范圍（0，PT）。

⑶ 輸出狀態(tài)Tout。表示ET=PT，改變定時(shí)器輸出值Q。

再將定時(shí)器內(nèi)部計(jì)算過(guò)程模擬為變遷，通過(guò)改變變遷使能的順序，達(dá)到定時(shí)器輸入/輸出動(dòng)作切換的目的，從而實(shí)現(xiàn)ST語(yǔ)言中定時(shí)器到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換。

基于上述對(duì)ST定時(shí)器建模原理的闡述，結(jié)合IEC61131-3標(biāo)準(zhǔn)對(duì)定時(shí)器的定義，在建模實(shí)現(xiàn)過(guò)程中將定時(shí)器定義為結(jié)構(gòu)體類(lèi)型，如表1所示。IN為輸入的使能變量，PT為輸入的預(yù)設(shè)時(shí)間變量，ET為輸出的當(dāng)前已計(jì)時(shí)間變量，Q為輸出的輸出值變量。

針對(duì)不同功能的定時(shí)器具體建模，從而得到各類(lèi)定時(shí)器的時(shí)間自動(dòng)機(jī)模型。本文以TON為例構(gòu)建的定時(shí)器模型如圖2所示。

2 C語(yǔ)言中定時(shí)器函數(shù)建模

對(duì)于定時(shí)器轉(zhuǎn)換后的C函數(shù)，本文采用中間形式的表示方法，將相應(yīng)的定時(shí)函數(shù)轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)。C語(yǔ)言中的定時(shí)器函數(shù)是根據(jù)定時(shí)器特性所實(shí)現(xiàn)的，這里以TON函數(shù)為例，該函數(shù)實(shí)現(xiàn)的偽代碼如表2。由于ST中功能塊的輸出結(jié)果是可以存取的，因此在C函數(shù)中輸出變量的類(lèi)型為指針數(shù)據(jù)類(lèi)型。函數(shù)體中的CurTime（）函數(shù)返回系統(tǒng)當(dāng)前時(shí)間。

2.1 建模原理

C程序到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換采用中間表示（Intermediate Representation， IR）的形式。根據(jù)時(shí)間自動(dòng)機(jī)語(yǔ)法和語(yǔ)義，IR具有滿足條件Ci（TA中的guard）和賦值A(chǔ)i（TA中的遷移）兩個(gè)表達(dá)式。賦值表達(dá)式Ai具有“v：=e”形式，其中v是變量，e是表達(dá)式。條件C和表達(dá)式e定義如下（其中◇為比較操作）：

每一個(gè)IR的表示形式及其相應(yīng)的平行分支形式如下。

IR用來(lái)表示指令的語(yǔ)法，可以翻譯為兩個(gè)位置l與l'之間的遷移，翻譯如表3所示。

如果對(duì)于所有的i≠j，，但是，所有條件構(gòu)成的一個(gè)全集，即，從而所有的條件互斥。

2.2 建模結(jié)果

根據(jù)建模原理可知，當(dāng)遇到分支語(yǔ)句時(shí)，將分支語(yǔ)句的判斷條件作為遷移的guard值，條件成立后的賦值語(yǔ)句作為遷移的update值。從表2描述的TON函數(shù)偽代碼可以看出，函數(shù)體共有2個(gè)IF語(yǔ)句，根據(jù)IR方法可以得出TON的平行分支表達(dá)形式如下：

讀取TON平行分支表達(dá)，并將其轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)。根據(jù)上述原理，所構(gòu)建的C函數(shù)中TON的時(shí)間自動(dòng)機(jī)如圖3所示。

3 定時(shí)器驗(yàn)證

UPPAAL工具提供了強(qiáng)大的模擬器和驗(yàn)證器[10]，可以在驗(yàn)證器中利用時(shí)序邏輯TCTL來(lái)驗(yàn)證一些關(guān)注的性質(zhì)。因此，本文采用該工具驗(yàn)證定時(shí)器轉(zhuǎn)換前后功能的一致性，驗(yàn)證標(biāo)準(zhǔn)為：當(dāng)C程序中定時(shí)器函數(shù)所對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)到達(dá)（未到達(dá)）最終狀態(tài)T時(shí)，ST定時(shí)器對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)也到達(dá)（未到達(dá)）最終狀態(tài)Tout。所使用的性質(zhì)驗(yàn)證語(yǔ)句如表4所示。

在UPPAAL的驗(yàn)證器中分別輸入表4中的驗(yàn)證語(yǔ)句，結(jié)果如圖4所示。結(jié)果表明，針對(duì)定時(shí)器的ST語(yǔ)言程序與C語(yǔ)言程序所建立的時(shí)間自動(dòng)機(jī)模型等價(jià)。

4 小結(jié)

本文針對(duì)PLC中的定時(shí)器展開(kāi)研究，提出定時(shí)器中ST程序和C程序到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換方法，并采用UPPAAL工具進(jìn)行驗(yàn)證，結(jié)果表明兩種語(yǔ)言描述的定時(shí)器是一致的。以UPPAAL為工具對(duì)時(shí)間自動(dòng)機(jī)做模型檢測(cè)時(shí)，隨著時(shí)間自動(dòng)機(jī)數(shù)量、時(shí)鐘變量的增多，驗(yàn)證過(guò)程的復(fù)雜性將提高、耗時(shí)增加，甚至可能會(huì)導(dǎo)致驗(yàn)證無(wú)法順利完成。因此，下一步工作重點(diǎn)是刻畫(huà)出ST語(yǔ)言轉(zhuǎn)時(shí)間自動(dòng)機(jī)的優(yōu)化方法，使得在功能等價(jià)的情況下，狀態(tài)盡可能精簡(jiǎn)，從而提高正確性驗(yàn)證的效率。此外，我們還將進(jìn)一步研究ST語(yǔ)言中其他功能塊的驗(yàn)證及實(shí)際應(yīng)用。

參考文獻(xiàn)（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] 彭瑜，何衍慶.智能制造工業(yè)控制軟件規(guī)范及其應(yīng)用[M].機(jī)械工業(yè)出版社，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] 溫世剛，羅繼亮，倪會(huì)娟等.基于普通Petri網(wǎng)的梯形圖中接通延時(shí)定時(shí)器的建模方法[J].計(jì)算機(jī)科學(xué)，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