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

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