基于PLCopen運動控制功能塊的時間自動機建模與驗證

孫青怡，黃志韜

（杭州電子科技大學(xué) 計算機學(xué)院，杭州 310018）

0 引言

PLCopen組織制定的運動控制功能塊[1]是基于IEC61131-3 標(biāo)準(zhǔn)定義的一組功能塊語言，主要是在IEC的研發(fā)環(huán)境中加入運動控制技術(shù)，采用統(tǒng)一接口以提高代碼復(fù)用性和系統(tǒng)可重構(gòu)性，具有統(tǒng)一的編程規(guī)范，功能塊直觀性強，使用功能塊圖語言能夠使編程調(diào)式時間大大減少。隨著運動控制系統(tǒng)的不斷發(fā)展和日益復(fù)雜，需要提高系統(tǒng)的安全性和可靠性[2]。運動控制系統(tǒng)的安全性驗證問題[3]是驗證工業(yè)控制系統(tǒng)建模的關(guān)鍵問題，目前缺少針對該系統(tǒng)的驗證方法，而傳統(tǒng)的驗證方法很少考慮到驗證難度、驗證時間以及驗證模型可重用性的問題。在我們的工作中，我們討論了PLCopen運動控制功能塊的可靠性驗證。

D.Aza-Vallina[4]等人描述了個現(xiàn)場總線的行為，他們使用mode自動機（mode-automata）而不是傳統(tǒng)的馬爾可夫鏈方法對這些行為進行建模,該方法可以縮小模型的狀態(tài)空間但是沒有對時間進行建模，所以無法驗證系統(tǒng)的實時性。Y.Jiang[5]將可編程控制器的程序的邏輯模塊以及硬件組件抽象成貝葉斯結(jié)點，再將它們映射到貝葉斯網(wǎng)絡(luò)中，從而得出系統(tǒng)運行錯誤的概率。De Silva和Dias等[6]提出了一種基于模型的方法來驗證安全儀表系統(tǒng)（SIS）。在這種方法中，由國際自動化協(xié)會（ISA）描述的規(guī)范和FBD程序被自動轉(zhuǎn)換為時間自動機模型，然后使用Uppaal測試工具驗證安全儀表系統(tǒng)是否符合規(guī)范模型。F.Basile[7]提出了一個基于事件驅(qū)動的方法來輔助功能塊圖程序的設(shè)計。該方法將每一個功能塊實例抽象成一個對象，并且這些對象的執(zhí)行由具體的事件來驅(qū)動。

迄今為止，以功能塊實現(xiàn)的運動控制系統(tǒng)，還缺乏相關(guān)的形式化驗證研究。因此，提出一種PLC執(zhí)行模型和轉(zhuǎn)換算法來形式化運動控制功能塊，通過Uppaal檢測系統(tǒng)[8]來驗證程序的可靠性。

1 PLC執(zhí)行模型

功能塊圖程序在循環(huán)中掃描執(zhí)行程序，將可編程控制器掃描周期過程轉(zhuǎn)換為時間自動機模型，這個模型作為功能塊的循環(huán)執(zhí)行模型來描述可編程控制器的執(zhí)行階段。自動機模型決定了一個自動機實例的行為，定義一個模型模板主要包括它的局部變量、常量、Location集合以及Edge集合。首先對時間自動機模型中的Location進行結(jié)構(gòu)化定義，可將狀態(tài)定義為一個四元組如定義1所示。

定義1 TA模型的Location：

1）name描述該狀態(tài)名稱，是在一個模型模板中狀態(tài)的唯一標(biāo)識，類型為字符串；

2）rate指定指數(shù)分布參數(shù)，規(guī)定了系統(tǒng)在該狀態(tài)的停留時間滿足的指數(shù)分布的參數(shù)，類型為字符串；

3）invariant指定狀態(tài)約束條件，描述了系統(tǒng)位于該狀態(tài)必須滿足的條件，類型為字符串；

4）type指定狀態(tài)結(jié)點的類別，包括initial、urgent和committed三個類別，initial用于指定該狀態(tài)是否為初始狀態(tài)，urgent用于指定該狀態(tài)是否為緊急狀態(tài)，committed用于指定該狀態(tài)是否為提交狀態(tài)，類型都為布爾變量。

