畢業(yè)論文外文翻譯-PLC的正式建模和檢查方法

學(xué)號(hào)：10463331常州大學(xué)畢業(yè)設(shè)計(jì)（論文）外文翻譯（2010屆）外文題目PLCModelingandCheckingBasedonFormalMethod譯文題目PLC的正式建模和檢查方法外文出處ScientificResearch學(xué)生學(xué)院懷德學(xué)院專業(yè)班級(jí)電氣101校內(nèi)指導(dǎo)教師專業(yè)技術(shù)職務(wù)講師二○一三年十一月常州大學(xué)本科生畢業(yè)設(shè)計(jì)（論文）外文翻譯目錄TOC\o"1-3"\h\u12726摘要 頁(yè)共8頁(yè)摘要高可靠性是電氣控制設(shè)備的關(guān)鍵性能。PLC結(jié)合計(jì)算機(jī)技術(shù)，自動(dòng)控制技術(shù)和通信技術(shù)，并廣泛應(yīng)用于工業(yè)過程的自動(dòng)化。一些需求復(fù)雜PLC的系統(tǒng)不能滿足傳統(tǒng)的驗(yàn)證方法。在本文中，提出了一個(gè)有效的PLC系統(tǒng)建模和驗(yàn)證方法。為了保證PLC的高速性能，我們提出了“時(shí)間間隔模式”和“通知等待”的技術(shù)。它可以減少狀態(tài)空間并可以驗(yàn)證一些復(fù)雜的PLC系統(tǒng)。同時(shí)，通過建立PLC模型到Promela語(yǔ)言轉(zhuǎn)換，用于建模和檢查的PLC系統(tǒng)被設(shè)計(jì)出來了——PLC檢查器工具。使用PLC檢查器核實(shí)一個(gè)經(jīng)典的PLC的例子，發(fā)現(xiàn)一個(gè)反例。雖然這一邏輯錯(cuò)誤發(fā)生的概率很小，這可能導(dǎo)致系統(tǒng)崩潰的致命的。關(guān)鍵詞：模型檢查，PLC建模，PLC檢查器，形式化方法1.介紹PLC自動(dòng)控制裝置可以接受從傳感器傳來的信息，計(jì)算裝置或其它PLC邏輯輸入信號(hào)，輸出邏輯信號(hào)處理。該控制算法可以用標(biāo)準(zhǔn)的語(yǔ)言，如梯形圖（LD），結(jié)構(gòu)化文本（ST）或指令表（IL）[1]。PLC技術(shù)使用可編程語(yǔ)言來控制大規(guī)模集成電路被廣泛應(yīng)用在工業(yè)[2]。由于安全關(guān)鍵軟件會(huì)導(dǎo)致生命或財(cái)產(chǎn)的嚴(yán)重?fù)p害，安全關(guān)鍵軟件驗(yàn)證已成為保證軟件質(zhì)量一個(gè)不可或缺的步驟需要。目前驗(yàn)證PLC的方法還需要通過仿真和測(cè)試。然而，它們不能覆蓋所有可能的情況，特別是滿足需求的PLC的設(shè)計(jì)模型。因此，模型檢測(cè)技術(shù)被引入到PLC領(lǐng)域。PLC設(shè)計(jì)成為重要的理論分析。PLC模型檢查的主要步驟是建立PLC模型，例如建立功能圖模型[3]。PLC模型側(cè)重于建立的時(shí)間屬性[4]。它可以通過同步自動(dòng)操作[5]或時(shí)間建模方法[6]建模。因此，該模型的狀態(tài)空間會(huì)隨著的同步自動(dòng)操作而下降。無論哪種方式選擇，最終都可以給出一個(gè)抽象的模型[7]。對(duì)檢查來說，如何建立一個(gè)良好的PLC抽象模型是一個(gè)最重要的問題。用手動(dòng)建模很容易引入很多錯(cuò)誤，所以一個(gè)集成的建模和測(cè)試工具的建立是非常重要的，這是本文關(guān)注的問題之一。PLC控制程序在實(shí)時(shí)操作系統(tǒng)運(yùn)行中有多任務(wù)或單任務(wù)之分；本文主要基于PLC系統(tǒng)的多任務(wù)調(diào)度。文章的第2節(jié)介紹PLC系統(tǒng)建模方法。文章的第3節(jié)給出了該模型分析和改進(jìn)以及我們可以減少偽錯(cuò)誤的可能。文章第4節(jié)設(shè)計(jì)的模型檢測(cè)工具的PLC檢查器檢查所建立的模型，包括介紹PLC程序轉(zhuǎn)換成SPIN的Promela代碼輸入語(yǔ)言的方法。最后是核實(shí)PLC的一個(gè)經(jīng)典例子和PLC檢查器發(fā)現(xiàn)的一個(gè)關(guān)鍵的反例。2.PLC建模建模的步驟有三個(gè)：模型、屬性描述和驗(yàn)證。最重要的是如何構(gòu)建系統(tǒng)模型。在系統(tǒng)中，PLC控制器不是孤立的，而是有其工作環(huán)境、驅(qū)動(dòng)和本性的相互作用[8]。因此，這些因素也應(yīng)該被建模。環(huán)境、本性和PLC控制器是獨(dú)立和在邏輯彼此同時(shí)發(fā)生。同時(shí)，模型檢查器SPIN的輸入語(yǔ)言Promela集中描述同時(shí)發(fā)生，所以從這一思想出發(fā)，建立了這些多個(gè)并發(fā)進(jìn)程因素來適應(yīng)SPIN的檢查，也將準(zhǔn)確地描述系統(tǒng)。為了描述方便，它們將被稱為并發(fā)實(shí)體。PLC控制器與并發(fā)實(shí)體通過符號(hào)圖像表相互作用。PLC系統(tǒng)的符號(hào)包括I（輸入端口），Q（輸出端口），和M（中間繼電器）。圖1為PLC系統(tǒng)模型。圖1PLC系統(tǒng)模型時(shí)間間隔的建模策略：使用特定的并發(fā)實(shí)體的位狀態(tài)的標(biāo)志代表并發(fā)實(shí)體的狀態(tài)，而不考慮系統(tǒng)時(shí)鐘。這可以忽視狀態(tài)的時(shí)間差，從而簡(jiǎn)化了PLC模型。建模的策略，沒有增加的系統(tǒng)時(shí)鐘性能，不完全符合原PLC的模型。這主要是由于加入的系統(tǒng)時(shí)鐘將使PLC系統(tǒng)模型變得太大，沒有模型檢測(cè)工具來處理如此大規(guī)模的模型。像這樣狀態(tài)的建模出發(fā)點(diǎn)轉(zhuǎn)移經(jīng)歷時(shí)是不考慮PLC次數(shù)掃描的。不管有多少次的掃描經(jīng)歷，它們都將包括在這個(gè)模型中。換句話說，實(shí)體模型是所建模型的一個(gè)子集（時(shí)間間隔模型）。真正的PLC環(huán)境是復(fù)雜的，包括各種硬件和人類行為。以下我們將提供不同種類PLC環(huán)境下的并行實(shí)體分析。1）硬件實(shí)體PLC系統(tǒng)的硬件實(shí)體主要是一些PLC控制的設(shè)備。這些設(shè)備的狀態(tài)可以是PLC控制器的輸入。因此，硬件實(shí)體和相關(guān)的I和Q的結(jié)合，而硬件有自己的工作流程，工作流程是由硬件要求決定。這個(gè)工作流程可以抽象成自動(dòng)機(jī)。該自動(dòng)機(jī)是用來描述硬件的工作狀態(tài)。這個(gè)工作流程可以抽象成自動(dòng)機(jī)。該自動(dòng)機(jī)是用來描述硬件的工作狀態(tài)。定義2.1硬件實(shí)體的一個(gè)數(shù)組是Env=<Ienv,Qenv,A>，Ienv的輸入口和硬件實(shí)體是連接的，Qenv的輸出口和實(shí)體連接。A是自動(dòng)機(jī)描述實(shí)體的工作流程，A的數(shù)組A=<s0,S,T>，s0是初始狀態(tài)的A，S是狀態(tài)的集合，T是傳輸?shù)募稀Ｓ布?shí)體的狀態(tài)是符號(hào)I的子集，每個(gè)狀態(tài)I信號(hào)都會(huì)映射到{真，假}，I的符號(hào)沒有在狀態(tài)出現(xiàn)可以是真也可以是假（即：獨(dú)斷獨(dú)行）。用符號(hào)Q的子集直接表達(dá)硬件實(shí)體的轉(zhuǎn)移，所有在子集中的符號(hào)Q在同一時(shí)間的狀態(tài)之間的遷移是真的。硬件實(shí)體的狀態(tài)轉(zhuǎn)換圖還需要指定一個(gè)初始狀態(tài)，轉(zhuǎn)換圖起始于這種狀態(tài)。硬件實(shí)體的狀態(tài)轉(zhuǎn)換圖是基于不同部門的符號(hào)I并且時(shí)間性質(zhì)不作考慮。硬件實(shí)體的狀態(tài)轉(zhuǎn)換圖實(shí)際上是忽略了時(shí)間的硬件實(shí)體抽象，這種抽象的模擬需要用硬件做參考。2）簡(jiǎn)單的輸出實(shí)體簡(jiǎn)單的輸出實(shí)體只與Q端口綁定而不使用I端口，這意味著簡(jiǎn)單輸出實(shí)體沒有狀態(tài)轉(zhuǎn)換圖。簡(jiǎn)單的輸出是實(shí)體顯示PLC的工作狀態(tài)的設(shè)備，如信號(hào)燈。簡(jiǎn)單的輸出實(shí)體用法是和Q端口綁定，PLC可實(shí)現(xiàn)其邏輯設(shè)計(jì)。3）人類行為實(shí)體定義2.2人類的行為實(shí)體的一個(gè)數(shù)組是Env=<Ienv,A>，Ienv的輸入口和硬件實(shí)體是連接的，Qenv的輸出口和實(shí)體連接。A是自動(dòng)機(jī)描述實(shí)體的工作流程，A的數(shù)組A=<s0,S,T>，s0是初始狀態(tài)的A，S是狀態(tài)的集合，T是傳輸?shù)募?。人類行為?shí)體與硬件實(shí)體類似；它們有相同的狀態(tài)定義。模擬人的行為是很難的，特別是一些涉及個(gè)人的PLC設(shè)計(jì)。針對(duì)這些困難，人類行為建模需要一個(gè)重復(fù)的過程：首先，使用模型驗(yàn)證建立一個(gè)簡(jiǎn)單的行為模型；其次，如果沒能找到一個(gè)反例，建立一個(gè)更復(fù)雜的模型并驗(yàn)證，直到找到一個(gè)反例或難以更復(fù)雜；最后，如果沒有找到一個(gè)有意義的反例，就生成一個(gè)完全隨機(jī)的個(gè)人行為模型（即：人類的行為是一個(gè)完整的圖形的所有傳輸是真的）來驗(yàn)證。然而，完全隨機(jī)的行為驗(yàn)證將導(dǎo)致狀態(tài)空間急劇增加，因此如何選擇一個(gè)合適的人類行為模型在建模中是最有難度的。如果個(gè)人的輸入是相對(duì)簡(jiǎn)單的，我們可以用完全隨機(jī)的行為來建模，否則，你需要認(rèn)真考慮建立一個(gè)合理的人類行為模型。我們將建立高于PLC環(huán)境和人類行為的模型，然后我們還將建立PLC控制器的模型。PLC控制器在打開時(shí)將在一個(gè)循環(huán)過程。?PLC從I端口讀取所有的輸入。?PLC計(jì)算所有的邏輯單元。?PLC設(shè)置所有的Q端口。PLC的基本單元過程稱為網(wǎng)絡(luò)。所有的網(wǎng)絡(luò)操作在設(shè)計(jì)時(shí)的根據(jù)是數(shù)字集合。PLC控制器的基本邏輯操作網(wǎng)絡(luò)包括：S觸發(fā)器，R觸發(fā)器，SR置“1”置“0”觸發(fā)器，EQ觸發(fā)器，RS置“0”置“1”觸發(fā)器，POS上升邊緣檢測(cè)器，NEG下降邊緣檢測(cè)器等等。基本的邏輯操作網(wǎng)絡(luò)建模，我們使用了直接映射策略，即：網(wǎng)絡(luò)行為的PLC控制器模型和網(wǎng)絡(luò)的邏輯的行為是完全等價(jià)的。其中S觸發(fā)器，R觸發(fā)器，SR觸發(fā)器，EQ觸發(fā)器，RS觸發(fā)器可以直接使用布爾表達(dá)式（Booleanexpressions）來映射到它們的行為。3.PLC模型的分析和改進(jìn)前一部分介紹了PLC系統(tǒng)的建模，根據(jù)這一策略；我們可以抽象PLC系統(tǒng)為模型檢驗(yàn)的形式化模型。因此,該模型將直接決定模型檢測(cè)結(jié)果的可信度。如果模型沒有完全覆蓋原系統(tǒng)（我們稱之為比原始系統(tǒng)小），則有可能導(dǎo)致一些沒有被檢測(cè)到錯(cuò)誤；在真實(shí)系統(tǒng)中模型可以完全被覆蓋，但它包含著原始系統(tǒng)不存在的狀態(tài)（我們稱之為比原始系統(tǒng)大），這可能會(huì)引入一些實(shí)際的系統(tǒng)中不存在的錯(cuò)誤。在這里稱之為偽錯(cuò)誤。所以有兩個(gè)建模策略的要求。首先，為了找到系統(tǒng)中所有的錯(cuò)誤，我們將建立一個(gè)足以囊括所有原始系統(tǒng)狀態(tài)的模型；其次，要求模型是盡可能的接近真實(shí)系統(tǒng)。這不僅可以減少狀態(tài)空間，而且提高效率?；诖艘?，我們將提供有關(guān)的時(shí)間間隔模型的分析。命題1如果時(shí)間間隔模型符合該屬性，也符合真實(shí)的PLC系統(tǒng)模型。命題1的正確性可以從兩個(gè)模型之間的關(guān)系得出結(jié)論。這意味著所有的情況下，實(shí)體模型將發(fā)生的事包括時(shí)間間隔模型，時(shí)間間隔模型比實(shí)體模型大。如果你不能通過使用一個(gè)時(shí)間間隔模型找到一個(gè)相反的例子，可以證明真正PLC模型的正確性；另一方面，如果我們找到了一個(gè)相反的例子，我們就不能確定是否是真實(shí)PLC系統(tǒng)的錯(cuò)誤。也就是說命題1的逆命題是錯(cuò)誤的。然后需要人工干預(yù)來分析反例，以確定它是否是一個(gè)偽錯(cuò)誤。時(shí)間間隔建模策略可以得到一個(gè)抽象的PLC模型，許多基于NuSMV的研究也使用類似的時(shí)間間隔模型策略到PLC系統(tǒng)的模型。然而，“時(shí)間間隔模型”與實(shí)體模型有較大的偏差，需要改進(jìn)。偏差就是：“時(shí)間間隔模型”不能反映PLC的高速掃描特性和并發(fā)實(shí)體的低速特性。環(huán)境中的所有變化應(yīng)該被PLC高速掃描，但時(shí)間間隔模型忽略了PLC的高速特性，這使得在外部環(huán)境的變化可能沒被掃描。為了解決上述問題，考慮到外部高速掃描和低速并行的物理特性，時(shí)間間隔的建模策略應(yīng)加注意通知等待機(jī)制的改進(jìn)。在時(shí)間間隔模型的基礎(chǔ)上，每一個(gè)并發(fā)狀態(tài)的實(shí)體必須阻止，等待后才發(fā)生轉(zhuǎn)移。只有當(dāng)PLC控制器至少完成一次掃描，通知等待機(jī)制將發(fā)送至并發(fā)實(shí)體移除障礙，然后繼續(xù)工作。然后，轉(zhuǎn)移完成。并發(fā)實(shí)體工作的通知等待機(jī)制轉(zhuǎn)移過程如圖2所示：圖2并發(fā)實(shí)體通知等待機(jī)制?t0：轉(zhuǎn)移開始，塊和通知PLC控制器。?t1~tm：PLC完全掃描m次（m至少是一次）。?tm+1：并發(fā)實(shí)體從PLC得到通知，轉(zhuǎn)移完成。這種機(jī)制確保并發(fā)實(shí)體每一狀態(tài)的變化可以被PLC控制器至少掃描一次。命題2添加通知等待機(jī)制后，模型成為時(shí)間間隔模型的一個(gè)子集。同時(shí)，該模型還可以包括實(shí)體模型的整個(gè)情況。也就是說，如果一個(gè)模型添加的通知等待機(jī)制符合這種特性，真正的PLC系統(tǒng)模型也符合。命題2的證明和命題1類似。由命題2我們可以看到，添加了通知等待機(jī)制的模型仍具有良好的性質(zhì)。正如前面提到的，一個(gè)抽象的系統(tǒng)模型有兩個(gè)要求：首先，充分包含真實(shí)的系統(tǒng)，其次是模型盡可能接近真實(shí)的系統(tǒng)。第一個(gè)命題證明的時(shí)間間隔模型包括真實(shí)的系統(tǒng)，只要使用模型檢測(cè)工具來證明該抽象模型滿足一定的特性，那么系統(tǒng)的本質(zhì)也將滿足這一點(diǎn)。但該模型和實(shí)體模型并不完全相等，應(yīng)該遠(yuǎn)遠(yuǎn)大于實(shí)體模型。比較時(shí)間間隔模型，該模型進(jìn)一步降低真實(shí)系統(tǒng)之間的距離，進(jìn)而大大減少找到偽錯(cuò)誤的機(jī)會(huì)。模型檢查工具會(huì)給出一個(gè)反例違反的系統(tǒng)性能；它易于手動(dòng)確定反例在真實(shí)的系統(tǒng)中是不是真的。如果原系統(tǒng)中的錯(cuò)誤真的存在，那么我們找到一個(gè)反例。否則，這個(gè)錯(cuò)誤是因?yàn)槌橄竽Ｐ痛笥谡鎸?shí)的系統(tǒng)，這是一個(gè)偽錯(cuò)誤。因此，雖然這個(gè)時(shí)間間隔模型與原系統(tǒng)不是完全等同的，但通過這種模型，我們可以斷定一個(gè)系統(tǒng)滿足一定的特性，如果沒有，我們可以找到一個(gè)特定的反例（還需要更多的研究來確定它是否是一個(gè)偽錯(cuò)誤）。模型不等于與原系統(tǒng)，主要是因?yàn)橛性S多因素在真實(shí)的系統(tǒng)中難以模仿，其中的一些可能會(huì)加大錯(cuò)誤。如果所有的因素都進(jìn)行建模，這將導(dǎo)致建立起一個(gè)巨大的模型以至于無法檢查，或根本無法實(shí)現(xiàn)的。時(shí)間間隔模型抽象的關(guān)鍵因素是真實(shí)的系統(tǒng)和模仿他們，這大大減少了狀態(tài)空間，并降低了時(shí)間復(fù)雜度。同時(shí)，通過添加通知等待機(jī)制，模型變得更接近真實(shí)的系統(tǒng)，不僅降低了時(shí)間復(fù)雜度，同時(shí)減少之前提到的偽錯(cuò)誤。4.PLC模型檢查PLC被廣泛運(yùn)用于許多應(yīng)用中，并且有許多設(shè)備；這是研究的一個(gè)大型領(lǐng)域。任何PLC的工作環(huán)境包括不同的設(shè)備和人員，所以PLC系統(tǒng)是并行。在同一時(shí)間，很難找到是否有一些錯(cuò)誤，這主要是因?yàn)樵谶壿嬙O(shè)計(jì)錯(cuò)誤，并不是計(jì)算錯(cuò)誤。我們專注于PLC程序的邏輯過程的檢測(cè)，這種邏輯可以通過位邏輯完全描述。因此，為了簡(jiǎn)化PLC程序模型，專注于模型檢查，我們進(jìn)行如下設(shè)置：?PLC是一種邏輯控制程序，所有的控制變量只有0和1兩種狀態(tài)；?在并發(fā)環(huán)境中運(yùn)行PLC程序。在這種情況下，PLC編程更可能產(chǎn)生一些錯(cuò)誤不容易找到。在上述特征方面，我們利用模型檢測(cè)工具SPIN（我們的PLC檢查器工具實(shí)現(xiàn)了NuSMV）對(duì)已建立的上述模型進(jìn)行檢測(cè)。我們做了一系列的轉(zhuǎn)換規(guī)則，建立了上述模型轉(zhuǎn)化為SPIN的輸入語(yǔ)言Promela，系統(tǒng)屬性也需要被翻譯成Promela語(yǔ)言，SPIN將它們放在一起，然后進(jìn)行檢測(cè)。PROMELA語(yǔ)言是C類的語(yǔ)言，它們?cè)谡Z(yǔ)義相似。所以我們只會(huì)給一些例子說明翻譯的基本概念?？碢ROMELA語(yǔ)言的詳情，請(qǐng)瀏覽。我們將介紹PROMELA文件的三個(gè)部分作為SPIN的輸入。1）PLC控制器代碼PLC控制器由多個(gè)網(wǎng)絡(luò)組成。PLC控制器代碼也從網(wǎng)絡(luò)上產(chǎn)生的。當(dāng)然，在這之前，你需要聲明所需的變量。每個(gè)網(wǎng)絡(luò)都有其輸入端口和輸出端口，每個(gè)端口可以表示的布爾表達(dá)式（Booleanexpression）。我們通過對(duì)所有輸入端口的邏輯運(yùn)算指定輸出端口的值。這是PLC網(wǎng)絡(luò)的翻譯方法。這里是SR網(wǎng)絡(luò)的轉(zhuǎn)換例子：if::Exp(R)==1->Q=0;::else->if::Exp(S)==1->Q=1;::else->skip;fi;fi;/*Exp(S)布爾表達(dá)式表達(dá)式的S端口Exp(R)布爾表達(dá)式表達(dá)式的R端口Q輸出端口*/2）并發(fā)實(shí)體編碼我們考慮每個(gè)并發(fā)實(shí)體的一種獨(dú)特過程，無論是人類的行為還是設(shè)備。這些進(jìn)程與PLC控制器進(jìn)程共享變量。這是必須的以確保該系統(tǒng)的并發(fā)性。在本文的第二部分，我們討論了所有的并發(fā)實(shí)體都作為自動(dòng)機(jī)進(jìn)行建模。自動(dòng)機(jī)的意思是從一個(gè)狀態(tài)轉(zhuǎn)移到另一個(gè)狀態(tài)。我們使用I端口以形成實(shí)體的狀態(tài)。使用goto語(yǔ)句作為傳輸（就像匯編語(yǔ)言一樣）。一個(gè)簡(jiǎn)單的例子是顯示在下面：StateA:atomic{if::Q1->{IB,gotoStateB}::Q2->{IC,gotoStateC}fi;}/*StateA是StateA的標(biāo)簽Q1,Q2是轉(zhuǎn)移條件IB是將狀態(tài)值設(shè)置到狀態(tài)B的值gotoStateB意味著跳轉(zhuǎn)至stateB*/3）編碼的屬性屬性是PLC系統(tǒng)必須遵守的規(guī)則。我們使用的LTL（線性時(shí)間邏輯）公式作為輸入格式。我們應(yīng)該寫反屬性因?yàn)橛蠸PIN機(jī)制。SPIN會(huì)發(fā)現(xiàn)一個(gè)我們屬性發(fā)生的情況，這應(yīng)該是一個(gè)反例。我們不能直接寫LTL公式，但使用宏。首先我們應(yīng)該在宏中LTL定義所有的命題(like#definepi5==0)，然后我們使用命題定義，形成一個(gè)LTL公式。SPIN可以通過使用“SPIN–F”指令PROMELA代碼自動(dòng)轉(zhuǎn)換為L(zhǎng)TL公式（更多詳情見SPIN手動(dòng)操作）。4）通知等待機(jī)制在建模的探討中，我們提出了添加通知等待機(jī)制。這種機(jī)制也需要在代碼中體現(xiàn)。具體的實(shí)施是為每個(gè)非PLC過程簽署一個(gè)位變量（除了PLC控制器的所有進(jìn)程）作為一種信號(hào)。當(dāng)自動(dòng)機(jī)轉(zhuǎn)移到狀態(tài)標(biāo)簽，信號(hào)變量被設(shè)置為0，接下來的任務(wù)需要此變量為1以繼續(xù)。由于PROMELA語(yǔ)法特征的結(jié)果，這個(gè)過程將掛起。PLC過程中沒有這樣的限制，相反，PLC程序可以設(shè)置這些變量為1，從而確保每一個(gè)動(dòng)作都必須經(jīng)過完成至少一次PLC掃描。這就是所謂的通知等待機(jī)制。按照以上四步；我們得到了一個(gè)完整的SPIN輸入文件的系統(tǒng)代碼。然后我們可以使用SPIN檢查模型。操作SPIN模型檢查器的步驟，請(qǐng)查看SPIN手動(dòng)操作（訪問）。SPIN給出的反例是否找到的結(jié)果，我們可以分析使用前面提到的理論來追蹤SPIN給出的文件。利用該檢測(cè)機(jī)制，我們開發(fā)了一種用于模型檢查的PLC檢測(cè)器。它有助于建立視覺模型和執(zhí)行情況檢查，并可以給一個(gè)簡(jiǎn)單的分析的結(jié)果。當(dāng)然，反例發(fā)現(xiàn)后應(yīng)再用手動(dòng)檢查以確定它是否是一個(gè)真正的反例。然而，在跟蹤文件的幫助下，這也不是一個(gè)非常困難的任務(wù)。我們還成功地實(shí)現(xiàn)了利用PLC檢測(cè)器一些檢查（在下一節(jié)中所示）。在經(jīng)典范例中找到了一個(gè)反例。雖然反例發(fā)生的概率是非常低的，但它確實(shí)發(fā)生了，并且產(chǎn)生嚴(yán)重的后果。這個(gè)工具也證明了本文理論的正確性和有效性。5.運(yùn)行PLC檢查我們將通過檢查兩門通道模型顯示PLC檢測(cè)器的效力。兩門通道用于防止封閉的房間里和外面的世界接觸。通過輸入梯圖（響度平衡）和并發(fā)實(shí)體成為工具，同時(shí)定義屬性，我們執(zhí)行檢查。圖3顯示結(jié)果。圖3模型檢查結(jié)果我們可以看到，有一個(gè)錯(cuò)誤的結(jié)果。這證明檢查手動(dòng)跟蹤文件是一個(gè)真正的反例。這也就是說我們這種檢查PLC程序的機(jī)制是有效。6.結(jié)論我們?cè)诖宋闹醒芯苛嗽赑LC系統(tǒng)的正式建模和檢測(cè)方法理論。我們對(duì)PLC建模的要求進(jìn)行分析，并發(fā)實(shí)體的模型通過時(shí)間間隔策略已經(jīng)建立。然后，我們證明了時(shí)間間隔模型的一個(gè)超集PLC系統(tǒng)，并通過添加通知等待機(jī)制降低模型。它還確保系統(tǒng)中所有的變化都可以通過PLC控制器掃描。我們通過檢查系統(tǒng)的反例發(fā)現(xiàn)系統(tǒng)錯(cuò)誤。最后，使用SPIN驗(yàn)證給出的模型。還介紹了相應(yīng)模型的檢測(cè)工具PLC檢查器。在此階段，該機(jī)制仍然有許多缺陷，如定時(shí)器的處理。但它在解決狀態(tài)探索問題方面有著良好的和獨(dú)特的優(yōu)勢(shì)。我們?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),”ProceedingsoftheEighthIEEEInternationalSymposiumonHighAssu