一種可編程邏輯控制程序的競態(tài)檢測方法

黃穎坤，羅繼亮

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

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

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

1 梯形圖和競態(tài)

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

梯形圖的競態(tài)是指在輸入和功能模塊狀態(tài)不變的情況下，輸出發(fā)生變化.如圖1的梯形圖存在競態(tài)，假設(shè)線圈C是輸出線圈，觸點A 是輸入觸點.保持觸點A 是導(dǎo)通的，由于觸點B是常閉觸點，所以第一PLC 掃描周期線圈C 為高電平，當?shù)诙菁増?zhí)行完后，觸點B為高電平；第二PLC 掃描周期，由于觸點B 是常閉觸點，此時為高電平，所以C變?yōu)榈碗娖?因為輸出狀態(tài)的變化不是功能模塊引起的，所以梯形圖存在競態(tài).

2 關(guān)系圖的定義

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

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

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

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

3 梯形圖轉(zhuǎn)化為關(guān)系圖方法

梯形圖間的邏輯關(guān)系較復(fù)雜，從梯形圖的結(jié)構(gòu)無法直觀地表示變量之間的邏輯關(guān)系.因此，提出將梯形圖的邏輯關(guān)系轉(zhuǎn)化為關(guān)系圖來表示，使梯形圖內(nèi)各元素之間的邏輯關(guān)系清晰化，便于競態(tài)的檢測.

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

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

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

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

提出梯形圖到關(guān)系圖的轉(zhuǎn)化方法，給定一個梯形圖，假設(shè)其第一個梯級為1，以此類推.轉(zhuǎn)化方法為以下7個步驟.

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

步驟2任選梯形圖的一個線圈，假設(shè)該線圈為Cx，對應(yīng)的實結(jié)點為Vx.

步驟3確定Cx的割集的個數(shù)m，創(chuàng)建m個虛結(jié)點.

步驟4遍歷1個割集內(nèi)的元素，連接元素對應(yīng)實結(jié)點到該割集對應(yīng)的虛結(jié)點的有向??；連接虛結(jié)點到Vx的有向弧；為從實結(jié)點到實結(jié)點的有向弧賦予權(quán)值.重復(fù)上述步驟，直到遍歷完所有的割集.

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

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

步驟7取梯形圖的1個功能模塊，假設(shè)對應(yīng)的實結(jié)點為Vy.確定模塊割集的數(shù)目n，創(chuàng)建n個虛結(jié)點.遍歷一個模塊割集內(nèi)的元素，連接元素對應(yīng)的實結(jié)點到該模塊割集對應(yīng)的虛結(jié)點的有向??；連接虛結(jié)點到Vy的有向?。粸榛≠x予權(quán)值.重復(fù)上述步驟，直到遍歷完所有的模塊割集.

4 梯形圖不存在競態(tài)的充分條件

通過分析關(guān)系圖的結(jié)構(gòu)，可得出梯形圖不存在競態(tài)的充分條件.

定理1給定一個梯形圖，如果它的關(guān)系圖中不存在環(huán)，那么該梯形圖中一定不存在競態(tài).

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

根據(jù)競態(tài)的定義和上述的充分條件可得：如果關(guān)系圖存在環(huán)，且環(huán)內(nèi)包含有實結(jié)點對應(yīng)為梯形圖的功能模塊，對應(yīng)的梯形圖不存在競態(tài).

5 實例分析

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

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

遍歷所有線圈直到?jīng)]有可遍歷的線圈.由于該梯形圖存在功能模塊，所以遍歷功能模塊，確定其模塊割集｛I0.0，M0.0，Q0.0｝；創(chuàng)建1個虛結(jié)點v′5；連接模塊割集內(nèi)的元素對應(yīng)的結(jié)點之間的有向弧，即連接vi0.0，vm0.0，vq0.0到v′5的有向??；連接v′5到vC0的有向?。粸榛≠x予權(quán)值.得到的關(guān)系圖，如圖4所示.圖4的關(guān)系圖存在環(huán)結(jié)構(gòu)，但是環(huán)內(nèi)有代表功能模塊的結(jié)點，根據(jù)提出的競態(tài)判據(jù)，該梯形圖不存在競態(tài).

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

圖3 不存在競態(tài)的梯形圖Fig.3 A ladder diagram free of race

圖4 圖3梯形圖的關(guān)系圖模型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 結(jié)束語

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

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

［2］AIKEN A，F(xiàn)AHNDRICH 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］呂毅.形式化方法介紹及其在工程中的應(yīng)用［J］.微電子學與計算機，2003（10）：26－34.

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

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

［6］沈云付，解曉方.基于on－the－fly的Petri網(wǎng)模型檢查技術(shù)研究與實現(xiàn)［J］.計算機應(yīng)用與軟件，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］趙營，嚴義.基于梯形圖復(fù)雜依賴關(guān)系的分解研究［J］.機電工程，2012，29（5）：605－608.