外文文獻翻譯-基于形式化方法的PLC建模和檢測【中文6440字】 【中英文WORD】,中文6440字,中英文WORD,外文文獻翻譯-基于形式化方法的PLC建模和檢測【中文6440字】,【中英文WORD】,外文,文獻,翻譯,基于,形式化,方法,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é)給出了分析和改進這種模式的方法，因為我們需要降低偽錯誤的概率。第4節(jié)設(shè)計PLC檢測模型驗證工具，檢查所建立的模型，包括引進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é)合，并且擁有自己的工作流程，該工作流程是由所需硬件自身決定。這個工作流程可以抽象認為成是自動機，此自動機通常用來來描述的硬件的工作狀態(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)變直接表達為符號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端口進行邏輯設(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ù)雜的模型并進行驗證，直到找到一個反例或幾乎不能再復(fù)雜為止；最后，如果前面沒有找到有意義的反例，則生成一個完全隨機的人的行為模式（即：所有轉(zhuǎn)讓是真實的人類行為是一個完整的圖形）來核查。然而，完全隨機行為的核查將導(dǎo)致狀態(tài)空間的顯著增加，因此如何選擇一個合適的人類行為模式在建模中是存在很大難度的。如果人的輸入比較簡單，我們可以使用完全隨機的行為建模，否則，你需要認真考慮建立一個理性的人的行為模式。 上面我們建立了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ā)器可以直接使用布爾表達式進行觸發(fā)。 3.PLC模型的分析與改進 上一節(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)。然而“時間間隔模型”與真實模型有較大的偏差，從而需要加以改進。偏差是指：“時間間隔模式”并不能反映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)該遠遠大于實際的模型。比較時間間隔模型，此模型與實際系統(tǒng)之間的距離將進一步減小，大大降低了找出偽錯誤的機會。 模型檢測工具將給出一個違反系統(tǒng)屬性的反例；在實際系統(tǒng)中很容易確定反例的真假。如果原系統(tǒng)中的錯誤真的存在，那么我們就找出一個反例。否則，該錯誤會由于抽象模型大于真實的系統(tǒng)，而成為一個偽誤差。因此，雖然這個時間間隔模型和原來的系統(tǒng)是不能完全等同的，但通過這個模型我們可以判斷系統(tǒng)是否符合一定的屬性，如果不是我們可以找到一個具體的反例（仍需要更多的研究以確定它是否是一個偽誤差）。 模型是不等于原系統(tǒng)的，主要是因為在實際系統(tǒng)中有許多因素難以模型，其中有一些可能會引起錯誤。如果所有的因素都為藍本，將導(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）對上述建立的模型進行檢測。我們制定了一系列的轉(zhuǎn)變規(guī)則，用SPIN的輸入語言PROMELA建立上述模型中，系統(tǒng)屬性也需要被翻譯成PROMELA語句，SPIN將會把它們放在一起，然后進行檢測。 PROMELA語言是一種C類語言，它們在語義上相似。所以我們將只舉幾個例子來展示翻譯的基本概念。要詳細了解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ò)都有它的輸入端口和輸出端口，每個端口可以用一個布爾表達式。我們通過邏輯運算來設(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端口的布爾表達式 Exp（R）是R端口的布爾表達式 Q是輸出端口*/ 2）并發(fā)機構(gòu)守則 我們認為每個并發(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è)置的到達狀態(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建模的要求進行了分析，并同過時間間隔策略建立起并發(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)教師簽字： 年 月 日