PLC程序形式化的設(shè)計(jì)與驗(yàn)證

齊鵬飛，羅繼亮，陳雪琨

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

可編程邏輯控制器（PLC）是一種以微處理器為核心，在計(jì)算機(jī)技術(shù)、電氣自動(dòng)控制技術(shù)和網(wǎng)絡(luò)通信技術(shù)基礎(chǔ)上，開發(fā)出來的工業(yè)控制裝置［1］.傳統(tǒng)設(shè)計(jì)方法存在程序設(shè)計(jì)和調(diào)試的工作量繁瑣巨大，以及程序開發(fā)周期和開發(fā)成本難于控制等問題［2-4］.一般來說，傳統(tǒng)的PLC程序設(shè)計(jì)過程是一個(gè)開環(huán)控制過程，無法準(zhǔn)確指出錯(cuò)誤發(fā)生在哪一段程序.也就是說，整個(gè)檢測(cè)過程沒有一個(gè)準(zhǔn)確的反饋信息，這類似于開環(huán)控制存在的缺陷.設(shè)計(jì)人員只能按照程序設(shè)計(jì)的順序從上到下逐條檢測(cè)，這樣不但嚴(yán)重影響程序開發(fā)周期，浪費(fèi)人力、物力，更重要的是人為檢測(cè)并不能保證識(shí)別全部邏輯錯(cuò)誤.此外，編程軟件主要針對(duì)語法、語義上的檢測(cè)，并不能發(fā)現(xiàn)整個(gè)程序中邏輯性質(zhì)上的錯(cuò)誤，如競(jìng)態(tài)［5］和死鎖等.形式化方法是一種用于規(guī)范、設(shè)計(jì)和驗(yàn)證計(jì)算機(jī)系統(tǒng)的基本數(shù)學(xué)方法.引入形式化方法的目的，在于希望能使系統(tǒng)具有較高的可信度和正確性，并能使系統(tǒng)具有良好的結(jié)構(gòu)、易于維護(hù)、較好地滿足客戶的要求.目前，形式化方法已在不同領(lǐng)域的主流產(chǎn)品開發(fā)中得到了成功應(yīng)用，如Multos信用卡認(rèn)證系統(tǒng)、Eurocopter公司民用直升機(jī)自動(dòng)導(dǎo)航系統(tǒng)和AMD AthlonTM芯片浮點(diǎn)運(yùn)算部件驗(yàn)證等.這都說明了形式化方法在工業(yè)界的應(yīng)用條件已經(jīng)成熟，開始逐漸被工業(yè)界所接受.本文從形式化方法的角度出發(fā)，探討將形式化方法應(yīng)用到PLC程序設(shè)計(jì)中的理論成果.

1 形式化設(shè)計(jì)PLC程序

形式化設(shè)計(jì)PLC程序是以形式規(guī)范方法為核心，首先將被控對(duì)象的行為特性、時(shí)間特性、性能特性和內(nèi)部結(jié)構(gòu)用一種規(guī)范語言來描述，即構(gòu)建形式化模型 .最后，通過等價(jià)轉(zhuǎn)換，將形式化語言翻譯為工程人員熟知的PLC程序，并應(yīng)用于實(shí)際生產(chǎn).整個(gè)設(shè)計(jì)過程，如圖1所示.

1.1 構(gòu)建系統(tǒng)的形式化模型

最近幾年，形式化方法的應(yīng)用已經(jīng)滲入到現(xiàn)代工業(yè)各個(gè)領(lǐng)域.然而，由于每個(gè)領(lǐng)域內(nèi)系統(tǒng)的工作流程和特點(diǎn)不盡相同，所以在利用形式化方法對(duì)系統(tǒng)建模時(shí)也采用了不同的形式化語言.

