基于PLC建模的正式檢查方法

基于PLC建模的正式檢查方法摘文高可靠性是電氣控制設(shè)備的關(guān)鍵性能。PLC是結(jié)合了計算機技術(shù)、自動控制技術(shù)和通信技術(shù),被廣泛用于工業(yè)過程的自動化技術(shù)。在本文中,提出了一個有效的方法用于PLC系統(tǒng)的建模和驗證。為了確保PLC的高速特性,我們提出了一個“時間間隔模型”技術(shù)和“notice-waiting”。它可以降低狀態(tài)空間,也可以驗證一些復雜的PLC系統(tǒng)。同時,從PLC構(gòu)建模型轉(zhuǎn)換Promela語言來獲得建模和檢查工具PLC-Checker的PLC系統(tǒng)設(shè)計。盡管PLC這種邏輯錯誤發(fā)生的概率非常小,但是發(fā)生錯誤可能導致系統(tǒng)崩潰。接下來使用PLC-Checker檢查一個古典PLC的例子,這是一個反例。關(guān)鍵詞:模型檢查、PLC建模、PLC-Checker正式的方法介紹[1]PLC是一種自動控制裝置,可以從傳感器接收信息,計算設(shè)備或其它PLC邏輯輸入信號和輸出信號的邏輯處理。可以使用標準語言編寫控制算法,如梯形圖(LD)、結(jié)構(gòu)化的文本(ST)或指令表(IL)。[2]使用PLC技術(shù)的可編程語言來控制大規(guī)模集成電路已廣泛應用于工業(yè)。關(guān)于關(guān)鍵軟件的安全可以嚴重危害生命或財產(chǎn),驗證關(guān)鍵軟件的安全已經(jīng)成為不可或缺的步驟，所以需要保證軟件質(zhì)量。目前的PLC驗證方法仍是通過仿真和測試。然而,他們不能涵蓋所有可能的情況下,特殊的PLC的設(shè)計模型是否滿足需求。因此,模型檢測技術(shù)引入PLC的領(lǐng)域。提供給PLC設(shè)計重要的理論分析。[3]PLC模型檢測的主要步驟是建立PLC模式,如建立模型函數(shù)圖表。[4]關(guān)于PLC模型建立的時間屬性。它可以被建模的方法有時間自動機[5]或時間段建模方法[6]。[7]因此狀態(tài)空間模型與時間自動機相比將下降。不管怎樣選擇,最終都可以抽象模型。對于如何構(gòu)建一個好的PLC抽象模型檢查是最重要的問題。手動建模很容易引入許多錯誤,所以建立一個集成建模和測試工具是非常重要的,這是本文關(guān)注的問題之一。PLC控制程序在實時操作系統(tǒng)中運行(多任務或單一任務);本文主要是基于多任務調(diào)度PLC系統(tǒng)。第二節(jié)的文章介紹了PLC系統(tǒng)的建模方法。第三節(jié)給出了此模型的分析和改進,還有我們需要減少虛擬錯誤的概率。第四節(jié)是設(shè)計一個模型檢測工具PLC-Checker檢查建立模型,包括介紹了PLC程序轉(zhuǎn)換成主要的輸入語言Promela的代碼。最后，介紹了一個應用PLC-Checker檢查和一個關(guān)鍵問題的經(jīng)典例子。PLC建模有三個步驟的模型檢查:建模、屬性描述和驗證。最重要的是如何構(gòu)建系統(tǒng)模型。在系統(tǒng)中,PLC控制器不是孤立的,而是由驅(qū)動程序和人控制它的工作環(huán)境[8]。因此,這些因素也應該被建模。環(huán)境、人、PLC控制器是相互獨立和并發(fā)的邏輯。同時,模型檢查器轉(zhuǎn)換的輸入語言Promela側(cè)重于描述并發(fā),所以從這個觀點中,我們建立這些因素分成幾個并發(fā)進程轉(zhuǎn)換符合檢查,它也會準確地描述這個系統(tǒng)。為了描述方便,他們將被稱為并發(fā)實體。PLC控制器與并發(fā)交互實體通過符號表來表示。PLC系統(tǒng)的符號包括I(輸入端)、Q(輸出端口)和M(中間繼電器)。圖1是一個圖表的PLC系統(tǒng)模型。時間間隔建模策略:使用特定的并發(fā)實體的一些特定的狀態(tài)代表了并發(fā)中的實體狀態(tài),而不考慮系統(tǒng)時鐘。這可能忽視特定的時差,從而簡化了PLC模式。建模策略不添加系統(tǒng)時鐘屬性,不能完全符合最初的PLC模式。主要是由于加入系統(tǒng)時鐘會引起PLC系統(tǒng)模型太大,沒有模型檢查工具來處理如此大的模型。建模的起點狀態(tài)是不考慮PLC遷移時掃描的數(shù)量有經(jīng)驗。不管經(jīng)歷了多少掃描,他們都將包括在這個模型。換句話說,真正的模型將是建立模型的一個子集(時間間隔模型)。PLC的現(xiàn)實環(huán)境是復雜的,包括各種硬件和人為的行為。下面我們將分析不同類型的PLC并發(fā)實體環(huán)境。硬件實體硬件實體的PLC中,PLC控制系統(tǒng)主要是一些設(shè)備。這些設(shè)備的狀態(tài)可以輸入PLC控制器。雖然硬件都有自己的工作流程,但這個流程是由硬件需求決定的。因此,綁定硬件實體及其相關(guān)I和Q,。這個工作流程可以抽象為自動機。該自動機用于描述硬件的工作狀態(tài)。定義2.1.一個硬件實體是一個元組Env=<Ienv,Qenv,A>,Ienv是I的端口綁定與硬件實體，Qenv是Q的端口綁定的實體。A是自動機描述實體的工作流程，A是一個元組A=<s0,S,T>,當s0的初始狀態(tài)是A，S是特定集合T的轉(zhuǎn)移。硬件實體的狀態(tài)是I的一個子集符號,和標志每個狀態(tài)都映射到{真,假},I沒有出現(xiàn)的特定狀態(tài)可以是真或假(即:任意行動)。硬件實體的轉(zhuǎn)移與Q的子集直接表達符號表示所有問符號子集是真實的同時將驅(qū)動狀態(tài)之間的遷移。硬件實體的狀態(tài)轉(zhuǎn)換圖還需要從這個狀態(tài)轉(zhuǎn)換圖指定一個初始狀態(tài)。硬件實體的狀態(tài)轉(zhuǎn)換圖是基于分工的象征,不考慮時間和屬性。硬件實體狀態(tài)轉(zhuǎn)換圖實際上是一個忽略時間的抽象硬件實體,且需要抽象模擬硬件的參考。簡單輸出實體簡單的輸出實體只有綁定Q端口不使用I端口，這意味著簡單輸出實體沒有狀態(tài)轉(zhuǎn)換圖。簡單的輸出實體顯示了PLC的工作狀態(tài)的設(shè)備,像一個信號光。使用簡單的輸出實體是綁定的Q端口,PLC可使其進行邏輯設(shè)計。M端口Q端口I端口PLC控制器掃描和計算設(shè)置端口的值并發(fā)的實體簡單的輸出實體硬件實體M端口Q端口I端口PLC控制器掃描和計算設(shè)置端口的值并發(fā)的實體簡單的輸出實體硬件實體人類行為實體圖1所示PLC系統(tǒng)模型模型和實際模型并不完全相同的情況下,它應該是遠大于實際模型。與時間間隔模型相比,該模型進一步降低實際系統(tǒng)之間的距離,大大減少發(fā)生誤差的機會。模型檢測工具會給出一個破壞特性制度的反例;很容易手動確定反例在現(xiàn)實系統(tǒng)是真的還是假的。如果這一個反例是在原系統(tǒng)存在的錯誤。那么這個錯誤是因為在抽象模型中比真正的系統(tǒng)大,這是一個誤差。因此,雖然這個時間間隔模型和原系統(tǒng)不完全相同,但是通過這個模型,我們可以判斷一個系統(tǒng)滿足一定的特性,如果不是我們可以找到一個特定的反例(仍然需要更多的研究來確定是否有誤差)。模型并不等同與原系統(tǒng),主要是因為有許多因素難以模型在實際系統(tǒng),其中一些可能會導致錯誤。如果所有的因素進行建模,這將導致建立一個巨大的模型,無法檢查,或者根本無法實現(xiàn)。時間間隔模型抽象的關(guān)鍵因素從實際系統(tǒng)和模型,大大減少了狀態(tài)空間,降低時間復雜度。注意等待機制的存在,使添加的模型變得更接近實際系統(tǒng),不僅降低了時間復雜度,同時減少了之前提到的誤差。4所示。PLC模型檢查PLC廣泛應用在許多應用程序和很多設(shè)備中;這是一個大的研究領(lǐng)域。PLC任何的工作環(huán)境,都包括了不同的設(shè)備和人,所以PLC系統(tǒng)并發(fā)。同時,PLC系統(tǒng)很難找到如果有一些錯誤,主要是因為邏輯設(shè)計的錯誤,而不是計算誤差。我們專注于PLC程序邏輯過程的檢測,和這個邏輯可以完全由一些邏輯描述。因此,為了簡化PLC程序模型,集中在模型檢查,我們進行以下設(shè)置:PLC是一種邏輯控制程序,所有的控制變量只有0和1兩種狀態(tài);在并發(fā)環(huán)境中PLC程序運行。在這種情況下,PLC編程更可能有一些錯誤不容易找到。具上述特點,我們使用模型檢查工具轉(zhuǎn)換(我們的工具PLC檢測程序?qū)崿F(xiàn)NuSMV)對上述建立的模型檢查。我們做了一系列的轉(zhuǎn)換規(guī)則,建立上述模型轉(zhuǎn)換為輸入語言Promela,系統(tǒng)屬性也需要翻譯成Promela,轉(zhuǎn)換后將把它們放在一起,然后執(zhí)行檢測。PROMELA語言是一個C類語言,它們在語義上是相似的。所以我們只會給一些例子顯示翻譯的基本概念。看到PROMELA語言的細節(jié),請訪問。我們將介紹三個PROMELA文件作為輸入的一部分。PLC控制器的代碼PLC控制器是由多個網(wǎng)絡組成的。PLC控制器的代碼也是來自網(wǎng)絡。當然,在那之前,你應該申報所需要的變量。每個網(wǎng)絡都有其輸入端口和輸出端口,每個端口可以表明一個布爾表達式。我們分配輸出端口的值通過計算邏輯的輸入端口。這是PLC網(wǎng)絡的翻譯方法。這是一個老轉(zhuǎn)換網(wǎng)絡的例子:if::Exp(R)==1->Q=0;::else->if::Exp(S)==1->Q=1;::else->skip;fi;fi;/*Exp(S)是布爾表達式的港口Exp(R)是R的布爾表達式端口Q是輸出端口*/并發(fā)實體代碼我們認為每個并發(fā)實體一個獨特的過程,不管它是人類行為或設(shè)備。這些過程與PLC控制器進程共享變量。必須這樣做,以確保系統(tǒng)的并發(fā)性。在本文的第二部分,我們將討論所有的并發(fā)實體建模為一個自動機。自動機的意思是從一個狀態(tài)轉(zhuǎn)移到另一個地方。我們使用I端口形成實體的狀態(tài)。使用goto語句作為轉(zhuǎn)移(就像在匯編語言)。一個簡單的例子如所示:StateA:atomic{if::Q1->{IB,gotoStateB}::Q2->{IC,gotoStateC}fi;}/*StateA狀態(tài)的標簽Q1、Q2是轉(zhuǎn)移的條件IB是設(shè)置狀態(tài)值狀態(tài)B的值gotoStateB意味著跳到StateB*/代碼的特性特性是PLC系統(tǒng)必須遵守的規(guī)則。我們使用LTL(線性時間邏輯)公式的輸入格式。我們應該寫計數(shù)器屬性的機制。轉(zhuǎn)換會在一個我們特定的情況下發(fā)生,這應該是一個反例。我們不能直接寫LTL公式,要通過使用宏。首先我們應該在一個宏定義所有命題LTL(如#definepi5==0),然后使用LTL定義形成命題公式。SPIN可以自動轉(zhuǎn)換LTL公式PROMELA代碼通過使用“SPIN-f”指令(見更多的細節(jié)在SPIN手冊)。注意等待機制在建模討論,我們建議增加注意等待機制。這種機制也需要反映在代碼。具體實現(xiàn)是為每個non-PLC簽署一些變量的過程(所有流程PLC控制器除外)作為一個信號。自動機狀態(tài)轉(zhuǎn)移標簽時,信號變量設(shè)置為0,和下一個任務需要1繼續(xù)這個變量。PROMELA語法特性的結(jié)果,過程將掛起。PLC過程中沒有這樣的限制,相反,PLC過程可能將這些變量設(shè)置為1,從而確保每一個動作必須經(jīng)過至少一個PLC掃描完成。這就是所謂的注意等待機制。遵循以上四個步驟,我們得到一個完整的代碼的SPIN系統(tǒng)的輸入文件。然后我們可以使用SPIN檢查模型。SPIN模型檢查器的操作步驟,看SPIN的手冊(請訪問)。SPIN結(jié)果是否找到反例,我們可以使用上述理論分析SPIN的跟蹤文件。使用這種檢測機制,我們開發(fā)了一個工具檢查PLC檢測程序模型。它有助于構(gòu)建可視化模型和實施檢查,并可以給一個簡單的分析結(jié)果。當然,相反的例子,找到應用手動檢查以確定是否真正的反例。然而,在小徑的幫助文件,這不是一個非常困難的任務。我們還成功地實現(xiàn)一些檢查使用PLC檢測程序。在一個典型的范例,找到了一個反例。雖然反例的發(fā)生概率很低,但它確實發(fā)生,可能造成嚴重后果。這個工具也證明了本文理論的正確性和有效性。5。運行PLC檢測程序我們將介紹PLC的有效性檢查器通過檢查一輛雙門通道模型。雙門通道用于防止一個封閉的房間與外界聯(lián)系。通過輸入梯克和并發(fā)實體工具,在符合屬性的定義下,我們執(zhí)行檢查。圖3顯示了結(jié)果。我們可以看到,有一個錯誤的結(jié)果。它被證實是一個真正的反例通過檢查手動跟蹤文件。也就是說我們的機制是有效的檢查這樣的PLC程序。6。結(jié)論我們研究的理論建模和檢查PLC系統(tǒng)在正式的方法。PLC建模分析的要求,和并發(fā)實體的模型是建立在時間間隔的方法。然后我們證明的時間間隔模型一套超級的PLC系統(tǒng),通過添加注意等待機制和減少模型。這也保證了考試的所有更改可以掃描系統(tǒng)中PLC控制器。我們發(fā)現(xiàn)系統(tǒng)的誤差通過檢查系統(tǒng)的反例。最后,用SPIN的方式檢查模型。也對相應的模型檢查工具PLC-Checker介紹。在這個階段,機制仍然有許多缺陷,如處理定時器。但它在解決問題的探索有偉大的和獨特的優(yōu)點，表現(xiàn)我們?nèi)栽诜e極探索問題。引用[1]Pavlovic,R.PingerandM.Kollmann,“AutomatedFormalVerificationofPLCProgramsWritteninIL,”ConferenceonAutomatedDeduction(CADE),Bremen,July2007,pp.152-163.[2]M.B.YounisandG.Frey,“FormalizationofExistingPLCPrograms:ASurvey,”ProceedingsofCESA2003,Lille,2003.[3]N.Bauer,S.Engell,S.Lohmann,M.RemelheandO.Stursberg,“VerificationofPLCProgramGivenasSequentialFunctionCharts,”LectureNotesinComputerScience,Vol.3147,2004,pp.517-540.[4]S.R.Koo,P.H.SeongandS.D.Chaa,“SoftwareDesignSpecificationandAnalysisTechniquefortheSafetyCriticalSoftwarebasedonProgrammableLogicController(PLC),”ProceedingsoftheEighthIEEEInternationalSymposiumonHighAssuranceSystemsEngineering(HASE’04),Florida,March2004,pp.283-284.[5]A.MaderandH.Wupper,“TimedAutomatonModelsforSimpleProgrammableLogicControllers,”Proceedingsofthe11thEuromicroConferenceonReal-TimeSystems1999,York,June199