高可靠性是電氣控制設備性能的關鍵。 PLC結合了計算機技術、自動控制技術和通訊技術，廣泛應用于工業(yè)過程的自動化。 傳統(tǒng)的驗證方法無法滿足復雜PLC系統(tǒng)的一些要求。 在這個本文提出了一種高效的PLC系統(tǒng)建模和驗證方法。 為了保證PLC的高速性能，我們提出了“時間間隔模型”和“通知等待”技術。 它可以減少狀態(tài)空間并使驗證一些復雜的 PLC 系統(tǒng)成為可能。 此外，還獲得了從建立的PLC模型到Promela語言的轉換，并設計了一個用于PLC系統(tǒng)建模和檢查的工具PLC-Checker。 使用PLC-Checker 檢查一個經典的 PLC 例子，找到一個反例。 雖然這種邏輯錯誤發(fā)生的概率很小，但可能會導致系統(tǒng)死機。

一、簡介

PLC是一種自動控制設備，可以接收來自傳感器、計算設備或其他PLC的信息邏輯輸入信號，輸出處理后的邏輯信號。

控制算法可以使用標準語言編寫，例如梯形圖 (LD)、結構化文本(ST) 或指令列表 (IL) [1]。

PLC使用可編程語言的技術控制大規(guī)模集成電路已廣泛應用工業(yè)[2]。由于安全關鍵軟件可以對生命或財產造成嚴重損害，核實安全關鍵軟件已成為不可或缺的一步保證軟件質量的必要條件。目前的驗證PLC的方法仍然停留在仿真和測試上。但是，它們并不能涵蓋所有可能的情況，尤其是 PLC 的設計模型是否滿足需求。因此，引入了模型檢查技術進入PLC領域。對PLC進行理論分析設計變得很重要。

PLC模型檢查的首要步驟是建立PLC模型，比如建立一個模型來自功能圖 [3]。 PLC模型側重于建立時間屬性[4]?？梢越Ｍㄟ^時間自動機[5]的方法或時間段建模方法[6]。因此模型的狀態(tài)空間將是與定時自動機相比減少了。無論哪種方式選擇，最終可以給出一個抽象模型[7]。如何建立一個好的PLC抽象模型是檢驗的重中之重。作為手動建模容易引入很多錯誤，所以建立一個集成的建模和測試工具非常重要，這是本文關注的問題之一。

PLC控制程序在實時操作系統(tǒng)中運行（多任務或單任務）；本文主要基于多任務調度PLC系統(tǒng)。第 2 節(jié)文章介紹了建模方法PLC系統(tǒng)。第 3 節(jié)給出了該模型的分析和改進，因為我們需要降低偽錯誤。第四節(jié)設計了一個模型檢查工具PLC-Checker 檢查已建立的模型，包括介紹PLC程序轉換成SPIN的方法輸入語言 Promela 代碼。最后，一個經典的 PLC示例用于檢查和關鍵的計算機示例由 PLC-Checker 發(fā)現。

2.PLC建模*

這項工作由 NSFC 60973049、60635020 和 TNList 資助跨學科基礎。模型檢查分為三個步驟：建模、屬性描述和驗證。最重要的是如何建立系統(tǒng)模型。在系統(tǒng)中，PLC控制器不是孤立的，而是具有與工作環(huán)境、駕駛員和人的交互[8]。因此，這些因素也應該建模。環(huán)境、人、PLC控制器在邏輯上相互獨立和并行。此外，該模型檢查器 SPIN 的輸入語言 Promela 專注于關于描述并發(fā)，所以從這個想法開始，我們將這些因素構建到幾個并發(fā)進程中符合 SPIN 的檢查，它也將準確地描述系統(tǒng)。為了方便描述，它們將是稱為并發(fā)實體。 PLC控制器與并發(fā)實體通過圖像表中的符號。

PLC系統(tǒng)的符號包括I（輸入端口）、Q（輸出端口）和M（中間繼電器）。圖1是一個PLC系統(tǒng)模型圖。時間間隔建模策略：使用標志哪個特定并發(fā)實體的位狀態(tài)代表狀態(tài)中的并發(fā)實體，沒有關于系統(tǒng)時鐘。這可能會忽略時間狀態(tài)的差異，從而簡化了 PLC 模型。