在核工業(yè)領(lǐng)域，韓贊東等［6］提出了基于可控Petri網(wǎng)（CPN）的復(fù)雜系統(tǒng)設(shè)計(jì)方法，通過賦予庫所和變遷實(shí)際的控制屬性，引入宏庫所和宏操作，實(shí)現(xiàn)了對(duì)燃料元件裝卸系統(tǒng)的分層設(shè)計(jì)，很好地滿足了球床式高溫氣冷堆的設(shè)計(jì)要求.

在鐵路交通領(lǐng)域，Giua等［7］利用Petri網(wǎng)設(shè)計(jì)出了包含車站和軌道的鐵路交通系統(tǒng)模型，在設(shè)計(jì)過程中，模型的控制器的加載是在離散事件系統(tǒng)監(jiān)控理論的基礎(chǔ)上自動(dòng)完成的.這一方法能夠有效降低復(fù)雜系統(tǒng)建模工作量，而且免去了對(duì)復(fù)雜邏輯關(guān)系的分析，確保了系統(tǒng)的準(zhǔn)確性.Durmus等［8］利用自動(dòng)化Petri網(wǎng)（APN）實(shí)現(xiàn)了對(duì)一個(gè)簡易鐵路站場(chǎng)的信號(hào)與聯(lián)鎖系統(tǒng)的設(shè)計(jì)，通過使用抑制弧和附有激發(fā)條件的變遷等元素，動(dòng)態(tài)地表示出了鐵路站場(chǎng)內(nèi)的列車調(diào)度流程，實(shí)現(xiàn)了對(duì)列車的聯(lián)鎖控制.

圖1 PLC程序的形式化設(shè)計(jì)Fig.1 Design of PLC programs using formal methods

在化工領(lǐng)域，賈洋等［9］提出了基于賦時(shí)Petri網(wǎng)（TPN）的設(shè)計(jì)方法，實(shí)現(xiàn)了對(duì)間歇過程換熱網(wǎng)絡(luò)的設(shè)計(jì)，所采用時(shí)間庫表示間歇過程的時(shí)間，適合于優(yōu)化設(shè)計(jì)間歇過程換熱網(wǎng)絡(luò).

在軍事工業(yè)領(lǐng)域，胡昌華等［10］提出了基于普通Petri網(wǎng)（Ordinary PN）模型［11］的導(dǎo)彈控制系統(tǒng)故障診斷方法，充分利用了Petri網(wǎng)在描述系統(tǒng)動(dòng)態(tài)遷移上的能力，通過觀察托肯的最終走向來確定系統(tǒng)是否會(huì)達(dá)到故障狀態(tài)，簡單而直觀地表示了整個(gè)診斷過程.

在處理商務(wù)流程方面，Du等［12］也提出了以TPN為基礎(chǔ)設(shè)計(jì)國際股票交易系統(tǒng)形式化模型的方法，很好地刻畫了系統(tǒng)的動(dòng)態(tài)行為，并利用時(shí)態(tài)公式描述了各事件之間的因果關(guān)系，確保了系統(tǒng)模型的準(zhǔn)確性.

在離散制造業(yè)，Venkatesh等［13］提出了基于Petri網(wǎng)的離散事件控制器的設(shè)計(jì)方法，利用實(shí)時(shí)Petri網(wǎng)結(jié)構(gòu)去描述各單元之間的邏輯關(guān)系，并通過一個(gè)實(shí)例比較了Petri網(wǎng)模型與梯形圖之間的優(yōu)勢(shì)與不足，最終指出此方法更簡單高效.

雖然用來構(gòu)建目標(biāo)系統(tǒng)的形式化模型的語言有很多種，但是它們都遵循了一個(gè)共同的規(guī)則 .首先，要對(duì)目標(biāo)系統(tǒng)進(jìn)行透徹的分析，找出其重要的組成單元；然后，將這些組成單元用形式化語言來描述；最后，根據(jù)目標(biāo)系統(tǒng)的工作流程將上述形式化的組成單元連接起來，這樣就得到了目標(biāo)系統(tǒng)的初步形式化模型.除了上文提到的幾種形式化語言之外，還有很多人利用不同的語言進(jìn)行著研究工作.如Hanisch等［14］應(yīng)用Timed C／E system語言描述系統(tǒng)行為；Kotini等［15］通過混雜自動(dòng)機(jī)設(shè)計(jì)混合系統(tǒng)，等等.