根據(jù)可編程控制器的執(zhí)行流程生成執(zhí)行模型，用于模擬周期之間的執(zhí)行狀態(tài)轉(zhuǎn)換，模型如圖1所示。其中Idle狀態(tài)是時間自動機的初始狀態(tài)l0，Input、Execute、Output、Update、Next、End狀態(tài)是一個功能塊執(zhí)行時的不同階段，當(dāng)自動機進入Input狀態(tài)并以Next狀態(tài)結(jié)束時為一個周期。

圖1 可編程控制器循環(huán)執(zhí)行模型

上述執(zhí)行模型根據(jù)以下幾個狀態(tài)結(jié)點來描述PLC掃描周期的執(zhí)行階段：

這些狀態(tài)中，Idle表示當(dāng)前可編程控制器處于空閑狀態(tài)，變量IN表示當(dāng)前功塊已掃描的輸入引腳序號，OUT表示當(dāng)前功能塊的輸出引腳序號，變量N表示當(dāng)前功能塊圖程序的功能塊實例個數(shù)。當(dāng)可編程控制器開始執(zhí)行之后，模型狀態(tài)會從Idle轉(zhuǎn)換到Input狀態(tài)，表示當(dāng)前功能塊圖程序中功能塊實例使能并且開始讀取輸入數(shù)據(jù)。隨著input()函數(shù)的執(zhí)行，模擬讀取輸入變量，由于功能塊讀取輸入引腳時，會判斷功能塊是否使能以及參數(shù)是否合法等選擇不同處理方式，所以通過Input狀態(tài)和Execute狀態(tài)之間的循環(huán)轉(zhuǎn)換模擬功能塊讀取輸入引腳的過程。輸入引腳掃描結(jié)束之后將會從Execute狀態(tài)切換到Output狀態(tài)，calculate()函數(shù)表示功能塊會根據(jù)輸入引腳計算軸狀態(tài)（錯誤信息或預(yù)處理）、目標(biāo)位置、目標(biāo)速度、目標(biāo)加速度等等信息，所以也設(shè)置循環(huán)轉(zhuǎn)換模擬不斷查詢參數(shù)與狀態(tài)信息。Output狀態(tài)到Update狀態(tài)的轉(zhuǎn)換模擬判斷軸是否達到目標(biāo)位移，通過Output()函數(shù)表示修改軸信息結(jié)構(gòu)體的過程。Update狀態(tài)切換到Next狀態(tài)表示一次循環(huán)控制結(jié)束。對于循環(huán)執(zhí)行模型，變量FBN表示是否還有新的功能塊輸入，如果有新的輸入代表可編程控制器將執(zhí)行新的循環(huán)并且將輸入序號IN和輸出序號OUT重新置1，否則代表程序執(zhí)行結(jié)束。簡單來說，一個功能塊實例的執(zhí)行會更新系統(tǒng)環(huán)境中的變量。

2 功能塊圖程序建模

一個FBD程序的結(jié)構(gòu)化描述如定義2所示：

定義2 FBD程序：

其中：

1）FBDname：功能塊圖程序的名稱，一般會命名來體現(xiàn)本段程序的內(nèi)容；

2）Nodes：功能塊實例的集合，包含一段功能塊圖程序中的所有功能塊實例；

3）FBN：程序網(wǎng)絡(luò)結(jié)構(gòu)，由功能塊實例，以及實例之間的關(guān)系組成；

4）IP：一組輸入變量，用于表示程序中處理的參數(shù)；

5）OP：一組輸出變量，即程序執(zhí)行之后輸出的參數(shù)；

6）IOP：一組輸入輸出變量，是軸信息變量，一個結(jié)構(gòu)體參數(shù)，具體定義由開發(fā)商決定；

7）VL：一組FBD中定義的局部變量參數(shù)；

8）VG：一組FBD中定義的全局變量參數(shù)；

9）VE：全局外部變量，用于FBD與其他FBD的組織與合并參數(shù)；

10）VA：程序中可訪問變量；

11）Body：用于描述FBD程序的實例行為；

定義3 連接集合：

其中：

1）Nodes是功能塊實例FB的集合。＜FBx，Voutput，F(xiàn)By，Vinput是其中一個連接，可表示為FBnamei.opm→FBnamej.ipn；

2）FB以及FBy分別代表兩端的功能塊實例；

3）Voutput∈FBoutput以及Vinput∈FBinput分別代表兩個功能塊實例的輸出端口和輸入端口。

定義4 功能塊實例：

其中：

1）FBname：是該功能塊實例的名字；

2）FBTypeName：是該實例相應(yīng)的功能塊類型名稱。