建模策略不加系統(tǒng)時鐘屬性，與原PLC不完全對應模型。那主要是因為加入系統(tǒng)時鐘會導致PLC系統(tǒng)模型過大，沒有對于模型檢查工具來處理這么大模型。對狀態(tài)建模的起點這是不考慮 PLC 掃描的次數，當經歷過遷移。不管掃描多少次經驗豐富的，他們都將包括在這個模型中。在換句話說，真實模型將是構建的子集模型（時間間隔模型）。真實的 PLC 環(huán)境是復雜的，包括一個

各種硬件和人類行為。以下

我們將對不同種類的PLC環(huán)境并發(fā)實體進行分析。

1) 硬件實體

PLC系統(tǒng)的硬件實體主要是一些PLC控制的設備。這些設備的狀態(tài)可以作為PLC控制器的輸入。因此，硬件實體與其關聯(lián)的 I 和 Q 綁定，而硬件有自己的工作流程，這個工作流程是由硬件要求決定的。這個工作流程可以抽象成自動機。該自動機用于描述硬件的工作狀態(tài)。定義 2.1。硬件實體是一個元組 Env =，其中 Ienv 是與硬件綁定的 I 端口entity，Qenv是與實體綁定的Q端口。 A 是描述實體工作流程的自動機，A 是元組 A =，其中 s0 是 A 的初始狀態(tài)，S 是狀態(tài)集合，而 T 是轉移集合。硬件實體的狀態(tài)是 I 符號的子集，并且每個狀態(tài)的 Is 符號都映射到 {True, False}，I符號不出現的狀態(tài)可以是True或 False（即：任意行事）。硬件實體的轉移直接用 Q 的子集表示符號，表示子集中的所有 Q 符號在同時將推動國家之間的遷移。這硬件實體的狀態(tài)轉移圖也需要指定初始狀態(tài)，轉換圖從這種狀態(tài)。

硬件實體的狀態(tài)轉移圖是基于符號 I 的劃分，時間屬性為不考慮。硬件實體狀態(tài)轉換圖實際上是硬件實體的抽象被忽略時間，抽象的模擬需要參考的硬件。

2）簡單的輸出實體僅與 Q 端口綁定的簡單輸出實體不使用 I 端口，這意味著簡單的輸出實體沒有狀態(tài)轉換圖。簡單的輸出entity是顯示PLC工作狀態(tài)的設備，就像號燈一樣。簡單輸出實體的用法是與 Q 端口綁定，以便 PLC 可以使其邏輯設計。

3) 人類行為實體定義 2.2。人類行為實體是一個元組 Env= < Ienv, A>，其中 Ienv 是 I 端口與硬件實體，Qenv是與實體綁定的Q端口。 A 是描述工作流程的自動機實體，A 是一個元組 A =，其中 s0 是初始A 的狀態(tài)，S 是狀態(tài)的集合，T 是狀態(tài)的集合轉移。

人類行為實體與硬件實體類似；它們具有相同的狀態(tài)定義。很難模擬人的行為，尤其是設計一個PLC涉及到一些個人。作為回應這些困難，人類行為建模應該采取一個迭代過程：首先，一個簡單的行為模型是建立使用模型驗證；那么，如果沒有找到柜臺例如，構建并驗證更復雜的模型，

直到找到反例或難以更復雜；最后，如果之前沒有找到有意義的反例，則生成一個完全隨機的人的行為模型（即：人的行為是一個完整的圖

所有轉移都是真實的）以進行驗證。但是，完全隨機行為的驗證會導致狀態(tài)空間急劇增加，那么如何選擇合適的人類行為模型是建模的難點。如果人的輸入比較簡單，我們可以使用完全隨機的行為建模，否則，你需要認真考慮建立合理模型的人類行為。

我們對PLC環(huán)境和人建立模型上面的行為，然后我們將對 PLC 控制器進行建模。 PLC控制器在轉動時會處于一個循環(huán)中上。

? PLC 從 I 端口讀取所有輸入。

? PLC 計算所有邏輯單元。

? PLC 設置所有 Q 端口。

PLC進程上的基本單元稱為網絡。所有網絡將按照編號順序運行設計時設置。

PLC控制器的基本邏輯運算網絡包括：S觸發(fā)器、R觸發(fā)器、SR觸發(fā)器、EQ觸發(fā)器、RS觸發(fā)器，POS上升沿檢測器，NEG下降沿探測器等。對基本邏輯運算網絡建模，我們采用直接映射策略，即：PLC控制器模型的網絡行為和網絡的邏輯行為是完全等價的。哪里觸發(fā)器, R 觸發(fā)器, SR 觸發(fā)器, EQ 觸發(fā)器, RS 觸發(fā)器可以直接使用布爾表達式映射到它們的行為。