1.2 形式化建模性質(zhì)分析

當(dāng)完成了對(duì)系統(tǒng)的形式化建模后，首先要考慮的問題就是這個(gè)模型是否正確 .即模型是否滿足實(shí)際系統(tǒng)運(yùn)行所需的活性、無死鎖、無阻塞、有界、可重復(fù)性等性質(zhì)，而這些性質(zhì)的判斷又可以借助模型本身的結(jié)構(gòu)屬性.

Frey等［16-17］利用信號(hào)解釋Petri網(wǎng)（SIPN）構(gòu)建了一個(gè)簡易的水箱加熱控制器模型，通過托肯在庫所中的流動(dòng)動(dòng)態(tài)地表示出了系統(tǒng)的動(dòng)態(tài)行為.為了保證系統(tǒng)模型的正確性，他們針對(duì)SIPN這種語言具有的結(jié)構(gòu)屬性進(jìn)行了診斷.由于SIPN屬于普通Petri網(wǎng)的一種延伸，所以它也具有活性、可逆性、可達(dá)性和安全性等普通Petri網(wǎng)的性質(zhì).除此之外，SIPN還有決定性、終止性、輸出正確性、輸入依賴性等特殊性質(zhì).因此，在利用普通Petri網(wǎng)建模后，實(shí)際上可以拋開模型的物理意義，單純從數(shù)學(xué)角度去診斷整個(gè)模型是否存在錯(cuò)誤.

由于在建模時(shí)是嚴(yán)格按照規(guī)則執(zhí)行的，所以整個(gè)模型與實(shí)際系統(tǒng)是一一對(duì)應(yīng)的，發(fā)現(xiàn)的錯(cuò)誤可以直接還原到實(shí)際系統(tǒng)中.此外，可以使用PIPE，TINA等一些軟件工具來幫助診斷.當(dāng)軟件中不再顯示模型有錯(cuò)誤時(shí)，就完成了對(duì)系統(tǒng)的形式化建模工作.兩者相比較，不難看出：雖然SIPN在建模能力上超過了普通Petri網(wǎng)，但是在分析的時(shí)候卻增加了不小的難度.

1.3 將系統(tǒng)的形式化模型翻譯成PLC程序

Frey等［18］給出了將SIPN翻譯成PLC程序的轉(zhuǎn)換方法.他們將每一個(gè)庫所和變遷都對(duì)應(yīng)轉(zhuǎn)換成一條梯形圖程序.以庫所為例，如果當(dāng)前要轉(zhuǎn)換的庫所已經(jīng)被標(biāo)識(shí)，那么在梯形圖中，除了利用常開觸點(diǎn)表示庫所對(duì)應(yīng)的地址外，還要利用復(fù)位和置位指令將庫所對(duì)應(yīng)的輸出函數(shù)表示出來.當(dāng)把網(wǎng)結(jié)構(gòu)中的每一個(gè)變遷和庫所都轉(zhuǎn)換成一條梯形圖程序時(shí)，也就得到了整個(gè)系統(tǒng)對(duì)應(yīng)的梯形圖程序.在后續(xù)的工作中，F(xiàn)rey等［18］還開發(fā)出了相關(guān)的軟件SIPN-editor，可以在軟件中自動(dòng)實(shí)現(xiàn)上述整個(gè)過程.