3）executeOrder：是該功能塊相對其他功能塊的執(zhí)行順序。它是一個定義功能塊實例的執(zhí)行順序的整數(shù)。每個功能塊中心的數(shù)字則代表功能塊實例執(zhí)行的順序executeOrder，需要注意executeOrder是在執(zhí)行順序有歧義的情況下才有效果。

在把功能塊圖程序轉(zhuǎn)換為時間自動機模型之前，功能塊實例的執(zhí)行順序也必須確定。在PLCopen運動控制規(guī)范中啟動單個軸的運行方式其基本規(guī)則是按順序給出運動控制命令，即使PLC具有實時并行處理能力，也是按順序執(zhí)行運動控制命令。功能塊圖程序的執(zhí)行順序是由具體的廠商制定的。

在圖2所示功能塊圖程序中，計數(shù)器N代表功能塊實例編號，并確保功能塊實例一次執(zhí)行。在掃描最后一個功能塊實例之后，計數(shù)器將重置以便重復(fù)掃描周期。在圖2所示的程序片段中，當(dāng)Start變量設(shè)置為true時，mc_fb_1、mc_fb_2的執(zhí)行順序存在歧義，可以根據(jù)手動設(shè)定的executeOrder來判斷哪一個功能塊先執(zhí)行。由于圖中因此mc_fb_1先執(zhí)行。由于運動命令依次執(zhí)行，提取FBD程序的執(zhí)行列表，然后將其轉(zhuǎn)換為Uppaal模板。

圖2 功能塊圖程序

本小節(jié)提出一個Diagram-Uppaal（D-U）轉(zhuǎn)換來執(zhí)行上述轉(zhuǎn)換。D-U轉(zhuǎn)換的第一步，定義一個Diagram-List（D-L）轉(zhuǎn)換來提取出功能塊圖的執(zhí)行列表。由于功能塊圖的連接有輸入端和輸出端，可將功能塊實例以及邏輯操作（AND/OR）映射為節(jié)點，因此連接的輸入端為前驅(qū)節(jié)點，輸出端為后繼節(jié)點，將各節(jié)點之間的連接線映射成邊，所得到的功能塊圖程序的圖模型稱為FBD圖，定義一個元組Gi=＜Ni，F(xiàn)coni＞來描述圖模型，其中

例如將圖2中的程序用圖模型Gi來描述，該圖一共有三個功能塊實例，映射為三個圖，如圖3所示。

圖3 程序圖模型Gi

將該程序中的三個圖定義為G1，G2，G3，因此該功能塊圖之間的連接可描述為：

其中，函數(shù)last（G1）返回的是圖G1中所有功能塊實例的執(zhí)行結(jié)果（此處只有功能塊實例mc_fb_1），表示該連接關(guān)系中的前驅(qū)節(jié)點；函數(shù)head（G3）返回的是圖G3中所有功能塊實例的首節(jié)點，表示該連接關(guān)系中的后繼節(jié)點。

通過由功能塊之間的連接執(zhí)行D-L轉(zhuǎn)換得到的結(jié)構(gòu)形式為：

其中，fop取決于Nt，Nt代表邏輯表達式，如果Nt是邏輯與（AND），那么fop（Scnd1，Scnd2）執(zhí)行交運算，如果Nt是邏輯或（OR），那么fop（Scnd1，Scnd2）執(zhí)行并運算，我們在功能塊圖上重復(fù)執(zhí)行D-L轉(zhuǎn)換，直到功能塊實例上沒有邏輯運算。通過轉(zhuǎn)換結(jié)果，我們可以生成功能塊圖程序的執(zhí)行列表：

D-U轉(zhuǎn)換的第二步，將功能塊實例描述為時間自動機中的位置集合，將程序中的功能塊連接描述為時間自動機中的邊集合。由圖2中的功能塊程序生成的位置集合如下所示，位置范圍從lstart～lEnd。

其中，lfbi表示功能塊實例，lstart代表時間自動機的初始位置，lEnd代表時間自動機的最終位置，lEnd是程序單次運行周期的最終狀態(tài)，在程序下一個周期的運行開始之前，多個自動機將會在同步事件end的作用下切換到初始狀態(tài)lstart。并且提出以下規(guī)則，以便將程序的功能塊連接轉(zhuǎn)換為邊集合。

時間自動機中的邊可以表示為：

