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