除此之外，Wang等［19］給出了將時(shí)間自動(dòng)機(jī)［20］轉(zhuǎn)換成梯形圖的方法，也給出了相應(yīng)的算法，并通過軟件實(shí)現(xiàn)了自動(dòng)轉(zhuǎn)換.Perme等［21］提出了一種將擴(kuò)展Petri網(wǎng)（附帶有抑制弧、賦時(shí)變遷等元素）轉(zhuǎn)換成梯形圖程序的方法，并在PLC程序軟件上進(jìn)行了仿真 .同樣是以Petri網(wǎng)為模型，Dideban等［22］通過將Petri網(wǎng)轉(zhuǎn)換成順序功能圖表（SFC），解決了在資源分配時(shí)出現(xiàn)的互斥現(xiàn)象.Taholakian等［23］，Jones等［24］，琚長江等［25］，LEE等［26］也都分別提出了將Petri網(wǎng)轉(zhuǎn)換成梯形圖的不同方法.然而，在現(xiàn)有的方法中，更多的是針對(duì)PLC程序的單一指令，而沒有考慮指令與指令之間的邏輯關(guān)系.

2 形式化驗(yàn)證PLC程序

與形式化設(shè)計(jì)PLC程序不同，形式化驗(yàn)證PLC程序是以形式化驗(yàn)證技術(shù)為核心，將已經(jīng)編輯好的PLC程序轉(zhuǎn)換成驗(yàn)證工具所能夠識(shí)別的語言，然后利用驗(yàn)證工具對(duì)其進(jìn)行驗(yàn)證.如果出現(xiàn)錯(cuò)誤，驗(yàn)證工具會(huì)給出相應(yīng)的反例，這樣就可以有針對(duì)性地對(duì)原始程序進(jìn)行修改，從而得到正確的程序，保證了程序的可靠性.整個(gè)形式化驗(yàn)證PLC程序的過程，如圖2所示.

2.1 將已存在的PLC程序翻譯成形式化語言

現(xiàn)有的驗(yàn)證技術(shù)包括模型驗(yàn)證和定理證明兩大類.以此為標(biāo)準(zhǔn)，也把由PLC程序轉(zhuǎn)換成形式化語言的方法分為兩類.

圖2 形式化驗(yàn)證PLC程序過程Fig.2 Verification of PLC programs using formal methods

1）適用于模型驗(yàn)證的形式化語言.Wightkin等［27］提出了一種將SFC語言轉(zhuǎn)換成Petri網(wǎng)的方法.相比較前人的方法，Wightkin在建模時(shí)考慮了時(shí)間參數(shù)，很好地描述了PLC的繼電特性.當(dāng)然，賦時(shí)Petri網(wǎng)并不是唯一能夠融合時(shí)間參數(shù)的形式化語言.Mokadem等［28］利用時(shí)間自動(dòng)機(jī)也實(shí)現(xiàn)了對(duì)SFC程序的轉(zhuǎn)換，并且在UPPAAL［29］中進(jìn)行驗(yàn)證.

雖然兩種語言都達(dá)到了最初的目的，但是賦時(shí)Petri網(wǎng)模型要遠(yuǎn)小于賦時(shí)自動(dòng)機(jī)模型，建模效率更高.Oliveira等［30］完成了從梯形圖程序到有色Petri網(wǎng)的自動(dòng)轉(zhuǎn)換過程，Tsai等［31］則采用布爾Petri網(wǎng)完成了從梯形圖到形式化模型的翻譯.

2）適用于定理證明的形式化語言.陳鋼等［32］提出借助COQ定理證明器，去驗(yàn)證PLC程序是否存在錯(cuò)誤.在翻譯階段，他們首先建立好相關(guān)的基本定義，包括類型定義、變量定義和程序定義等；然后通過用COQ中的謂詞邏輯公式定義來描述每一段梯形圖程序的語義，實(shí)現(xiàn)了從PLC程序到數(shù)學(xué)邏輯語言的轉(zhuǎn)換.

相對(duì)來說，利用定理證明器來驗(yàn)證PLC程序的工作還是比較少見的.目前，只有Kramer等［33］利用HOL系統(tǒng)做了同樣的工作.

2.2 形式化描述PLC程序的控制規(guī)范

