外文文獻(xiàn)翻譯-基于形式化方法的PLC建模和檢測(cè)【中文6440字】 【中英文WORD】,中文6440字,中英文WORD,外文文獻(xiàn)翻譯-基于形式化方法的PLC建模和檢測(cè)【中文6440字】,【中英文WORD】,外文,文獻(xiàn),翻譯,基于,形式化,方法,PLC,建模,檢測(cè),中文,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建模和檢測(cè) 鄭岳山1,2，羅貴明1,2，孫俊波1,2，張俊杰1,2，王振峰1,2 1清華大學(xué)信息科學(xué)與技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室，清華大學(xué)，北京，中國(guó)；2軟件學(xué)院，清華大學(xué)，北京大學(xué)，中國(guó)。 郵箱：championkop@gmail.com, gluo@tsinghua.edu.cn 2010年9月5日，2010年9月16日修訂，2010年9月24日。 摘要 高可靠性是電氣控制設(shè)備的關(guān)鍵性能。PLC結(jié)合計(jì)算機(jī)技術(shù)，自動(dòng)的控制技術(shù)和通信技術(shù)，已成為廣泛用于工業(yè)過程自動(dòng)化中。傳統(tǒng)的驗(yàn)證方法已不能滿足某些復(fù)雜的PLC系統(tǒng)的要求。因此文章，提出PLC系統(tǒng)的建模和檢測(cè)的有效方法。為了確保PLC的高速特性，我們提出了“時(shí)間間隔模型”和“通知等待”方法。這兩種方法可以減少狀態(tài)空間，使人們可驗(yàn)證一些復(fù)雜的PLC系統(tǒng)。此外，這也可以獲得內(nèi)置PLC模型的PROMELA語(yǔ)言的轉(zhuǎn)換并且是PLC檢測(cè)建模和設(shè)計(jì)檢測(cè)PLC系統(tǒng)的建模的工具。使用PLC檢測(cè)來(lái)驗(yàn)證一個(gè)經(jīng)典的PLC例子，發(fā)現(xiàn)一個(gè)反例。雖然在檢測(cè)中邏輯錯(cuò)誤發(fā)生的概率很小，但是致命的，它可能會(huì)導(dǎo)致整個(gè)系統(tǒng)的崩潰。 關(guān)鍵詞：模型檢測(cè)，PLC建模， PLC檢測(cè)，形式化方法 1.介紹 PLC是一種自動(dòng)控制裝置，它可以接收來(lái)自傳感器，計(jì)算設(shè)備，其他PLC邏輯輸入信號(hào)，并輸出處理過的邏輯信號(hào)?？梢杂脴?biāo)準(zhǔn)的語(yǔ)言編寫控制算法，如梯形圖（LD），結(jié)構(gòu)文本（ST）或指令表（IL）[1]。 PLC用編程語(yǔ)言來(lái)控制大規(guī)模集成電路的技術(shù)已被廣泛用于工業(yè)中[2]。由于安全性重要性的軟件對(duì)生命或財(cái)產(chǎn)可造成嚴(yán)重威脅，因此檢測(cè)安全性重要性的軟件已經(jīng)成為一個(gè)必不可少的步驟，來(lái)確保軟件的質(zhì)量。目前的檢測(cè)方法任然為PLC通過仿真和測(cè)試，然而它們無(wú)法涵蓋所有??可能的情況，尤其是否是滿足PLC的設(shè)計(jì)模型的需求。因此，模型檢測(cè)技術(shù)引入到PLC領(lǐng)域，是為了使PLC設(shè)計(jì)的理論分析變得重要。 PLC模型檢測(cè)的首要步驟是確立PLC型號(hào)的，正如建立一個(gè)模型從功能圖開始[3]，而PLC模型的建立側(cè)重于時(shí)間屬性的確立[4]。它可以模擬自動(dòng)定時(shí)的方法[5]和時(shí)間段模建的方法[6]，因此狀態(tài)空間模型將減少相對(duì)于自動(dòng)定時(shí)。無(wú)論選擇哪種方法，最終可以給出一個(gè)抽象的模型[7]。檢測(cè)最重要的問題是如何建立一個(gè)良好的PLC抽象模型。由于手動(dòng)建模很容易引入許多錯(cuò)誤，因此，建立一個(gè)集成的建模和測(cè)試工具是非常重要的，這是本文關(guān)注的問題之一。 PLC控制程序運(yùn)行實(shí)時(shí)操作系統(tǒng)系統(tǒng)（多任務(wù)或單任務(wù)），本文主要是基于多任務(wù)調(diào)度PLC系統(tǒng)。第2節(jié)是對(duì)PLC系統(tǒng)的建模方法的介紹。第3節(jié)給出了分析和改進(jìn)這種模式的方法，因?yàn)槲覀冃枰档蛡五e(cuò)誤的概率。第4節(jié)設(shè)計(jì)PLC檢測(cè)模型驗(yàn)證工具，檢查所建立的模型，包括引進(jìn)PLC程序轉(zhuǎn)換成SPIN的輸入語(yǔ)言PROMELA的代碼。最后用一??個(gè)適用于檢查的經(jīng)典PLC的例子，并通過PLC檢測(cè)發(fā)現(xiàn)一個(gè)重要的反例。 2. PLC建模 模型檢測(cè)的三個(gè)步驟：建模，屬性描述和驗(yàn)證。最重要的是如何建立系統(tǒng)模型。 在系統(tǒng)中，PLC控制器不是孤立的，而是受其工作環(huán)境，驅(qū)動(dòng)程序和人類行為的影響[8]。因此，這些因素也應(yīng)考慮到建模中來(lái)。環(huán)境，人和PLC控制器是獨(dú)立的，并在邏輯上相互并行。此外，模型檢測(cè)工具SPIN的輸入語(yǔ)言PROMELA重點(diǎn)是描述并發(fā)系統(tǒng)的，所以從這個(gè)想法出發(fā)，我們建立幾個(gè)并發(fā)機(jī)構(gòu)，來(lái)運(yùn)用SPIN工具，它也將準(zhǔn)確地描述系統(tǒng)。為了描述方便，它們將被稱為并發(fā)的實(shí)體。PLC控制器通過映像表中的符號(hào)與并發(fā)實(shí)體聯(lián)系。PLC系統(tǒng)的符號(hào)包括I（輸入端口），Q（輸出端口）和M（中間繼電器）。圖1是PLC系統(tǒng)模型示意圖。 時(shí)間間隔建模策略：使用特定位狀態(tài)的并發(fā)實(shí)體的標(biāo)志，代表并發(fā)實(shí)體的狀態(tài)下，不考慮到系統(tǒng)時(shí)鐘，忽視狀態(tài)的時(shí)間差，從而簡(jiǎn)化了PLC建模。建模策略不添加系統(tǒng)時(shí)鐘的屬性，不完全對(duì)應(yīng)與原PLC模型。這主要是由于加入系統(tǒng)時(shí)鐘將導(dǎo)致PLC系統(tǒng)模型變得過于龐大，沒有任何模型檢測(cè)工具來(lái)處理這么大的模型。時(shí)間間隔建模的是以PLC在掃描時(shí)不考慮遷移量為起點(diǎn)情況下使用的。不管經(jīng)歷多少掃描都將包括在此模型中。換言之，真正的模型是所建模型（時(shí)間間隔模型）的一個(gè)子集。 真正的PLC環(huán)境是復(fù)雜的，包括了各種硬件和人類行為。下面我們將分析各種不同的PLC環(huán)境中的并發(fā)實(shí)體。 圖1：PLC系統(tǒng)模型 1)硬件機(jī)構(gòu) PLC系統(tǒng)的硬件實(shí)體，主要是一些PLC控制設(shè)備。這些設(shè)備的狀態(tài)可以作為PLC控制器的輸入。因此，硬件實(shí)體與其相關(guān)的輸入端口和輸出端口相結(jié)合，并且擁有自己的工作流程，該工作流程是由所需硬件自身決定。這個(gè)工作流程可以抽象認(rèn)為成是自動(dòng)機(jī)，此自動(dòng)機(jī)通常用來(lái)來(lái)描述的硬件的工作狀態(tài)。 定義2.1。硬件實(shí)體是一個(gè)元組ENV = ，，其中Ienv是輸入端口（I）綁定的硬件實(shí)體，Qenv是與實(shí)體結(jié)合的輸出端口（Q）。 A是自動(dòng)機(jī)用來(lái)描述實(shí)體的工作流程，A是一個(gè)元組A = ，其中S0是初始狀態(tài)，S是狀態(tài)的集合，而T是一系列的轉(zhuǎn)換。 硬件實(shí)體的狀態(tài)是符號(hào)I的一個(gè)子集，I標(biāo)志著每個(gè)狀態(tài)都映射為{真，假}，符號(hào)I不會(huì)出現(xiàn)既是真又是假（即：獨(dú)斷專行）。硬件實(shí)體的轉(zhuǎn)變直接表達(dá)為符號(hào)Q的子集，也就是說在子集中所有符號(hào)Q同時(shí)都是真時(shí)，將推動(dòng)狀態(tài)與狀態(tài)之間的遷移。硬件實(shí)體的狀態(tài)轉(zhuǎn)換圖，還需要指定一個(gè)初始狀態(tài)，轉(zhuǎn)換圖從這種狀態(tài)。 硬件實(shí)體的狀態(tài)轉(zhuǎn)換圖是基于符號(hào)I的劃分，并沒有考慮到時(shí)間屬性。硬件實(shí)體狀態(tài)轉(zhuǎn)移圖中被忽略的硬件實(shí)體的時(shí)間實(shí)際上是抽象的，這種抽象是硬件仿真所需的參考。 2)簡(jiǎn)單的輸出機(jī)構(gòu) 簡(jiǎn)單的輸出實(shí)體結(jié)合的Q端口不使用I端口，這意味著簡(jiǎn)單的輸出實(shí)體不具有的狀態(tài)轉(zhuǎn)變圖。簡(jiǎn)單的輸出實(shí)體是顯示PLC工作狀態(tài)的顯示裝置，就像一個(gè)光信號(hào)。簡(jiǎn)單的輸出實(shí)體的與Q端口連接，因此PLC能對(duì)Q端口進(jìn)行邏輯設(shè)計(jì)。 3)人的行為機(jī)構(gòu) 定義2.2人的行為機(jī)構(gòu)是一個(gè)元組ENV = ，其中Ienv 是I端口綁定的硬件實(shí)體，Qenv量是Q端口綁定的實(shí)體， A是自動(dòng)機(jī)描述實(shí)體的工作流程，A是一個(gè)元組A = ，其中S0是初始狀態(tài)，S是狀態(tài)的集合，而T是一系列的轉(zhuǎn)變。 人的行為機(jī)構(gòu)與硬件機(jī)構(gòu)類似，它們具有相同的狀態(tài)定義。模擬人的行為是很困難的，尤其是一些涉及人的行為的PLC設(shè)計(jì)。針對(duì)這些困難，人的行為建模應(yīng)采取一個(gè)反復(fù)的過程：首先，使用模型驗(yàn)證建立一個(gè)簡(jiǎn)單的行為模型，然后，如果沒有找到一個(gè)反例子，則建立更復(fù)雜的模型并進(jìn)行驗(yàn)證，直到找到一個(gè)反例或幾乎不能再?gòu)?fù)雜為止；最后，如果前面沒有找到有意義的反例，則生成一個(gè)完全隨機(jī)的人的行為模式（即：所有轉(zhuǎn)讓是真實(shí)的人類行為是一個(gè)完整的圖形）來(lái)核查。然而，完全隨機(jī)行為的核查將導(dǎo)致狀態(tài)空間的顯著增加，因此如何選擇一個(gè)合適的人類行為模式在建模中是存在很大難度的。如果人的輸入比較簡(jiǎn)單，我們可以使用完全隨機(jī)的行為建模，否則，你需要認(rèn)真考慮建立一個(gè)理性的人的行為模式。 上面我們建立了PLC的環(huán)境和人的行為模型，然后我們將模擬PLC的控制器。當(dāng)打開PLC控制器，。 ?PLC讀取I端口的所有輸入。 ?PLC計(jì)算所有的邏輯單元。 ?PLC設(shè)置所有的Q端口。 PLC運(yùn)行的基本單位稱為網(wǎng)絡(luò)。根據(jù)設(shè)計(jì)時(shí)設(shè)定的編碼，所有的網(wǎng)絡(luò)開始運(yùn)行。PLC控制器基本邏輯運(yùn)算網(wǎng)絡(luò)包括：S觸發(fā)器，R觸發(fā)器，SR觸發(fā)器，EQ觸發(fā)器，RS觸發(fā)器，POS上升沿檢測(cè)器，NEG下降沿檢測(cè)器等。要運(yùn)行網(wǎng)絡(luò)建模的基本邏輯，我們采用直接映射方法即：PLC控制器的網(wǎng)絡(luò)行為和邏輯網(wǎng)絡(luò)行為模式是完全等價(jià)的。其中S觸發(fā)器，R觸發(fā)器，SR觸發(fā)器，EQ觸發(fā)，RS觸發(fā)器可以直接使用布爾表達(dá)式進(jìn)行觸發(fā)。 3.PLC模型的分析與改進(jìn) 上一節(jié)介紹了PLC系統(tǒng)的建模，根據(jù)此策略我們可以抽象出一個(gè)PLC系統(tǒng)作為正式模型的檢測(cè)模型。因此，這模式將直接決定模型檢驗(yàn)結(jié)果的公信力。如果此模型不完全覆蓋原來(lái)的系統(tǒng)（我們稱之為小于原始系統(tǒng)），有可能會(huì)導(dǎo)致一些錯(cuò)誤無(wú)法檢測(cè)出來(lái)；如果真正的系統(tǒng)模型可被完全地覆蓋，但其中包含了許多原系統(tǒng)不存在的狀況（我們稱之為大于原來(lái)的系統(tǒng)），這可能會(huì)引入真正的系統(tǒng)不存在的錯(cuò)誤，我們把其稱為偽錯(cuò)誤。因此有兩個(gè)建模的要求。 首先，為了找到系統(tǒng)中的所有錯(cuò)誤，我們將建立一個(gè)模型，大到足以覆蓋原系統(tǒng)的所有狀態(tài)。第二，要求模型盡可能接近真實(shí)系統(tǒng)，這不僅會(huì)減少的狀態(tài)空間，還能提高工作效率?；谝?，我們將給出一個(gè)關(guān)于時(shí)間間隔模型的分析。 命題1，如果時(shí)間間隔模型符合性能，真正的PLC系統(tǒng)模型也符合。 從兩個(gè)模型之間的關(guān)系可以得出命題1的正確性結(jié)論。這意味著現(xiàn)實(shí)模型中會(huì)發(fā)生的所有的情況由時(shí)間間隔模型所包括，時(shí)間間隔模型是大于實(shí)際的模型。如果你不能用時(shí)間間隔模型找到一個(gè)反例，那你就可以證明真正的PLC模型的正確性;另一方面，如果我們找到一個(gè)反例，但無(wú)法確定PLC系統(tǒng)中是否真的存在此錯(cuò)誤，也就是說逆命題是錯(cuò)誤的。然后，需要手動(dòng)干預(yù)分析此反例，以確定它是否是一個(gè)偽誤差。 時(shí)間間隔建模策略可以得到一個(gè)抽象的PLC模型，基于對(duì)NuSMV的許多研究也可使用類似的時(shí)間間隔模型策略來(lái)建立PLC系統(tǒng)。然而“時(shí)間間隔模型”與真實(shí)模型有較大的偏差，從而需要加以改進(jìn)。偏差是指：“時(shí)間間隔模式”并不能反映PLC在并發(fā)系統(tǒng)的高速掃描特性和低速特性。也就是說，所有環(huán)境的變化應(yīng)由PLC快速的掃描，而時(shí)間間隔模型忽略了PLC的快速特性，這使得在外部環(huán)境的變化可能無(wú)法掃描。 為了解決上述問題，考慮到外部高速掃描和低速并發(fā)的物理特性，時(shí)間間隔建模策略應(yīng)通過加入的通知等待機(jī)制來(lái)改善。在時(shí)間間隔模型的基礎(chǔ)上，在發(fā)生傳輸后每個(gè)并發(fā)狀態(tài)機(jī)構(gòu)將被阻止并且等待。只有當(dāng)PLC控制器至少完全掃描一次后，通知等待機(jī)制將發(fā)送的信息給機(jī)構(gòu)移除阻止并繼續(xù)工作，然后傳輸完成。通過并發(fā)機(jī)構(gòu)的通知等待機(jī)制來(lái)完成傳輸?shù)倪^程，如圖2所示： 圖2：并發(fā)系統(tǒng)的通知等待機(jī)構(gòu) ?T0：傳輸開始，阻止并通知PLC控制器。 ?T1-TM：PLC完全掃描m次（m為至少一個(gè)）。 ?TM+1：并發(fā)機(jī)制從PLC中得到指令，傳輸完成。 這種機(jī)制確保每個(gè)并發(fā)機(jī)構(gòu)狀態(tài)的變化都能由PLC控制器至少一次掃描。 命題2：添加通知等候機(jī)制后，模型成為時(shí)間間隔模型的一個(gè)子集。同時(shí)，該模型也可以包括在現(xiàn)實(shí)模型中的所有情況，也就是說如果模型添加的通知等候機(jī)制符合屬性，真正的PLC系統(tǒng)模型也符合。 這類似于命題1證明與命題2，我們可以看出添加等待通知機(jī)制后的模式仍具有良好的性質(zhì)。正如前面提到的，抽象的系統(tǒng)模型有兩個(gè)要求：第一，要充分包含真正的系統(tǒng)模型接近真實(shí)系統(tǒng)；其次，第一命題證明的時(shí)間間隔模型包括了真實(shí)的系統(tǒng)，只要使用模型檢測(cè)工具證明這種抽象模型滿足一定屬性，那么原系統(tǒng)也將滿足這一點(diǎn)。但這種模式和實(shí)際的模型是不完全等價(jià)的，它應(yīng)該遠(yuǎn)遠(yuǎn)大于實(shí)際的模型。比較時(shí)間間隔模型，此模型與實(shí)際系統(tǒng)之間的距離將進(jìn)一步減小，大大降低了找出偽錯(cuò)誤的機(jī)會(huì)。 模型檢測(cè)工具將給出一個(gè)違反系統(tǒng)屬性的反例；在實(shí)際系統(tǒng)中很容易確定反例的真假。如果原系統(tǒng)中的錯(cuò)誤真的存在，那么我們就找出一個(gè)反例。否則，該錯(cuò)誤會(huì)由于抽象模型大于真實(shí)的系統(tǒng)，而成為一個(gè)偽誤差。因此，雖然這個(gè)時(shí)間間隔模型和原來(lái)的系統(tǒng)是不能完全等同的，但通過這個(gè)模型我們可以判斷系統(tǒng)是否符合一定的屬性，如果不是我們可以找到一個(gè)具體的反例（仍需要更多的研究以確定它是否是一個(gè)偽誤差）。 模型是不等于原系統(tǒng)的，主要是因?yàn)樵趯?shí)際系統(tǒng)中有許多因素難以模型，其中有一些可能會(huì)引起錯(cuò)誤。如果所有的因素都為藍(lán)本，將導(dǎo)致建立一個(gè)巨大的不可檢測(cè)或根本無(wú)法實(shí)現(xiàn)的模型。時(shí)間間隔模型是從真正的系統(tǒng)和他們的模型中抽象出來(lái)的，可大大減少狀態(tài)空間和時(shí)間復(fù)雜度。同時(shí)，添加通知等候機(jī)制，模型變得更接近真實(shí)系統(tǒng)，不僅降低了時(shí)間復(fù)雜度，同時(shí)減少了前面提到的偽錯(cuò)誤。 4.PLC模型檢測(cè) PLC被廣泛的使??用在許多領(lǐng)域，并有豐富的品種，這是一個(gè)很大的研究領(lǐng)域。任何PLC工作在包括不同的設(shè)備和人員的環(huán)境中，所以PLC系統(tǒng)是并發(fā)的。如果出現(xiàn)誤差，PLC系統(tǒng)很難在同一時(shí)間找到錯(cuò)誤的所在，其中主要是因?yàn)檫壿嬙O(shè)計(jì)錯(cuò)誤，但不會(huì)產(chǎn)生的計(jì)算誤差。所以我們專注于PLC程序的邏輯過程的檢測(cè)，這個(gè)邏輯可以完全通過為邏輯來(lái)描述。因此，為了簡(jiǎn)化PLC程序模型，專注于模型檢測(cè)，我們做如下設(shè)置： ?PLC邏輯控制程序，所有的控制變量只有兩個(gè)狀態(tài)0和1; ?PLC程序并發(fā)的環(huán)境中運(yùn)行。在這種情況下，PLC編程更可能會(huì)有一些不容易發(fā)現(xiàn)的錯(cuò)誤。 就上述特點(diǎn)，我們使用的模型檢測(cè)工具SPIN（我們的PLC檢查工具也識(shí)別NuSMV）對(duì)上述建立的模型進(jìn)行檢測(cè)。我們制定了一系列的轉(zhuǎn)變規(guī)則，用SPIN的輸入語(yǔ)言PROMELA建立上述模型中，系統(tǒng)屬性也需要被翻譯成PROMELA語(yǔ)句，SPIN將會(huì)把它們放在一起，然后進(jìn)行檢測(cè)。 PROMELA語(yǔ)言是一種C類語(yǔ)言，它們?cè)谡Z(yǔ)義上相似。所以我們將只舉幾個(gè)例子來(lái)展示翻譯的基本概念。要詳細(xì)了解PROMELA語(yǔ)言，請(qǐng)?jiān)L問www.spinroot.com 我們將介紹作為SPIK輸入的一個(gè)PROMELA文件的三個(gè)部分。 1）PLC控制器守則 PLC控制器由多個(gè)網(wǎng)絡(luò)組成的， PLC控制器代碼也從網(wǎng)絡(luò)中產(chǎn)生。當(dāng)然在這之前，應(yīng)先聲明所需的變量。每個(gè)網(wǎng)絡(luò)都有它的輸入端口和輸出端口，每個(gè)端口可以用一個(gè)布爾表達(dá)式。我們通過邏輯運(yùn)算來(lái)設(shè)計(jì)所有的輸入端口輸出端口的分配值,這是PLC網(wǎng)絡(luò)的翻譯方法。 下面是一個(gè)轉(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ā)機(jī)構(gòu)守則 我們認(rèn)為每個(gè)并發(fā)機(jī)構(gòu)是一個(gè)獨(dú)特的過程，不管是人的行為或設(shè)備。這些過程共享變量與PLC控制器的過程。這就確保了系統(tǒng)的并發(fā)性。 在本文的第二部分中，我們討論所有并發(fā)機(jī)構(gòu)的建模作為自動(dòng)機(jī)。自動(dòng)機(jī)的意思是從一個(gè)狀態(tài)轉(zhuǎn)變到另一個(gè)。我們使用的I端口形成的機(jī)構(gòu)狀態(tài)，使用goto語(yǔ)句作為轉(zhuǎn)變語(yǔ)句（就像匯編語(yǔ)言）。一個(gè)簡(jiǎ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的價(jià) goto StateB意味跳轉(zhuǎn)到狀態(tài)B*/ 3）屬性守則 屬性是PLC系統(tǒng)必須遵守的規(guī)則。我們使用LTL（線性時(shí)間邏輯）公式作為輸入方式。由于SPIK的機(jī)制，我們應(yīng)該編寫反屬性。SPIN將找出其屬性在什么情況下發(fā)生，此狀況則是一個(gè)反例。 我們不能直接寫LTL公式，但使用宏指令。首先，我們應(yīng)該用宏指令定義所有的LKL命題（例如定義p i5 == 0），然后我們用定義的命題，形成一個(gè)LTL公式。通過使用“SPIN-F”指令，SPIN可以自動(dòng)轉(zhuǎn)換LTL公式的PROMELA代碼。 4)通知等候機(jī)制 在建模的討論中，我們提出了添加通知等候機(jī)制。這種機(jī)制還需要在代碼中反映出來(lái)，具體做法是確定每個(gè)非PLC過程（PLC控制器除外）的位變量，將其作為一個(gè)信號(hào)。自動(dòng)機(jī)轉(zhuǎn)換到狀態(tài)標(biāo)簽時(shí)，設(shè)置的信號(hào)變量為0，直到下一個(gè)變量到來(lái)時(shí)變?yōu)?，否則繼續(xù)保持為0。PROMELA語(yǔ)法結(jié)果的特點(diǎn)，是此過程將保存起來(lái)。而在在PLC過程中則沒有這樣的限制，相反，PLC過程可以設(shè)置這些變量為1，從而確保每一動(dòng)作都必須經(jīng)過至少一個(gè)PLC的掃描完成。這就是所謂的等待通知機(jī)制。 遵循上述四個(gè)步驟，我們得到了一個(gè)完整的SPIN輸入文件代碼，然后我們就可以使用SPIK來(lái)檢測(cè)模型。對(duì)于SPIK模型檢測(cè)器的運(yùn)行步驟，請(qǐng)參閱SPIK的使用手冊(cè)（訪問www.spinroot.com）。SPIK能給出結(jié)果是否是所找的反例，而我們可以通過使用跟蹤文件的方法得出上述結(jié)論。 使用這種檢測(cè)機(jī)制，我們開發(fā)了一個(gè)能建模檢測(cè)PLC模型的工具。它有助于建立可視化模型和實(shí)施檢測(cè)，并且可以舉出一個(gè)簡(jiǎn)單的分析結(jié)果。當(dāng)然，發(fā)現(xiàn)反例則需要手動(dòng)檢測(cè)，以確保它是否是一個(gè)真正的反例，然而，有了跟蹤文件的幫助使這成了一個(gè)并不困難的任務(wù)。我們還成功的采用了一些PLC檢測(cè)（在下一節(jié)中所示）。教科書中發(fā)現(xiàn)的一個(gè)經(jīng)典例子可做反例。雖然發(fā)生反例的概率是很低的，但它確實(shí)存在，并且可能會(huì)產(chǎn)生嚴(yán)重的后果。文章中此工具也證明了理論的正確性和有效性。 5.運(yùn)行PLC檢查 通過檢測(cè)雙門通道模型，來(lái)展示PLC檢測(cè)的有效性。雙門通道是通過一個(gè)封閉的空間來(lái)防止與外界的接觸。 我們通過輸入梯形圖，并發(fā)機(jī)構(gòu)工具和定義屬性來(lái)執(zhí)行檢測(cè)。如圖3所示結(jié)果 圖3：模型檢測(cè)結(jié)果 正如我們所看到的：是一個(gè)錯(cuò)誤的結(jié)果，而且事實(shí)證明這是一個(gè)真正的通過手動(dòng)檢測(cè)跟蹤文件得出的反例，也就是說我們的PLC程序檢測(cè)這種機(jī)制是有效的。 6.結(jié)論 本文是研究的理論建模和檢測(cè)PLC系統(tǒng)的優(yōu)化方法。對(duì)PLC建模的要求進(jìn)行了分析，并同過時(shí)間間隔策略建立起并發(fā)系統(tǒng)。然后，我們證明了時(shí)間間隔模式的PLC系統(tǒng)中的一個(gè)超集，并加入通知等候機(jī)制來(lái)降低了模型。通知等候機(jī)制還確保在系統(tǒng)中的所有的變化可以被PLC控制器掃描，并且我們找到了系統(tǒng)誤差檢測(cè)的反例，最后給出使用SPIK檢測(cè)模型的方式。此外，引入了相應(yīng)的模型檢測(cè)工具PLC檢測(cè)器。在此階段，該機(jī)制仍然有許多缺陷，如定時(shí)器的處理，但它在解決空間探索問題上有很大而獨(dú)特的優(yōu)勢(shì)。我們?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