外文文獻(xiàn)翻譯-基于形式化方法的PLC建模和檢測【中文6440字】 【中英文WORD】

外文文獻(xiàn)翻譯-基于形式化方法的PLC建模和檢測【中文6440字】 【中英文WORD】,中文6440字,中英文WORD,外文文獻(xiàn)翻譯-基于形式化方法的PLC建模和檢測【中文6440字】,【中英文WORD】,外文,文獻(xiàn),翻譯,基于,形式化,方法,PLC,建模,檢測,中文,6440,中英文,WORD J.軟件工程與應(yīng)用，2010年，3，1054-1059 doi:10.4236/jsea.2010.311124網(wǎng)上公布2010年11月（http://www.SciRP.org/journal/jsea）版權(quán)所有 基于形式化方法的PLC建模和檢測 鄭岳山1,2，羅貴明1,2，孫俊波1,2，張俊杰1,2，王振峰1,2 1清華大學(xué)信息科學(xué)與技術(shù)國家重點實驗室，清華大學(xué)，北京，中國；2軟件學(xué)院，清華大學(xué)，北京大學(xué)，中國。 郵箱：championkop@gmail.com, gluo@tsinghua.edu.cn 2010年9月5日，2010年9月16日修訂，2010年9月24日。 摘要 高可靠性是電氣控制設(shè)備的關(guān)鍵性能。PLC結(jié)合計算機技術(shù)，自動的控制技術(shù)和通信技術(shù)，已成為廣泛用于工業(yè)過程自動化中。傳統(tǒng)的驗證方法已不能滿足某些復(fù)雜的PLC系統(tǒng)的要求。因此文章，提出PLC系統(tǒng)的建模和檢測的有效方法。為了確保PLC的高速特性，我們提出了“時間間隔模型”和“通知等待”方法。這兩種方法可以減少狀態(tài)空間，使人們可驗證一些復(fù)雜的PLC系統(tǒng)。此外，這也可以獲得內(nèi)置PLC模型的PROMELA語言的轉(zhuǎn)換并且是PLC檢測建模和設(shè)計檢測PLC系統(tǒng)的建模的工具。使用PLC檢測來驗證一個經(jīng)典的PLC例子，發(fā)現(xiàn)一個反例。雖然在檢測中邏輯錯誤發(fā)生的概率很小，但是致命的，它可能會導(dǎo)致整個系統(tǒng)的崩潰。 關(guān)鍵詞：模型檢測，PLC建模， PLC檢測，形式化方法 1.介紹 PLC是一種自動控制裝置，它可以接收來自傳感器，計算設(shè)備，其他PLC邏輯輸入信號，并輸出處理過的邏輯信號。可以用標(biāo)準(zhǔn)的語言編寫控制算法，如梯形圖（LD），結(jié)構(gòu)文本（ST）或指令表（IL）[1]。 PLC用編程語言來控制大規(guī)模集成電路的技術(shù)已被廣泛用于工業(yè)中[2]。由于安全性重要性的軟件對生命或財產(chǎn)可造成嚴(yán)重威脅，因此檢測安全性重要性的軟件已經(jīng)成為一個必不可少的步驟，來確保軟件的質(zhì)量。目前的檢測方法任然為PLC通過仿真和測試，然而它們無法涵蓋所有??可能的情況，尤其是否是滿足PLC的設(shè)計模型的需求。因此，模型檢測技術(shù)引入到PLC領(lǐng)域，是為了使PLC設(shè)計的理論分析變得重要。 PLC模型檢測的首要步驟是確立PLC型號的，正如建立一個模型從功能圖開始[3]，而PLC模型的建立側(cè)重于時間屬性的確立[4]。它可以模擬自動定時的方法[5]和時間段模建的方法[6]，因此狀態(tài)空間模型將減少相對于自動定時。無論選擇哪種方法，最終可以給出一個抽象的模型[7]。檢測最重要的問題是如何建立一個良好的PLC抽象模型。由于手動建模很容易引入許多錯誤，因此，建立一個集成的建模和測試工具是非常重要的，這是本文關(guān)注的問題之一。 PLC控制程序運行實時操作系統(tǒng)系統(tǒng)（多任務(wù)或單任務(wù)），本文主要是基于多任務(wù)調(diào)度PLC系統(tǒng)。第2節(jié)是對PLC系統(tǒng)的建模方法的介紹。第3節(jié)給出了分析和改進(jìn)這種模式的方法，因為我們需要降低偽錯誤的概率。第4節(jié)設(shè)計PLC檢測模型驗證工具，檢查所建立的模型，包括引進(jìn)PLC程序轉(zhuǎn)換成SPIN的輸入語言PROMELA的代碼。最后用一??個適用于檢查的經(jīng)典PLC的例子，并通過PLC檢測發(fā)現(xiàn)一個重要的反例。 2. PLC建模 模型檢測的三個步驟：建模，屬性描述和驗證。最重要的是如何建立系統(tǒng)模型。 在系統(tǒng)中，PLC控制器不是孤立的，而是受其工作環(huán)境，驅(qū)動程序和人類行為的影響[8]。因此，這些因素也應(yīng)考慮到建模中來。環(huán)境，人和PLC控制器是獨立的，并在邏輯上相互并行。此外，模型檢測工具SPIN的輸入語言PROMELA重點是描述并發(fā)系統(tǒng)的，所以從這個想法出發(fā)，我們建立幾個并發(fā)機構(gòu)，來運用SPIN工具，它也將準(zhǔn)確地描述系統(tǒng)。為了描述方便，它們將被稱為并發(fā)的實體。PLC控制器通過映像表中的符號與并發(fā)實體聯(lián)系。PLC系統(tǒng)的符號包括I（輸入端口），Q（輸出端口）和M（中間繼電器）。圖1是PLC系統(tǒng)模型示意圖。 時間間隔建模策略：使用特定位狀態(tài)的并發(fā)實體的標(biāo)志，代表并發(fā)實體的狀態(tài)下，不考慮到系統(tǒng)時鐘，忽視狀態(tài)的時間差，從而簡化了PLC建模。建模策略不添加系統(tǒng)時鐘的屬性，不完全對應(yīng)與原PLC模型。這主要是由于加入系統(tǒng)時鐘將導(dǎo)致PLC系統(tǒng)模型變得過于龐大，沒有任何模型檢測工具來處理這么大的模型。時間間隔建模的是以PLC在掃描時不考慮遷移量為起點情況下使用的。不管經(jīng)歷多少掃描都將包括在此模型中。換言之，真正的模型是所建模型（時間間隔模型）的一個子集。 真正的PLC環(huán)境是復(fù)雜的，包括了各種硬件和人類行為。下面我們將分析各種不同的PLC環(huán)境中的并發(fā)實體。 圖1：PLC系統(tǒng)模型 1)硬件機構(gòu) PLC系統(tǒng)的硬件實體，主要是一些PLC控制設(shè)備。這些設(shè)備的狀態(tài)可以作為PLC控制器的輸入。因此，硬件實體與其相關(guān)的輸入端口和輸出端口相結(jié)合，并且擁有自己的工作流程，該工作流程是由所需硬件自身決定。這個工作流程可以抽象認(rèn)為成是自動機，此自動機通常用來來描述的硬件的工作狀態(tài)。 定義2.1。硬件實體是一個元組ENV = ，，其中Ienv是輸入端口（I）綁定的硬件實體，Qenv是與實體結(jié)合的輸出端口（Q）。 A是自動機用來描述實體的工作流程，A是一個元組A = ，其中S0是初始狀態(tài)，S是狀態(tài)的集合，而T是一系列的轉(zhuǎn)換。 硬件實體的狀態(tài)是符號I的一個子集，I標(biāo)志著每個狀態(tài)都映射為{真，假}，符號I不會出現(xiàn)既是真又是假（即：獨斷專行）。硬件實體的轉(zhuǎn)變直接表達(dá)為符號Q的子集，也就是說在子集中所有符號Q同時都是真時，將推動狀態(tài)與狀態(tài)之間的遷移。硬件實體的狀態(tài)轉(zhuǎn)換圖，還需要指定一個初始狀態(tài)，轉(zhuǎn)換圖從這種狀態(tài)。 硬件實體的狀態(tài)轉(zhuǎn)換圖是基于符號I的劃分，并沒有考慮到時間屬性。硬件實體狀態(tài)轉(zhuǎn)移圖中被忽略的硬件實體的時間實際上是抽象的，這種抽象是硬件仿真所需的參考。 2)簡單的輸出機構(gòu) 簡單的輸出實體結(jié)合的Q端口不使用I端口，這意味著簡單的輸出實體不具有的狀態(tài)轉(zhuǎn)變圖。簡單的輸出實體是顯示PLC工作狀態(tài)的顯示裝置，就像一個光信號。簡單的輸出實體的與Q端口連接，因此PLC能對Q端口進(jìn)行邏輯設(shè)計。 3)人的行為機構(gòu) 定義2.2人的行為機構(gòu)是一個元組ENV = ，其中Ienv 是I端口綁定的硬件實體，Qenv量是Q端口綁定的實體， A是自動機描述實體的工作流程，A是一個元組A = ，其中S0是初始狀態(tài)，S是狀態(tài)的集合，而T是一系列的轉(zhuǎn)變。 人的行為機構(gòu)與硬件機構(gòu)類似，它們具有相同的狀態(tài)定義。模擬人的行為是很困難的，尤其是一些涉及人的行為的PLC設(shè)計。針對這些困難，人的行為建模應(yīng)采取一個反復(fù)的過程：首先，使用模型驗證建立一個簡單的行為模型，然后，如果沒有找到一個反例子，則建立更復(fù)雜的模型并進(jìn)行驗證，直到找到一個反例或幾乎不能再復(fù)雜為止；最后，如果前面沒有找到有意義的反例，則生成一個完全隨機的人的行為模式（即：所有轉(zhuǎn)讓是真實的人類行為是一個完整的圖形）來核查。然而，完全隨機行為的核查將導(dǎo)致狀態(tài)空間的顯著增加，因此如何選擇一個合適的人類行為模式在建模中是存在很大難度的。如果人的輸入比較簡單，我們可以使用完全隨機的行為建模，否則，你需要認(rèn)真考慮建立一個理性的人的行為模式。 上面我們建立了PLC的環(huán)境和人的行為模型，然后我們將模擬PLC的控制器。當(dāng)打開PLC控制器，。 ?PLC讀取I端口的所有輸入。 ?PLC計算所有的邏輯單元。 ?PLC設(shè)置所有的Q端口。 PLC運行的基本單位稱為網(wǎng)絡(luò)。根據(jù)設(shè)計時設(shè)定的編碼，所有的網(wǎng)絡(luò)開始運行。PLC控制器基本邏輯運算網(wǎng)絡(luò)包括：S觸發(fā)器，R觸發(fā)器，SR觸發(fā)器，EQ觸發(fā)器，RS觸發(fā)器，POS上升沿檢測器，NEG下降沿檢測器等。要運行網(wǎng)絡(luò)建模的基本邏輯，我們采用直接映射方法即：PLC控制器的網(wǎng)絡(luò)行為和邏輯網(wǎng)絡(luò)行為模式是完全等價的。其中S觸發(fā)器，R觸發(fā)器，SR觸發(fā)器，EQ觸發(fā)，RS觸發(fā)器可以直接使用布爾表達(dá)式進(jìn)行觸發(fā)。 3.PLC模型的分析與改進(jìn) 上一節(jié)介紹了PLC系統(tǒng)的建模，根據(jù)此策略我們可以抽象出一個PLC系統(tǒng)作為正式模型的檢測模型。因此，這模式將直接決定模型檢驗結(jié)果的公信力。如果此模型不完全覆蓋原來的系統(tǒng)（我們稱之為小于原始系統(tǒng)），有可能會導(dǎo)致一些錯誤無法檢測出來；如果真正的系統(tǒng)模型可被完全地覆蓋，但其中包含了許多原系統(tǒng)不存在的狀況（我們稱之為大于原來的系統(tǒng)），這可能會引入真正的系統(tǒng)不存在的錯誤，我們把其稱為偽錯誤。因此有兩個建模的要求。 首先，為了找到系統(tǒng)中的所有錯誤，我們將建立一個模型，大到足以覆蓋原系統(tǒng)的所有狀態(tài)。第二，要求模型盡可能接近真實系統(tǒng)，這不僅會減少的狀態(tài)空間，還能提高工作效率。基于要求，我們將給出一個關(guān)于時間間隔模型的分析。 命題1，如果時間間隔模型符合性能，真正的PLC系統(tǒng)模型也符合。 從兩個模型之間的關(guān)系可以得出命題1的正確性結(jié)論。這意味著現(xiàn)實模型中會發(fā)生的所有的情況由時間間隔模型所包括，時間間隔模型是大于實際的模型。如果你不能用時間間隔模型找到一個反例，那你就可以證明真正的PLC模型的正確性;另一方面，如果我們找到一個反例，但無法確定PLC系統(tǒng)中是否真的存在此錯誤，也就是說逆命題是錯誤的。然后，需要手動干預(yù)分析此反例，以確定它是否是一個偽誤差。 時間間隔建模策略可以得到一個抽象的PLC模型，基于對NuSMV的許多研究也可使用類似的時間間隔模型策略來建立PLC系統(tǒng)。然而“時間間隔模型”與真實模型有較大的偏差，從而需要加以改進(jìn)。偏差是指：“時間間隔模式”并不能反映PLC在并發(fā)系統(tǒng)的高速掃描特性和低速特性。也就是說，所有環(huán)境的變化應(yīng)由PLC快速的掃描，而時間間隔模型忽略了PLC的快速特性，這使得在外部環(huán)境的變化可能無法掃描。 為了解決上述問題，考慮到外部高速掃描和低速并發(fā)的物理特性，時間間隔建模策略應(yīng)通過加入的通知等待機制來改善。在時間間隔模型的基礎(chǔ)上，在發(fā)生傳輸后每個并發(fā)狀態(tài)機構(gòu)將被阻止并且等待。只有當(dāng)PLC控制器至少完全掃描一次后，通知等待機制將發(fā)送的信息給機構(gòu)移除阻止并繼續(xù)工作，然后傳輸完成。通過并發(fā)機構(gòu)的通知等待機制來完成傳輸?shù)倪^程，如圖2所示： 圖2：并發(fā)系統(tǒng)的通知等待機構(gòu) ?T0：傳輸開始，阻止并通知PLC控制器。 ?T1-TM：PLC完全掃描m次（m為至少一個）。 ?TM+1：并發(fā)機制從PLC中得到指令，傳輸完成。 這種機制確保每個并發(fā)機構(gòu)狀態(tài)的變化都能由PLC控制器至少一次掃描。 命題2：添加通知等候機制后，模型成為時間間隔模型的一個子集。同時，該模型也可以包括在現(xiàn)實模型中的所有情況，也就是說如果模型添加的通知等候機制符合屬性，真正的PLC系統(tǒng)模型也符合。 這類似于命題1證明與命題2，我們可以看出添加等待通知機制后的模式仍具有良好的性質(zhì)。正如前面提到的，抽象的系統(tǒng)模型有兩個要求：第一，要充分包含真正的系統(tǒng)模型接近真實系統(tǒng)；其次，第一命題證明的時間間隔模型包括了真實的系統(tǒng)，只要使用模型檢測工具證明這種抽象模型滿足一定屬性，那么原系統(tǒng)也將滿足這一點。但這種模式和實際的模型是不完全等價的，它應(yīng)該遠(yuǎn)遠(yuǎn)大于實際的模型。比較時間間隔模型，此模型與實際系統(tǒng)之間的距離將進(jìn)一步減小，大大降低了找出偽錯誤的機會。 模型檢測工具將給出一個違反系統(tǒng)屬性的反例；在實際系統(tǒng)中很容易確定反例的真假。如果原系統(tǒng)中的錯誤真的存在，那么我們就找出一個反例。否則，該錯誤會由于抽象模型大于真實的系統(tǒng)，而成為一個偽誤差。因此，雖然這個時間間隔模型和原來的系統(tǒng)是不能完全等同的，但通過這個模型我們可以判斷系統(tǒng)是否符合一定的屬性，如果不是我們可以找到一個具體的反例（仍需要更多的研究以確定它是否是一個偽誤差）。 模型是不等于原系統(tǒng)的，主要是因為在實際系統(tǒng)中有許多因素難以模型，其中有一些可能會引起錯誤。如果所有的因素都為藍(lán)本，將導(dǎo)致建立一個巨大的不可檢測或根本無法實現(xiàn)的模型。時間間隔模型是從真正的系統(tǒng)和他們的模型中抽象出來的，可大大減少狀態(tài)空間和時間復(fù)雜度。同時，添加通知等候機制，模型變得更接近真實系統(tǒng)，不僅降低了時間復(fù)雜度，同時減少了前面提到的偽錯誤。 4.PLC模型檢測 PLC被廣泛的使??用在許多領(lǐng)域，并有豐富的品種，這是一個很大的研究領(lǐng)域。任何PLC工作在包括不同的設(shè)備和人員的環(huán)境中，所以PLC系統(tǒng)是并發(fā)的。如果出現(xiàn)誤差，PLC系統(tǒng)很難在同一時間找到錯誤的所在，其中主要是因為邏輯設(shè)計錯誤，但不會產(chǎn)生的計算誤差。所以我們專注于PLC程序的邏輯過程的檢測，這個邏輯可以完全通過為邏輯來描述。因此，為了簡化PLC程序模型，專注于模型檢測，我們做如下設(shè)置： ?PLC邏輯控制程序，所有的控制變量只有兩個狀態(tài)0和1; ?PLC程序并發(fā)的環(huán)境中運行。在這種情況下，PLC編程更可能會有一些不容易發(fā)現(xiàn)的錯誤。 就上述特點，我們使用的模型檢測工具SPIN（我們的PLC檢查工具也識別NuSMV）對上述建立的模型進(jìn)行檢測。我們制定了一系列的轉(zhuǎn)變規(guī)則，用SPIN的輸入語言PROMELA建立上述模型中，系統(tǒng)屬性也需要被翻譯成PROMELA語句，SPIN將會把它們放在一起，然后進(jìn)行檢測。 PROMELA語言是一種C類語言，它們在語義上相似。所以我們將只舉幾個例子來展示翻譯的基本概念。要詳細(xì)了解PROMELA語言，請訪問www.spinroot.com 我們將介紹作為SPIK輸入的一個PROMELA文件的三個部分。 1）PLC控制器守則 PLC控制器由多個網(wǎng)絡(luò)組成的， PLC控制器代碼也從網(wǎng)絡(luò)中產(chǎn)生。當(dāng)然在這之前，應(yīng)先聲明所需的變量。每個網(wǎng)絡(luò)都有它的輸入端口和輸出端口，每個端口可以用一個布爾表達(dá)式。我們通過邏輯運算來設(shè)計所有的輸入端口輸出端口的分配值,這是PLC網(wǎng)絡(luò)的翻譯方法。 下面是一個轉(zhuǎn)變?yōu)镾R網(wǎng)絡(luò)的例子： if :: Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp（S）是S端口的布爾表達(dá)式 Exp（R）是R端口的布爾表達(dá)式 Q是輸出端口*/ 2）并發(fā)機構(gòu)守則 我們認(rèn)為每個并發(fā)機構(gòu)是一個獨特的過程，不管是人的行為或設(shè)備。這些過程共享變量與PLC控制器的過程。這就確保了系統(tǒng)的并發(fā)性。 在本文的第二部分中，我們討論所有并發(fā)機構(gòu)的建模作為自動機。自動機的意思是從一個狀態(tài)轉(zhuǎn)變到另一個。我們使用的I端口形成的機構(gòu)狀態(tài)，使用goto語句作為轉(zhuǎn)變語句（就像匯編語言）。一個簡單的例子如下所示: StateA: atomic { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /*StateA的狀態(tài)A的標(biāo)志 Q1，Q2是轉(zhuǎn)換條件 IB是所設(shè)置的到達(dá)狀態(tài)B的價 goto StateB意味跳轉(zhuǎn)到狀態(tài)B*/ 3）屬性守則 屬性是PLC系統(tǒng)必須遵守的規(guī)則。我們使用LTL（線性時間邏輯）公式作為輸入方式。由于SPIK的機制，我們應(yīng)該編寫反屬性。SPIN將找出其屬性在什么情況下發(fā)生，此狀況則是一個反例。 我們不能直接寫LTL公式，但使用宏指令。首先，我們應(yīng)該用宏指令定義所有的LKL命題（例如定義p i5 == 0），然后我們用定義的命題，形成一個LTL公式。通過使用“SPIN-F”指令，SPIN可以自動轉(zhuǎn)換LTL公式的PROMELA代碼。 4)通知等候機制 在建模的討論中，我們提出了添加通知等候機制。這種機制還需要在代碼中反映出來，具體做法是確定每個非PLC過程（PLC控制器除外）的位變量，將其作為一個信號。自動機轉(zhuǎn)換到狀態(tài)標(biāo)簽時，設(shè)置的信號變量為0，直到下一個變量到來時變?yōu)?，否則繼續(xù)保持為0。PROMELA語法結(jié)果的特點，是此過程將保存起來。而在在PLC過程中則沒有這樣的限制，相反，PLC過程可以設(shè)置這些變量為1，從而確保每一動作都必須經(jīng)過至少一個PLC的掃描完成。這就是所謂的等待通知機制。 遵循上述四個步驟，我們得到了一個完整的SPIN輸入文件代碼，然后我們就可以使用SPIK來檢測模型。對于SPIK模型檢測器的運行步驟，請參閱SPIK的使用手冊（訪問www.spinroot.com）。SPIK能給出結(jié)果是否是所找的反例，而我們可以通過使用跟蹤文件的方法得出上述結(jié)論。 使用這種檢測機制，我們開發(fā)了一個能建模檢測PLC模型的工具。它有助于建立可視化模型和實施檢測，并且可以舉出一個簡單的分析結(jié)果。當(dāng)然，發(fā)現(xiàn)反例則需要手動檢測，以確保它是否是一個真正的反例，然而，有了跟蹤文件的幫助使這成了一個并不困難的任務(wù)。我們還成功的采用了一些PLC檢測（在下一節(jié)中所示）。教科書中發(fā)現(xiàn)的一個經(jīng)典例子可做反例。雖然發(fā)生反例的概率是很低的，但它確實存在，并且可能會產(chǎn)生嚴(yán)重的后果。文章中此工具也證明了理論的正確性和有效性。 5.運行PLC檢查 通過檢測雙門通道模型，來展示PLC檢測的有效性。雙門通道是通過一個封閉的空間來防止與外界的接觸。 我們通過輸入梯形圖，并發(fā)機構(gòu)工具和定義屬性來執(zhí)行檢測。如圖3所示結(jié)果 圖3：模型檢測結(jié)果 正如我們所看到的：是一個錯誤的結(jié)果，而且事實證明這是一個真正的通過手動檢測跟蹤文件得出的反例，也就是說我們的PLC程序檢測這種機制是有效的。 6.結(jié)論 本文是研究的理論建模和檢測PLC系統(tǒng)的優(yōu)化方法。對PLC建模的要求進(jìn)行了分析，并同過時間間隔策略建立起并發(fā)系統(tǒng)。然后，我們證明了時間間隔模式的PLC系統(tǒng)中的一個超集，并加入通知等候機制來降低了模型。通知等候機制還確保在系統(tǒng)中的所有的變化可以被PLC控制器掃描，并且我們找到了系統(tǒng)誤差檢測的反例，最后給出使用SPIK檢測模型的方式。此外，引入了相應(yīng)的模型檢測工具PLC檢測器。在此階段，該機制仍然有許多缺陷，如定時器的處理，但它在解決空間探索問題上有很大而獨特的優(yōu)勢。我們?nèi)栽诜e極的探索此類問題。 9 指導(dǎo)教師意見 指導(dǎo)教師簽字： 年 月 日 J. Software Engineering & Applications, 2010, 3, 1054-1059 doi:10.4236/jsea.2010.311124 Published Online November 2010 (http://www.SciRP.org/journal/jsea) Copyright PLC Modeling and Checking Based on Formal Method* Yueshan Zheng1,2, Guiming Luo1,2, Junbo Sun1,2, Junjie Zhang1,2, Zhenfeng Wang1,2 1Tsinghua National Laboratory for Information Science and Technology, Tsinghua University, Beijing, China; 2School of Software, Tsinghua University, Beijing, China. Email: championkop@gmail.com, gluo@tsinghua.edu.cn Received September 5th, 2010; revised September 16th, 2010; accepted September 24th, 2010. ABSTRACT High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the PROMAL language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally. Keywords: Model Checking, PLC Modeling, PLC-Checker, Formal Method 1. Introduction PLC is an automatic control device that can receive information from sensors, computing device or other PLC logic input signal, and output the logic signal processed. The control algorithm can be written using standard language, such as Ladder Diagram (LD), Structured Text (ST) or Instruction List (IL) [1]. The technique of PLC using programmable language to control large scale integrated circuit has been widely used in industry [2]. Because of safety critical software can cause serious damage to life or property, verification of safety critical software has become an indispensable step required to assure software quality. The present verifying method for the PLC is still stuck by simulation and testing. However, they cannot cover all possible cases, especial whether the design model of PLC to meet the demand. Therefore, the model checking technology is introduced into the field of PLC. To give theoretical analysis of PLC design becomes important. The primary step of PLC model checking is to the establishment of PLC model, such as establish a model from Function Charts [3]. The PLC model focuses on the establishment of the time attributes [4]. It can be modeled by the method of timed automata [5] or time period modeling method [6]. Thus state space of the model will be decreased compared to timed automata. Either way one choose, eventually an abstract model can be given [7]. How to build a good PLC abstract model is the most important issue to the checking. As the manually modeling is easy to introduce many errors, so the establishment of an integrated modeling and testing tool is very important, and this is one of the issues of concern to this paper. PLC control program runs in real-time operating sys-tem (multi-task or single-task); this paper is mainly based on multi-task scheduling PLC system. Section 2 of the article has an introduction to the modeling method of PLC system. Section 3 gives the analysis and improvement of this model as we need to reduce the probability of pseudo-errors. Section IV designs a model checking tool PLC-Checker to check the established model, including introduce the way of converting PLC program into SPIN's input language PROMELA code. Finally, a classical PLC example is applied to check and a critical counter-example is found by the PLC-Checker. 2. PLC Modeling There are three steps of model checking: modeling, property description, and verification. The most important is how to build the system model. In the system, PLC controller is not isolated, but has interaction with its working environment, driver and human [8]. Therefore, these factors should also be modeling. The environment, human, and the PLC controller is independent and concurrent with each other in logic. Also, the model checker SPIN’s input language PROMELA is focused on describing the concurrent, so starting from this idea, we build these factors into several concurrent processes to fit the checking from SPIN, it will also accurately describe the system. To describe conveniently, they will be called concurrent entities. PLC controller interacts with the concurrent entities through the symbols in image table. The symbols of PLC system include I (input port), Q (output port), and M (intermediate relay). Figure 1 is a diagram of PLC system model. Time interval modeling strategy: using the flag which specific the bit state of concurrent entities to represent the concurrent entities in the state, without regard to the system clock. This may neglect the time difference of states, thus simplifying the PLC model. The modeling strategy does not add the system clock properties, not fully corresponds with the original PLC model. That is mainly due to join the system clock will cause PLC system model become too large, there is no for model checking tool to deal with such a large model. The starting point for modeling the state like this is not to consider the number of PLC scans when a migration is experienced. No matter how many scans it experienced, they will all include in this model. In other words, the real model will be a subset of the built model (Time interval model). The real PLC environment is complex, and includes a variety of hardware and human behavior. The following we will give an analysis of different kinds of PLC environment concurrent entities 1) Hardware entity Hardware entity of the PLC system is mainly some equipment that PLC controls. The state of these equipments can be the input of PLC controller. Therefore, the hardware entity binding with its associated I and Q, while the hardware has its own workflow, this workflow is decided by the hardware requirements. This work flow can be abstracted into automata. This automata is used to describe the working status of the hardware. Definition 2.1. A Hardware entity is a tuple Env = , where Ienv is the I port binding with the hardware entity, Qenv is the Q port binding with the entity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. The states of hardware entities is a subset of I symbols, and the I’s sign each state are all mapped to {True, False}, the I symbol do not appear in the state can be either True or False (that is: act arbitrarily). The transfer of the hardware entities directly expressed with the subset of Q symbols, said that all Q symbols in the subset be true at the same time will drive migration between states. The state transition diagram of hardware entities also need to specify an initial state, the transitions graph starts from this state. The hardware entities’ states of transition diagram are based on the division of symbol I, and time properties are not taken into account. Hardware entities state transition diagram is actually an abstract of hardware entity ignored time, the abstract simulation required reference of the hardware. 2) Simple output entity Simple output entity only binding with the Q port without using I port, that means the simple output entities does not have a state transition diagram. Simple output entity is the equipment that shows the work state of PLC, like a signal light. The usage of the simple output entity is to bind with the Q port such that the PLC can make its logical design. 3) Human behavior entity Definition 2.2. A Human behavior entity is a tuple Env = < Ienv, A>, where Ienv is the I port binding with the hardware entity, Qenv is the Q port binding with the entity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. Human behavior entity is similar with Hardware entity; they have the same state definition. It is difficult to simulate the behavior of people, especially the design of a PLC to a number of individuals involved. In response to these difficulties, human behavior modeling should take an iterative process: First, a simple behavior model is built use the model validation; then, if not find a counter example, a more complex model is built, and validate, until find a counter-example or hard to be more complex; Finally, if not previously find a meaningful counter-ex-ample, then generate a completely random person behavior model (that is: human behavior is a complete graph with all transfers be true) to verification. However, completely random behavior’s verification will cause state space increases dramatically, so how to choose a suitable model of human behavior is the difficulty in modeling. If the person's input is relatively simple, we can use completely random behavior modeling, otherwise, you need to seriously consider the establishment of a rational model of human behavior. We build model to PLC environment and the human behaviors above, and then we will model the PLC controller. PLC controller will be in a loop when it is turned on. ?PLC read all the input from I ports. ?PLC compute all the logic units. ?PLC set all the Q ports. PLC process on the basic unit called Network. All the networks will operate in order according to the number set when design. Basic logic operation network of PLC controller includes: S Trigger, R Trigger, SR flip-flop, EQ trigger, RS flip-flop, POS rising edge detector, NEG falling edge detector and so on. To the basic logic operation network modeling, we use direct mapping strategy, namely: PLC controller model of network behavior and the logical behavior of the network is completely equivalent. Where S trigger, R trigger, SR flip-flop, EQ trigger, RS flip-flop can directly use Boolean expressions to mapped to their behavior. 3. PLC Model’s Analysis and Improvement The previous section describes the modeling of a PLC system, according to this strategy; we can abstract a PLC system as a formal model for model checking. Therefore, this model will have a direct decision of the credibility of the model checking results. If the model does not fully cover the original system (we call smaller than the original system), there may cause some errors are not detected; model can be completely covered if the real system, but it contains many states that the original system does not exist (we call it larger than the original system), this may introduce some errors that real system do not exist. Here called it pseudo-error. So there are two requirements for modeling strategy. First, in order to find all the errors in the system, we shall build a model large enough to cover all the states in the original system; second, require the model be close to the real system as much as possible. This will not only reduce the state space, but also improve efficiency. Base on the requirements, we will give an analysis about the Time interval model. Proposition 1 If time interval model conforms the property, real PLC system model also conforms. The correctness of Proposition 1 can be concluded from the relationship between the two models. That means all the situations that real model will happen are included by the time interval model, time interval model is larger than the real model. If you couldn’t find a counter-example by using a time interval model, you can prove the correctness of the real PLC model; the other hand, if we find a counter-example, we cannot determine whether there are errors in the real PLC system. That is to say the converse of proposition 1 is wrong. Then manual intervention is required to analyze the anti-cases to determine whether it is a pseudo-error. Time interval modeling strategy can get an abstract PLC model, many research based on NuSMV also use the strategy similar to time interval model to model PLC system. However, the “time interval model” has large deviation with the real model, it needs to be improved. The deviation is: “time interval model” does not reflect the high-speed scanning characteristics of PLC and low-speed characteristics of concurrent entities. That is, all the changes in the environment should be scanned by the high-speed PLC, but the time interval model ignores the high-speed characteristics of PLC, which makes changes in the external environment may not be scanned. To address the above issues, taking into account the external high-speed scanning and low-speed concurrent physical characteristics, time interval modeling strategy shall be improved by adding a notice-waiting mechanism. Base on the time interval model, each concurrent state entity must be blocked and wait after the transfer took place. Only if the PLC controller completely scans at least once, the notice-waiting mechanism will sent messages to concurrent entities to remove the block and go on working. Then the transfer finished. The process that concurrent entities work to complete the migration by notice-waiting mechanism is shown in Figure 2: ?t0: Transfer start, block and notice the PLC controller. ?t1-tm: PLC completely scanned m times (m is one at least). ?tm+1: The concurrent entities get the notice from the PLC, transfer finish. This mechanism ensures every state change of concurrent entities can be scanned at least once by PLC controller. Proposition 2 After add the notice-waiting mechanism, the model become a subset of the time interval model. At the same time, the model can also include the entire situation in real model. That is to say, if a model which adds the notice-waiting mechanism conforms the property, real PLC system model also conforms. It is similar to prove proposition 2 with proposition 1. By proposition 2 we can see, after add the notice-waiting mechanism the model still has a good nature. As previously mentioned, an abstract system model has two requirements: first, to fully contain the real system, followed by the model as close to real systems. The first proposition is proved that the time interval model includes the real systems, as long as the use of model checking tools to prove that this abstract model satisfies a certain property, then the true nature of the system will also satisfy this. But this model and the real model is not entirely equal, it should be far greater than the real model. Compare to time interval model, this model further reduced the distance between the real systems, greatly reduce the chance that finding out pseudo-errors. Model checking tool will give out a counter-example violate the property of the system; it is easy to manually determine the counter-examples in the real system is true or not. If the errors in the original system really exist, then we find a counter-example. Otherwise, this error is because the abstract model is larger than the real system, it is a pseudo-error. Therefore, although this time interval model and the original system are not fully equivalent, but by this model, we can judge a system meets a certain property, if not we can find a specific counter-example (still needs more examine to determine whether it is a pseudo-error). Model is not equivalent with the original system, mainly because there are many factors difficult to model in real systems, some of which may give rise to error. If all the factors are modeled, that will lead to the establishment of a huge model that cannot check, or simply cannot be achieved. Time interval model abstract the key factors from the real system and model them, greatly reducing the state space, and reduce the time complexity. Meanwhile, add by the notice-waiting mechanism, the model become much closer to real systems, not only reduces the time complexity, while it reduced the pseudo-errors mentioned before. 4. PLC Model Checking PLC is widely used in many applications, and has many devices; this is a large area of research. Any PLC work in the environment that includes different equipment and people, so PLC system is concurrent. At the same time, a PLC system difficult to find if there are some errors, mostly because of the logical design errors, but not the calculation error. So we focus on the detection of PLC program logic process, and this logic can be completely described by bit logic. Therefore, in order to simplify the PLC program model, focused on model checking, we make the following settings: ?PLC is a logic control program, all the control variables only has two states 0 and 1; ?PLC program is run in concurrent environment. In this case, PLC programming is more likely to have some errors not easy to find. In respect of the above characteristics, we use the model checking tool SPIN (our tools PLC-Checker also realized NuSMV) on the above established model for checking. We made a series of transformation rules, build the above model into SPIN's input language PROMELA, the system property also need to be translated into PROMELA, SPIN will put them together and then perform detection. PROMELA language is a C class language, they are similar in semantic. So we will only give some examples to show the basic concept of the translation. To see the details of PROMELA language, please visit www.spinroot.com. We will introduce the three part of a PROMELA file as the input of SPIN. 1) Code of PLC controller PLC controller is composed of multiple networks. Code of PLC controller is also generated from the network. Of course, before that, you should declare the variables you need. Each network has its input ports and output ports, each port can be indicate by a Boolean expression. We assign the output port’s value through the logic computing of all the input port. This is the translation approach of PLC network. Here is an example of converting SR network: if :: Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp(S) is the Boolean expression of S port Exp(R) is the Boolean expression of R port Q is the output port */ 2) Code of concurrent entities We consider each concurrent entity a unique process, no matter it is human behavior or equipment. These processes share variables with PLC controller process. This must be done to ensure the concurrency of the system. In the 2nd part of this paper, we discuss that all the concurrent entities are modeled as an automata. The meaning of automata is to transfer from a state to another. We use the I port to form the state of the entities. Use goto statement as the transfer (just like in Assembly language). A simple example is shown like below: StateA: atomic { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /* StateA is the label of State A Q1, Q2 is the condition of transfer IB is to set the state value to the value of state B goto StateB means jump to stateB */ 3) Code of property Property is the rule that the PLC system must obey. We use LTL (Linear Time Logic) formula as the input format. We should write the counter-property because of the mechanism of SPIN. SPIN will find a situation that our property happens, that should be a counter-example. We couldn’t directly write the LTL formula, but by using macros. Firstly we should define all the propositions in the LTL in a macro