PLC程序的控制規(guī)范與系統(tǒng)的控制規(guī)范相似，它們描述了整個(gè)程序要實(shí)現(xiàn)什么功能，以及在這個(gè)實(shí)現(xiàn)過程中可以達(dá)到的某些狀態(tài).常見的規(guī)范有順序、聯(lián)鎖和“無競(jìng)態(tài)”控制等.實(shí)際上，在利用形式化語言進(jìn)行系統(tǒng)建模時(shí)，也是要考慮到系統(tǒng)控制規(guī)范的.能否清晰地表征出系統(tǒng)的控制規(guī)范是在利用形式化語言建模時(shí)的一個(gè)基本要求.

在這一步中，依然可以根據(jù)驗(yàn)證技術(shù)的不同，來選擇不同的形式化語言來描述控制規(guī)范 .顧明等所使用的仍然是COQ特有的謂詞邏輯公式來描述.這把要驗(yàn)證的PLC程序和要實(shí)現(xiàn)的控制目標(biāo)都轉(zhuǎn)換成了同一種語言，方便于下一步的推理證明 .時(shí)態(tài)邏輯語言是另外一種可以用來描述PLC程序控制規(guī)范的形式化語言，可以根據(jù)對(duì)時(shí)間認(rèn)識(shí)的不同將其分為線性時(shí)態(tài)邏輯（LTL）和計(jì)算樹邏輯（CTL）［34］，廣泛應(yīng)用于模型驗(yàn)證技術(shù).

2.3 利用形式化驗(yàn)證工具驗(yàn)證PLC程序

在定理證明中，經(jīng)常被提到的驗(yàn)證工具除了COQ定理證明器外，還有HOL和ACL2等.定理證明實(shí)際上是利用邏輯公式來描述系統(tǒng)及其性質(zhì)，通過一些公理或推理規(guī)則來證明系統(tǒng)滿足某些性質(zhì).而且，可以利用歸納法來處理無限狀態(tài)的驗(yàn)證問題.

與之相對(duì)的是模型檢測(cè)技術(shù).模型檢驗(yàn)是最近十幾年經(jīng)常被學(xué)者們采用的一類形式化驗(yàn)證方法.它的基本思想是通過對(duì)狀態(tài)空間的搜索來確認(rèn)系統(tǒng)是否具有某些性質(zhì).其中，狀態(tài)空間指的是利用形式語言并且在嚴(yán)格遵循被控對(duì)象性質(zhì)的前提下，設(shè)計(jì)的系統(tǒng)模型中的所涵蓋的全部狀態(tài).

NuSMV是目前最為廣泛應(yīng)用的一種模型檢測(cè)工具，它是由Carnegie Mellon University的McMillan博士在SMV基礎(chǔ)上重新構(gòu)造和實(shí)現(xiàn)的.雖然從輸入語言的角度來講，NuSMV和SMV都是針對(duì)有限狀態(tài)機(jī)來進(jìn)行搜索的.但是，NuSMV在融合了BDD［35］技術(shù)后，更有效地解決了狀態(tài)空間爆炸的問題.相對(duì)來說更適用于更復(fù)雜的程序驗(yàn)證.

NuSMV可以驗(yàn)證工業(yè)設(shè)計(jì)的可靠性，也作為一個(gè)定制的檢測(cè)工具的核心，還可以作為一個(gè)驗(yàn)證技術(shù)的試驗(yàn)平臺(tái)應(yīng)用于其他領(lǐng)域.因此，在形式化驗(yàn)證PLC程序的研究領(lǐng)域內(nèi)，NuSMV都得到了很多學(xué)者的肯定，如Pavlovic等［36］和 Gourcuffc等［37］.除此之外，SPIN［38］，UPPAAL 等驗(yàn)證工具也被應(yīng)用于PLC程序驗(yàn)證.

3 研究展望

