一種可編程邏輯控制程序的競態檢測方法

黃穎坤，羅繼亮

（華僑大學 信息科學與工程學院，福建 廈門361021）

梯形圖具有形象、直觀、實用等特點，是目前使用最多的一種可編程邏輯控制器（programmable logic controller，PLC）的編程語言［1］.但是，梯形圖容易產生競態，而競態很難用傳統的方法檢測出來［2］，且驗證程序的正確性需要極大的代價，動輒就是上百萬美元.由于驗證需要耗費大量時間，使得工廠、企業長時間停工.目前的研究成果大多是基于形式化方法［3－4］，包括模型檢測和定理證明.模型檢測是用一種形式化語言描述系統，生成系統行為的形式化描述，遍歷系統模型的狀態空間檢驗系統行為是否與需求相一致.國內外學者［5－11］普遍使用Petri網或自動機為系統建模，將系統行為用另一種形式化語言描述，再用模型檢測工具進行競態檢測.雖然模型檢測可以實現檢驗過程的自動化，但是要遍歷系統模型的狀態空間，面臨著“狀態空間爆炸”的問題.定理證明可以處理無限的狀態空間，它使用類似于結構化的推導過程來證明具有無限狀態的系統.Kramer等［12］提出了Higher Order Logic分析PLC 程序的方法.陳鋼等［13］用COQ 定理證明器輔助PLC 程序驗證和分析.但是，定理證明大多數是交互的，需要人的參與，所以不僅提高了出錯的概率，也降低了自動驗證的可行性.盡管目前出現了用依賴圖［14－15］描述程序之間關系的研究，但是它將一個梯級看成結點，忽略了很多細節，無法清楚地表達梯形圖各元素的邏輯關系.因此，本文提出了關系圖的概念，通過梯形圖轉化為關系圖；然后，從關系圖的結構檢驗梯形圖不存在競態；最后，通過實例探討該方法在競態檢驗上的應用.

圖1 簡單的梯形圖Fig.1 Simple ladder diagram

1 梯形圖和競態

梯形圖是在原繼電器－接觸器控制系統的繼電器梯形圖基礎上演變而來的一種圖形語言.由于梯形圖直觀易懂，成為目前使用最廣泛的一種PLC 編程語言.梯形圖的一個執行周期可以看成能量流從左垂直線經過A，B到達C，然后從下一梯級的左母線經過C到達B的過程，如圖1所示.

梯形圖的競態是指在輸入和功能模塊狀態不變的情況下，輸出發生變化.如圖1的梯形圖存在競態，假設線圈C是輸出線圈，觸點A 是輸入觸點.保持觸點A 是導通的，由于觸點B是常閉觸點，所以第一PLC 掃描周期線圈C 為高電平，當第二梯級執行完后，觸點B為高電平；第二PLC 掃描周期，由于觸點B 是常閉觸點，此時為高電平，所以C變為低電平.因為輸出狀態的變化不是功能模塊引起的，所以梯形圖存在競態.

2 關系圖的定義

從形式化的角度，一個關系圖D由非空有限集V（D），V′（D），A（D）和c構成，可以被定義為一個四元組，記為D＝（V，V′，A，c）.其中：V＝｛v1，v2，…，vn｝表示有限非空實結點的集合；V′＝｛v′1，v′2，…，v′m｝表示有限非空虛結點的集合，V∩V′＝?，V∪V′≠?；A?（V×V′）∪（V′×V）是實結點和虛結點組成的二元組的集合，表示從實結點到虛結點或虛結點到實結點的有向弧集合；c∶A→Z＋表示關系圖中每一條弧上的權值，Z＋表示正整數集合.

用關系圖描述梯形圖的邏輯關系.關系圖的實結點用“□”表示，對應為梯形圖的圖符單元，如觸點、線圈、功能模塊等；虛結點表示邏輯關系“與”，用“|”來表示，沒有具體的意義；弧上權值大小為對應梯形圖的梯級，如權值為“1”表示第一個梯級，“2”表示第二個梯級，以此類推.圖1梯形圖對應的關系圖，如圖2所示.圖2表示的邏輯關系為實結點Vc受實結點Va，Vb同時控制的，對應到梯形圖表示為線圈C的狀態受觸點A，B的狀態共同控制，符合圖1梯形圖的描述.同理，實結點Vb受實結點Vc控制，對應到梯形圖表示為觸點B受線圈C 控制，也符合梯形圖的描述.因此，可以用關系圖等價的描述梯形圖的邏輯關系.

為了更好地認識關系圖，引入幾個概念.如果一個實結點只有輸入有向弧沒有輸出有向弧，稱該實結點為根結點；實結點到虛結點的有向弧或虛結點到實結點的有向弧，稱為關系圖的線路，簡稱線路；如果一個實結點，存在一條線路，使之沿著這條線路能回到原點，稱該線路是一個關系圖的環.

