電梯PLC控制系統(tǒng)設(shè)計
附錄1：外文譯文
第十九屆世界大會論文集國際自動控制聯(lián)合會開普敦，南非。
2014年8月24日至29日
大型PLC程序中的定時方面的建模和正式驗證
Borja Fernandez Adiego丹尼爾·達(dá)拉斯
Enrique Blanco Vi?nuela Jean-Charles Tournier
V ctor M. Gonzalez Suarez Jan Olaf Blech
CERN，歐洲核研究組織，CH-1211 Geneva 23，瑞士（電子郵件:fborja.fernandez.adiego,daniel.darva，enrique.blanco，jean-charles.tournierg@cern.ch）。
ISA，University of Oviedo，Campus de Viesques 33204 - Gijon，Spain（電子郵件：victor@isa.uniovi.es）
RMIT大學(xué)，澳大利亞墨爾本（電子郵件：janolaf.blech@rmit.edu.au）
摘要：防止模型檢查在工業(yè)控制系統(tǒng)中廣泛使用的主要障礙之一是從PLC程序構(gòu)建正式模型的復(fù)雜性，特別是當(dāng)需要集成時序方面時。本文通過提出一種模擬和驗證PLC程序的時序方面的方法來解決這個障礙。提出了兩種方法以允許用戶平衡模型的復(fù)雜性（即其狀態(tài)數(shù)）與可能被驗證的規(guī)范的集合之間的貿(mào)易。已經(jīng)開發(fā)了一種支持該方法的工具，該方法允許直接從PLC程序產(chǎn)生用于不同模型檢查器的模型。 本文使用NuSMV提出了實際PLC程序的時序方面的驗證。
關(guān)鍵詞：PLC，定時器，正式驗證，模型檢驗，自動機，抽象
1.引言
CERN，歐洲核研究組織，依靠大量的PLC（可編程邏輯控制器）應(yīng)用來操作其不同的粒子加速器。這些應(yīng)用對于CERN操作至關(guān)重要，因此保證其行為符合其規(guī)定是最重要的。正式驗證，特別是模型檢查，似乎是一個有前途的技術(shù)，以確保PLC程序滿足其初始規(guī)格。然而，由于構(gòu)建PLC程序的形式模型的復(fù)雜性，這種技術(shù)在工業(yè)中沒有被廣泛使用，構(gòu)建這樣的形式模型需要對系統(tǒng)進(jìn)行建模（硬件和軟件）以及基礎(chǔ)模型的深入知識檢查器。此外，當(dāng)需要考慮定時方面，即PLC時間和定時器時，模型化任務(wù)變得甚至更復(fù)雜，因為所得到的模型，無需重新定義表示，通常在狀態(tài)空間而言過大而無法通過模型檢查器來處理。
在本文中，我們提出了一種方法來建立PLC時間和計時器。該方法被整合到Darvas等人描述的通用框架中（2013）允許從PLC程序自動生成正式模型。提出了兩種方法來考慮定時方面：現(xiàn)實和抽象模型化。在現(xiàn)實的做法表示定時器的行為和時間在PLC的內(nèi)部表示高保真度。這種建模允許驗證時間相關(guān)的屬性以確保給定的動作將（或不會）在給定延遲之后或之后執(zhí)行（例如，在給定輸入被設(shè)置為真之后500ms后PLC輸出設(shè)置為真）。雖然這種模型化在表現(xiàn)力方面是強大的，但是它可能產(chǎn)生太大而不能由模型檢查器處理的模型，因此導(dǎo)致第二建模方法。抽象方法省略了時間本身的建模，并給出了一個非確定性的定時器模型。與第一種方法相比，這大大減少了生成模型的狀態(tài)空間，因此允許驗證大型PLC程序，同時仍然提供驗證一些時間相關(guān)規(guī)格的能力。可以通過應(yīng)用該第二建模來驗證的屬性例如是活性屬性（例如，在其輸入被設(shè)置為假之后，PLC輸出將被設(shè)置為真）。使用抽象時間模型化驗證的要求在現(xiàn)實模型上仍然有效，因為現(xiàn)實的方法是抽象的模型的重構(gòu)。最后，工具實現(xiàn)兩種類型的時間模型化，并產(chǎn)生正式型號為NuSMV（Cimatti等人（2002）），BIP（Basu等人（2011））和UPPAAL（Amnell等人（2001））已 開發(fā)并應(yīng)用于CERN的控制系統(tǒng)。
1.1相關(guān)工作
雖然以前在文獻(xiàn)中已經(jīng)研究了PLC程序的建模時序行為，但是它們都沒有提供允許自動地生成包括時序方面的形式模型并且同時執(zhí)行對這些模型的驗證的一般方法。此外，文獻(xiàn)中發(fā)現(xiàn)的所有方法都限于特定的模型檢查器，從而阻止了不同類型的模型檢查器的優(yōu)點。
事實上，Mader和Wupper（1999）或Perin和Faure（2013）提出了一種使用定時自動機模型對PLC定時器建模的方法，但不提供驗證結(jié)果。由于時間被認(rèn)為是線性和單調(diào)函數(shù)，所以生成的模型將具有巨大的狀態(tài)空間，如果這種方法將被應(yīng)用于大型系統(tǒng)，使得驗證是不可能的，因為是在CERN開發(fā)的系統(tǒng)。類似地，Mokadem等人（2010）提出了一個案例研究，其中為驗證目的創(chuàng)建了定時多任務(wù)PLC程序的全局模型。這種方法類似于由Mader和Wupper（1999）提出的方法，但是使用UPPAAL使用時鐘執(zhí)行驗證，并且因此具有單調(diào)時間表示。在Wang et al（2013）中，使用基于組件的BIP框架對包括定時器的PLC控制系統(tǒng)的幾個方面進(jìn)行建模。在這種情況下，在這種情況下，它們假設(shè)xed PLC周期長度是一個大的應(yīng)變，與實際的PLC定時器相比，定時器模型不夠精確。此外，不提供驗證結(jié)果。
本文的其余部分結(jié)構(gòu)如下：第2節(jié)介紹了PLC中的時間和計時器的概念。第3節(jié)概述了所提出的方法，允許為PLC程序中的各種模型檢查器生成正式模型。第4節(jié)詳細(xì)介紹了對PLC程序時序方面進(jìn)行建模的兩種建議方法，以及應(yīng)用模型化的案例研究。此外，本節(jié)正式表明，現(xiàn)實的時間模型化是其抽象的一個要素。最后，第5節(jié)通過突出它們的優(yōu)點和缺點來分析這兩種方法，并在文章結(jié)束。
2. 定時PLC控制系統(tǒng)
本節(jié)概述PLC控制系統(tǒng)，重點介紹時序方面。此外，提出了一個案例研究，將用于其余部分，以說明本文提出的模型化方法。
2.1 PLC的時序特性
PLC是執(zhí)行稱為掃描周期的同步和循環(huán)過程的工業(yè)計算機，包括以下主要步驟：（1）讀取存儲器的輸入值，（2）使用讀取數(shù)據(jù)解釋和執(zhí)行程序邏輯 ，以及（3）將計算的輸出值寫入實際輸出。
在標(biāo)準(zhǔn)PLC，即非安全PLC中，周期時間不是固定的，但是存在由看門狗模塊實施的上限。 如果PLC循環(huán)時間大于該上限，例如，由于PLC程序中的無限循環(huán)，PLC執(zhí)行負(fù)責(zé)處理定時錯誤的程序的特殊部分。相比之下，安全PLC具有固定周期時間。
定時器操作，例如定時器，由IEC 61131定義，可以被認(rèn)為是延遲信號或產(chǎn)生脈沖的功能塊。 不同類型定時器可以在PLC中找到，最常見的定時器之一是TON（定時器打開延遲）（見圖1）。該定時器有2個輸入變量：IN和PT。IN是一個布爾輸入信號，PT是延遲時間。定時器有2個輸出：Q和ET。Q是布爾輸出變量，當(dāng)IN執(zhí)行上升沿時，其值將在預(yù)定延遲（PT）后為真，如果IN為假，則其值為假。 ET是經(jīng)過的時間，其值增加到PT，當(dāng)IN上出現(xiàn)上升沿時開始。
圖1.TON時間圖
PLC定時器使用特定的數(shù)據(jù)類型用于稱為TIME的定時操作。這種數(shù)據(jù)類型由IEC 61131定義為一個簡單的變量，它說明“這些數(shù)據(jù)類型中的值的范圍和表示的精度是依賴于實現(xiàn)的”。通過一個有限變量表示時間導(dǎo)致非單調(diào)的時間表示為變量可以溢出時（比較圖的上半部分圖2）。例如，在Siemens S7 PLC中，TIME數(shù)據(jù)類型定義為具有1毫秒相同精度的有符號32位整數(shù)（見Siemens（1998）），其上限約為+24天，下限為 的24天。然而，在Schneider和Beckho PLC中，TIME數(shù)據(jù)類型是無符號的32位整數(shù)，精度為1 ms。在本文中，我們考慮在西門子PLC中標(biāo)記的時間解釋。
圖2.有時間表示的后果
2.2案例研究
在本文的上下文中，把CERN開發(fā)和使用的工業(yè)控制系統(tǒng)框架稱為UNICOS（Blanco等人（2011））作為一個案例研究。UNICOS提供了表示通用工業(yè)控制儀器（例如傳感器，執(zhí)行器，子系統(tǒng)）的基本對象的庫。這些對象在PLC代碼中表示為功能塊，使用ST（結(jié)構(gòu)化文本）語言，可以調(diào)用PLC上的不同功能塊。目前UNICOS被實現(xiàn)用于標(biāo)準(zhǔn)PLC，即其中周期時間不是固定的，并且取決于總體應(yīng)用。
在本文中，我們重點介紹由UNICOS庫為西門子PLC提供的OnO對象。該對象用于表示作為由數(shù)字信號（例如閥，加熱器，電動機）驅(qū)動的執(zhí)行器的物理設(shè)備。使用60個輸入變量（其中13個是參數(shù)），62個輸出變量，600行ST代碼和3個定時器實例，OnO對象在大小和復(fù)雜性方面代表其他UNICOS對象。
附錄2：外文文獻(xiàn)
30