PLC程序可靠性的首要內(nèi)容是PLC系統(tǒng)的形式化描述（形式化建模），它又分為硬件（傳感器和執(zhí)行機(jī)構(gòu)）系統(tǒng)建模和控制規(guī)范的形式化描述，現(xiàn)有的方法在這兩方面還沒有出現(xiàn)系統(tǒng)的理論成果，還需要大量研究工作.

在硬件系統(tǒng)的建模方面，主要是通過PLC程序的識(shí)別來獲得形式化模型（Petri網(wǎng)或自動(dòng)機(jī)）.然而，現(xiàn)有的成果只是給出了某類指令到某類Petri網(wǎng)結(jié)構(gòu)或自動(dòng)機(jī)之間的一一對(duì)應(yīng)關(guān)系，沒有描述指令之間的邏輯語義，因此無法將一個(gè)完整的PLC程序自動(dòng)描述為Petri網(wǎng)或自動(dòng)機(jī).在得到硬件系統(tǒng)的模型和控制規(guī)范的形式化模型之后，如何添加控制庫所才能獲得可靠、最優(yōu)的閉環(huán)系統(tǒng)的研究還屬空白.基于上述分析，以下幾個(gè)問題是PLC形式化設(shè)計(jì)和驗(yàn)證的最具價(jià)值的研究方向.

1）基于Petri網(wǎng)監(jiān)控理論的形式化設(shè)計(jì) .包括受控PLC系統(tǒng)（傳感器和執(zhí)行機(jī)構(gòu)）的系統(tǒng)建模方法、一般PLC控制規(guī)范（順序、聯(lián)鎖和無競(jìng)態(tài)等）描述為線性約束［39］的方法，以及根據(jù)控制規(guī)范設(shè)計(jì)閉環(huán)Petri網(wǎng)和從Petri網(wǎng)到PLC語言的等價(jià)轉(zhuǎn)換方法.

2）PLC程序的系統(tǒng)的形式化建模方法 .目前，雖然學(xué)術(shù)界在針對(duì)PLC程序中簡單指令的建模工作取得了一定的成績，但現(xiàn)有的成果更多地局限于單一指令的建模，而沒有考慮到指令之間邏輯組合后的建模方法.而且，定時(shí)器、計(jì)數(shù)器器等復(fù)雜指令或功能模塊的建模問題還沒有取得明顯的進(jìn)展.

3）基于Petri網(wǎng)結(jié)構(gòu)特征的定理證明方法.當(dāng)構(gòu)建一個(gè)系統(tǒng)的Petri網(wǎng)模型后，可以基于Petri網(wǎng)的結(jié)構(gòu)特征對(duì)模型進(jìn)行性質(zhì)分析，如根據(jù)虹吸結(jié)構(gòu)［40-41］判斷系統(tǒng)是否死鎖（適用于普通Petri網(wǎng)）.這樣就可以避免模型檢測(cè)遍歷系統(tǒng)的每個(gè)狀態(tài)，大大降低程序驗(yàn)證時(shí)的計(jì)算復(fù)雜性.

4）定理證明技術(shù)和模型驗(yàn)證技術(shù)相融合的驗(yàn)證方法 .模型驗(yàn)證的原理是在有窮狀態(tài)上進(jìn)行遍歷搜索，無法處理系統(tǒng)狀態(tài)無限多的情況和狀態(tài)空間爆炸時(shí)模型檢測(cè)的工作效率低下問題.顯然，在利用定理證明的過程中，是可以通過推導(dǎo)來驗(yàn)證無窮狀態(tài)的.

定理證明技術(shù)降低了計(jì)算量，而模型驗(yàn)證技術(shù)又保證了要被檢測(cè)的系統(tǒng)中沒有狀態(tài)遺失.如何將兩者完美地結(jié)合在一起，可以獲得一種高效率、高質(zhì)量的PLC程序驗(yàn)證方法，這將會(huì)是未來一個(gè)重要的研究方向.

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