圖2 圖1梯形圖的關系圖模型Fig.2 Relation graphs model of ladder diagram shown in figure 1

3 梯形圖轉化為關系圖方法

梯形圖間的邏輯關系較復雜，從梯形圖的結構無法直觀地表示變量之間的邏輯關系.因此，提出將梯形圖的邏輯關系轉化為關系圖來表示，使梯形圖內各元素之間的邏輯關系清晰化，便于競態的檢測.

定義1在梯形圖中，由觸點、功能模塊以及連接它們之間的導線組成的線路稱為梯形圖的路徑.

定義2可使能量流從左母線到線圈（右母線）的路徑，稱為梯級路徑.從圖1的梯形圖實例可以看出：梯形圖有2條梯級路徑.梯級路徑的個數等于梯形圖的梯級數.

定義3由梯級路徑中的觸點、功能模塊組成的集合，并且刪除該集合內的任意元素，都會使梯級路徑斷開，則稱該集合為梯級路徑的割集，簡稱割集.

定義4從左母線到功能模塊所有端口的路徑，由這些路徑上的觸點組成的集合，并且刪除該集合內的任意元素，都會使功能模塊不能正常工作，稱該集合為模塊割集.

提出梯形圖到關系圖的轉化方法，給定一個梯形圖，假設其第一個梯級為1，以此類推.轉化方法為以下7個步驟.

步驟1將梯形圖的觸點、線圈、功能模塊模擬為實結點.

步驟2任選梯形圖的一個線圈，假設該線圈為Cx，對應的實結點為Vx.

步驟3確定Cx的割集的個數m，創建m個虛結點.

步驟4遍歷1個割集內的元素，連接元素對應實結點到該割集對應的虛結點的有向弧；連接虛結點到Vx的有向?。粸閺膶嵔Y點到實結點的有向弧賦予權值.重復上述步驟，直到遍歷完所有的割集.

步驟5取Cx梯級路徑上的一個觸點，判斷梯形圖是否存在以該觸點為輸出線圈的路徑，如果有，重復步驟3，4；如果沒有，取另一個觸點進行判斷，直到遍歷完所有觸點.

步驟6若還存在其他沒有遍歷的線圈，重復步驟2～5，直到遍歷完所有線圈.

步驟7取梯形圖的1個功能模塊，假設對應的實結點為Vy.確定模塊割集的數目n，創建n個虛結點.遍歷一個模塊割集內的元素，連接元素對應的實結點到該模塊割集對應的虛結點的有向??；連接虛結點到Vy的有向??；為弧賦予權值.重復上述步驟，直到遍歷完所有的模塊割集.

4 梯形圖不存在競態的充分條件

通過分析關系圖的結構，可得出梯形圖不存在競態的充分條件.

定理1給定一個梯形圖，如果它的關系圖中不存在環，那么該梯形圖中一定不存在競態.

證明 反證法.假設一個無環的關系圖對應的梯形圖存在競態.對于無環的關系圖，取任意非根結點，假設為V1，可以找到控制其狀態的實結點，假設為V2；同樣，V2如果不為根結點，可以找到控制其狀態的實結點，以此類推，直到遍歷到根節點.非根結點V1最后總可以看成控制了一個根結點的狀態.由于根結點的狀態在PLC的掃描周期內是不變的，所以V1不變.如果V1對應梯形圖的輸出線圈，說明輸出線圈在程序執行的過程中狀態不變，結論與假設矛盾，所以該充分條件成立.

根據競態的定義和上述的充分條件可得：如果關系圖存在環，且環內包含有實結點對應為梯形圖的功能模塊，對應的梯形圖不存在競態.

5 實例分析

梯形圖存在計數器C0，計數器的預設值為“2”，如圖3所示.當計數器的脈沖輸入端CU 為上升沿時，計數器加“1”；當計數器達到預設值時，C0輸出高電平；如果R 端為高電平時，計數器清零，輸出為低電平.根據前面提出的方法，將該梯形圖中的觸點、線圈、功能模塊模擬為實結點，得到的實結點集合V＝｛vm0.0，vm0.1，vm0.2，vq0.0，vq0.1，vi0.0，vC0｝；選取線圈Q0.1，其對應的實結點為vq0.1.遍歷線圈Q0.1可以得到Q0.1的割集為｛M0.1，M0.2｝，｛M0.2，M0.3｝，所以創建2個虛結點v′1，v′2；遍歷2個割集內的元素，連接對應結點之間的有向弧，然后給弧賦上相應的權值.

