李雨真

摘? 要： C語言具有良好的可移植性，適合于可編程控制器（Programmable Logical Controller，PLC）的嵌入式系統(tǒng)實現(xiàn)和研發(fā);而定時器在PLC系統(tǒng)負責時序邏輯描述，具有很重要的作用。文章著重研究如何將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 引言

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

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

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

1 ST語言中定時器建模

對ST語言中的定時器功能塊，本文通過對定時器特性的分析，提取出定時器的通性，抽象成一個含有時間信息的通用模型，再結合各個定時器特性，將其轉換成符合的時間自動機。

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

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

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

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

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

再將定時器內部計算過程模擬為變遷，通過改變變遷使能的順序，達到定時器輸入/輸出動作切換的目的，從而實現(xiàn)ST語言中定時器到時間自動機的轉換。

基于上述對ST定時器建模原理的闡述，結合IEC61131-3標準對定時器的定義，在建模實現(xiàn)過程中將定時器定義為結構體類型，如表1所示。IN為輸入的使能變量，PT為輸入的預設時間變量，ET為輸出的當前已計時間變量，Q為輸出的輸出值變量。

針對不同功能的定時器具體建模，從而得到各類定時器的時間自動機模型。本文以TON為例構建的定時器模型如圖2所示。

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

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

2.1 建模原理

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

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

IR用來表示指令的語法，可以翻譯為兩個位置l與l'之間的遷移，翻譯如表3所示。

如果對于所有的i≠j，，但是，所有條件構成的一個全集，即，從而所有的條件互斥。

2.2 建模結果

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

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

3 定時器驗證

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

在UPPAAL的驗證器中分別輸入表4中的驗證語句，結果如圖4所示。結果表明，針對定時器的ST語言程序與C語言程序所建立的時間自動機模型等價。

4 小結

本文針對PLC中的定時器展開研究，提出定時器中ST程序和C程序到時間自動機的轉換方法，并采用UPPAAL工具進行驗證，結果表明兩種語言描述的定時器是一致的。以UPPAAL為工具對時間自動機做模型檢測時，隨著時間自動機數(shù)量、時鐘變量的增多，驗證過程的復雜性將提高、耗時增加，甚至可能會導致驗證無法順利完成。因此，下一步工作重點是刻畫出ST語言轉時間自動機的優(yōu)化方法，使得在功能等價的情況下，狀態(tài)盡可能精簡，從而提高正確性驗證的效率。此外，我們還將進一步研究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] 彭瑜，何衍慶.智能制造工業(yè)控制軟件規(guī)范及其應用[M].機械工業(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] 溫世剛，羅繼亮，倪會娟等.基于普通Petri網(wǎng)的梯形圖中接通延時定時器的建模方法[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