規(guī)則1：對于start到程序的第一個功能塊實例，轉(zhuǎn)換成時間自動機的邊

規(guī)則2：對于程序的最后一個功能塊實例到end，轉(zhuǎn)換成時間自動機的邊

規(guī)則3：對于其他功能塊實例之間的連接關(guān)系，轉(zhuǎn)換成時間自動機的邊

其中assignmenti()將輸入變量傳遞到輸入緩沖區(qū)，cndi()獲取邊的執(zhí)行條件。

D-U轉(zhuǎn)換完成之后，可以得到基于功能塊圖程序的時間自動機位置集合以及邊集合，將程序轉(zhuǎn)換為時間自動機模型，該模型描述為FBDProgramModel()。

3 實驗

以拋球機為例，對實現(xiàn)該系統(tǒng)的程序進行建模。圖4(a)中是拋球機器照片以及圖4(b)是該機器的示意圖。根據(jù)示意圖，A沿y軸移動，B沿x軸移動。A和B移動到準(zhǔn)備位置，通過設(shè)置B在y軸的距離和速度實現(xiàn)拋球功能。我們把這部分轉(zhuǎn)換成時間自動機模型來檢查功能和性能要求是否得到滿足。

圖4 拋球機

圖2中的功能塊圖程序是用于實現(xiàn)拋球機功能的部分程序，對該程序進行驗證，將程序轉(zhuǎn)換為時間自動機模型FBDProgramModel()，如圖5所示。

圖5 程序模型FBDProgramModel()

程序模型可以描述為：

其中，F(xiàn)BExecuteModel()是PLC循環(huán)執(zhí)行模型。

目前，使用Uppaal檢測工具來驗證時間自動機，該工具利用一組有界整型變量的時間自動機，模擬非確定性并行過程的實時系統(tǒng)。Uppaal的時序邏輯（TCLT）使用路徑公式量化模型的路徑及軌跡[9]。需要驗證的標(biāo)準(zhǔn)如下：系統(tǒng)可達性、是否存在死鎖情況、系統(tǒng)在y軸上的運行距離不能超過拋球機實物的軸長度800。所使用的性質(zhì)驗證語句如下所示：

P1：E＜＞ fbd.End；模型可達性驗證。

P2：E＜＞ FBEN.End；模型可達性驗證。

P3：A[] not deadlock；模型死鎖情況驗證。

P4：A[] Position_Y＜800；模型安全性驗證，系統(tǒng)在y軸上的運行距離不能超過拋球機實物的軸長度800。

在Uppaal系統(tǒng)驗證器中分別輸入以上的驗證語句，驗證結(jié)果如圖6所示。其中滿足E＜＞ fbd.End和E＜＞FBEN.End性質(zhì)表示該模型的可達性滿足，說明存在路徑開始于初始狀態(tài)并最終滿足模型的結(jié)束狀態(tài)，驗證該系統(tǒng)能順利執(zhí)行完成，功能塊程序能到達最終狀態(tài)。死鎖狀態(tài)是指這個狀態(tài)和它的延遲后續(xù)沒有任何輸出動作，性質(zhì)A[] not deadlock驗證結(jié)果為滿足，表示該系統(tǒng)在任何狀態(tài)下不存在死鎖，即該模型的狀態(tài)都可以有輸出動作。性質(zhì)A[] Position_Y＜800驗證模型的安全性，驗證結(jié)果為滿足，表示Position_Y＜800在可達狀態(tài)下永遠為真。驗證結(jié)果表明滿足驗證的全部性質(zhì)，即驗證了程序的可靠性。

圖6 驗證情況

4 結(jié)語

本文致力于對PLCopen標(biāo)準(zhǔn)運動控制功能塊圖程序進行建模及驗證，功能塊圖語言采用圖形化描述，結(jié)構(gòu)簡單并且易于實現(xiàn)復(fù)雜的控制程序，是運用最為廣泛的PLC標(biāo)準(zhǔn)編程語言。經(jīng)過深入分析國內(nèi)外現(xiàn)狀和查閱大量有關(guān)文獻，本文實現(xiàn)了將功能塊轉(zhuǎn)換為時間自動機，利用Uppaal檢測工具驗證其可達性、死鎖、安全性等性質(zhì)，從而可以對程序進行可靠性驗證。通過實驗結(jié)果，開發(fā)人員可以發(fā)現(xiàn)程序或系統(tǒng)的安全性問題或性能改進點，從而更好地改進系統(tǒng)。