通過遍歷線圈Q0.1梯級路徑上的觸點可知：不存在以梯級路徑上的觸點為輸出線圈的路徑，所以取另一個線圈M0.0進行遍歷.步驟同上，可知M0.0的割集只有1個｛M0.1｝，所以創建1個虛結點v′3，連接對應結點之間的有向弧，最后給弧賦上相應的權值.

遍歷所有線圈直到沒有可遍歷的線圈.由于該梯形圖存在功能模塊，所以遍歷功能模塊，確定其模塊割集｛I0.0，M0.0，Q0.0｝；創建1個虛結點v′5；連接模塊割集內的元素對應的結點之間的有向弧，即連接vi0.0，vm0.0，vq0.0到v′5的有向弧；連接v′5到vC0的有向弧；為弧賦予權值.得到的關系圖，如圖4所示.圖4的關系圖存在環結構，但是環內有代表功能模塊的結點，根據提出的競態判據，該梯形圖不存在競態.

從時序圖的角度觀察，如圖5所示.從圖5中可以看出：輸出Q0.0的變化是由計數器C0到達預設值引發的，當計數器C0為低電平時，輸出Q0.0為低電平，根據競態的定義可知，梯形圖不存在競態.

圖3 不存在競態的梯形圖Fig.3 A ladder diagram free of race

圖4 圖3梯形圖的關系圖模型Fig.4 Relation graphs model of ladder diagram shown in figure 3

圖5 圖3梯形圖的時序圖Fig.5 Timing chart of ladder diagram shown in figure 3

6 結束語

競態本質上是由梯形圖內部觸點以及梯級的排列順序產生的，即梯形圖的結構影響到競態的產生.所以從梯形圖的結構入手，提出了用關系圖來描述梯形圖的邏輯關系，從而快速的判斷出梯形圖不存在競態.當需要檢測一個大型梯形圖程序是否存在競態，傳統的模型檢測會耗費大量的時間，文中為競態的檢測提出了一個新的思想.通過將梯形圖轉化為關系圖，根據所提出的充分條件，可以較快的判斷梯形圖不存在競態.為了實現構建過程的自動化及完善關系圖的判斷方法，未來的工作主要是基于提出的方法給出轉化算法，并給出梯形圖存在競態在關系圖中的充分條件.

［1］呂衛陽.PLC技術綜述［J］.自動化博覽，2008（增刊1）：16－19.

［2］AIKEN A，FAHNDRICH M，SU Zhen－dong.Detecting races in relay ladder logic programs［J］.International Journal on Software Tools for Technology Transfer，2000，3（1）：93－105.

［3］呂毅.形式化方法介紹及其在工程中的應用［J］.微電子學與計算機，2003（10）：26－34.

［4］張廣泉.關于軟件形式化方法［J］.重慶師范學院學報：自然科學版，2002，19（2）：1－4.

［5］楊年華，虞彗群，孫華.帶抑制弧的時延著色Petri網模型檢測技術［J］.計算機科學，2011，38（1）：170－176.

［6］沈云付，解曉方.基于on－the－fly的Petri網模型檢查技術研究與實現［J］.計算機應用與軟件，2011，28（5）：82－85.

［7］BENDER D F，COMBEMALE B，CRéGUT X，et al.Ladder metamodeling and PLC program validation through time Petri nets［C］∥4th European Conference on Model Driven Architecture－Foundations and Applications.Berlin：Springer，2008：121－136.

［8］NGALAMOU L，MYERS L.Combining software methods for effective deployment of programmable logic controllers［J］.International Journal of Computer Science and Network Security，2010，10（12）：134－145.

［9］WIGHTKIN N，BUY U，DARABI H.Formal modeling of sequential function charts with time Petri nets［J］.IEEE Transactions on Control Systems Technology，2011，19（2）：455－464.

［10］MOKADEM H B，BERARD B，GOURCUFF V，et al.Verification of a timed multitask system with UPPAAL［J］.IEEE Transactions on Automation Science and Engineering，2010，7（4）：921－932.

［11］TSAI J，TENG C C.Constructing an abstract model for ladder diagram using Petri nets［J］.Asian Journal of Control，2010，12（3）：309－322.

［12］KRAMER B J，VAOLKER N.A highly dependable computing architecture for safety－critical control application［J］.Real－Time Systems，1997，13（3）：237－251.

［13］陳鋼，宋曉宇，顧明.COQ 定理證明輔助PLC 程序驗證和分析［J］.北京大學學報：自然科學版，2010，46（1）：30－34.

［14］FERRANTE J，OTTENSTEIN K J，WARREN J D.The program dependence graph and its use in optimization［J］.ACM Transactions on Programming Languages and Systems，1987，9（3）：319－349.

［15］趙營，嚴義.基于梯形圖復雜依賴關系的分解研究［J］.機電工程，2012，29（5）：605－608.