［2］ FREY G，LITZ L.Formal methods in PLC programming［C］∥International Conference on Systems，Man and Cybernetics，Tennessee.Nashville：IEEE Press，2000：2431-2436.

［3］ HOLLOWAY L E，KROGH B H.Synthesis of feedback logic for a class of controlled petri nets［J］.IEEE Transaction on Automatic Control，1990，35（5）：514-523.

［4］ PELED D A.Software reliability methods［M］.New York：Springer-Verlag，2001：1-9.

［5］ BENDER D F，COMBEMALE B，CREGUT X，et al.Ladder metamodeling and PLC program validation through timed Petri nets［C］∥4th European Conference on Model Driven Architecture-Foundations and Applications.Berlin：Springer，2008：121-136.

［6］ 韓贊東，劉繼國，羅晟.基于控制Petri網(wǎng)的高溫氣冷堆燃料裝卸過程控制系統(tǒng)設(shè)計(jì)方法［J］.核動(dòng)力工程，2008，29（1）：14-18.

［7］ GIUA A，SEATZU C.Modeling and supervisory control of railway networks using Petri nets［J］.IEEE Transaction on Automation Science and Engineering，2008，5（3）：431-445.

［8］ DURMUS M S，SOYLEMEZ M T.Railway signalization and interlocking design via automation Petri nets［C］∥Proceedings of the 7th Asian Control Conference.Hong Kong：［s.n.］，2009：1558-1569.

［9］ 賈洋，肖武，董宏光.基于自組織Petri Net的間歇過程換熱網(wǎng)絡(luò)優(yōu)化設(shè)計(jì)［J］.化工學(xué)報(bào)，2010，61（12）：3167-3171.

［10］ 胡昌華，王青，陳新海.基于Petri網(wǎng)的導(dǎo)彈控制系統(tǒng)故障診斷梯形圖求解法［J］.宇航學(xué)報(bào)，2001，22（1）：37-42.

［11］ 大衛(wèi) R，奧蘭 H.佩特利網(wǎng)和邏輯控制器圖形表示工具（GRAFCET）［M］.北京：機(jī)械工業(yè)出版社，1995：5-6.

［12］ DU Yu-yue，JIANG Chang-jun，ZHOU Meng-chu.A Petri-net-based correctness analysis of internet stock trading systems［J］.IEEE Transactions on Systems，Man and Cybernetics，Part C：Applications and Reviews，2008，38（1）：93-99.

［13］ VENKATESH K，ZHOU Meng-chu，CAUDILL R J.Comparing ladder logic diagrams and Petri nets for sequence controller design through a discrete manufacturing system［J］.IEEE Transactions on Industrial Electronics，1994，41（6）：611-618.

［14］ HANISCH H M，THIEME J，LIIDER A，et al.Modeling of PLC behavior by means of timed net condition／event systems［C］∥Proceedings of the 6th International Conference on Emerging Technologies and Factory Automation.Los Angeles：［s.n.］，1997：391-396.

［15］ KOTINI I，HASSAPIS，MODELING G.Performance evaluation of hybrid systems［C］∥Proceedings of the 1st South-East European Workshop on Formal Methods.Thessaloniki：［s.n.］，2003：21-35.

［16］ FREY G，LITZ L.Correctness analysis of Petri net based logic controllers［C］∥Proceedings of American Control Conference.Chicago：［s.n.］，2000：3165-3166.

［17］ FREY G，LITZ L.Analysis of Petri-net based control algorithms-based properties［C］∥Proceedings of American Control Conference.Chicago：［s.n.］，2000：3172-3176.

［18］ FREY G，LITZ L.Automatic implementation of Petri net based control algorithms on PLC［C］∥Proceedings of A-merican Control Conference.Chicago：［s.n.］，2000：2819-2823.

［19］ WANG Rui，SONG Xiao-yu，ZHU Jian-zhong，et al.Formal modeling and synthesis of programmable logic controllers［J］.Computer in Industry，2010，61（1）：23-31.

［20］ ALUR R，DILL D L.A theory of timed automata［J］.Theoretical Computer Science，1994，26（2）：183-235.

［21］ PERME T.Translation of extended Petri net model into ladder diagram and simulation with PLC［J］.Strojniski vestnik-Journal of Mechanical Engineering，2009，55（10）：608-622.

［22］ DIDEBAN A，KIANI M，ALLA H.Implementing PN-based controller with mutually exclusive transitions by SFC［C］∥Proceedings of the 35th IEEE Annual Conference of Industrial Electronics.Porto：［s.n.］，2009：4353-4358.

［23］ TAHOLAKIAN A，HALES W M M.PNP?PLC：A methodology for designing，simulating and coding PLC based control systems using Petri nets［J］.International Journal of Production Research，1997，35（6）：1743-1762.

［24］ JONES A H，UZAM M，KHAN A H，et al.A general methodology for converting Petri nets into ladder logic：The TPLL methodology［C］∥Proceedings of the 5th Internatioal Conference on Computer Integrated Manufacturing and Automation Technology.Grenoble：［s.n.］，1996：357-362.

［25］ 琚長江，楊根科.Petri網(wǎng)在模塊化制造系統(tǒng)PLC程序設(shè)計(jì)中的應(yīng)用［J］.低壓電器，2006（4）：20-23.

［26］ LEE G B，HAN Z D，LEE J S.Automatic generation of ladder diagram with control Petri net［J］.Journal of Intelligent Manufacturing，2004，15（2）：245-252.

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

［28］ BEHRMANN G，DAVID A，LARSEN K G.A tutorial on uppaal［J］.Lecture Notes in Computer Science，2004，3185：33-35.

［29］ MOKADEM H B，BéRARD 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.

［30］ DA SILVA O E A，DA SILVA L D，GORGONIO K，et al.Obtaining formal models from ladder diagrams［C］∥Proceedings 9th IEEE International Conference on Industrial Informatics.Arapiraca：［s.n.］，2011：796-801.

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

［32］ 陳鋼，宋曉宇，顧明.COQ定理證明器輔助PLC程序驗(yàn)證和分析［J］.北京大學(xué)學(xué)報(bào)：自然科學(xué)版，2010，46（1）：30-34.

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

［34］ HUTH M，RYAN M.Logic in computer science［M］.Cambridge：Cambridge Univercity Press，2004：172-254.

［35］ 古天龍，徐周波.有序二叉決策圖及應(yīng)用［M］.北京：科學(xué)出版社，2009：18-19.

［36］ PAVLOVIC O，EHRICH H D.Model checking PLC software written in function block diagram［C］∥Proceedings of the 3rd International Conference on Software Testing，Verification and Validation.Braunschweig：［s.n.］，2010：439-448.

［37］ GOURCUFF V，DE SMET O，F(xiàn)AURE J M.Efficient representation for formal verification of PLC programs［C］∥Proceedings of the 8th International Workshop on Discrete Event Systems.Michigan：［s.n.］，2006：182-187.

［38］ HOLZMANN G J.The SIPN Model Checker［EB／OL］.［2012-06-15］.http：∥spinroot.com／spin／whatispin.html.

［39］ LUO Ji-liang，NONAMI K.Approach for transforming linear constraints on Petri nets［J］.IEEE Transactions on Automatic Control，2011，56（12）：2751-2765.

［40］ XING Ke-yi，HU Bao-sheng，CHEN Hao-xun.Deadlock avoidance policy for Petri-net modeling of flexible manufacturing systems with shared resources［J］.IEEE Transactions on Automatic Control，1996，41（2）：289-295.

［41］ LI Zhi-wu，ZHOU Meng-chu.Control of elementary and dependent siphons of Petri nets and their application［J］.IEEE Trans Systems，Man，Cybernetics，Part A：Syst Humans，2008，38（1）：133-148.