【正文】 時(shí)型檢測(cè)器的效率是很有意義的，就像在有可能存在的工作區(qū)內(nèi)進(jìn)行SPIN一樣。在此項(xiàng)目中對(duì)可編程邏輯控制器的相關(guān)實(shí)時(shí)參數(shù)進(jìn)行處理并且這些可編程邏輯控制器都運(yùn)用時(shí)域采樣技術(shù)。對(duì)于此進(jìn)程我們?cè)赑romela中運(yùn)行一種所謂的變時(shí)超前程序。這項(xiàng)技術(shù)的研究足夠可以證明在合理的時(shí)間和空間的要求下驗(yàn)證控制器的設(shè)計(jì)和推導(dǎo)優(yōu)化程序。1　介紹　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)42當(dāng)今，混合系統(tǒng)的驗(yàn)證在一個(gè)正規(guī)的系統(tǒng)領(lǐng)域里是一個(gè)流行的主題。不連續(xù)和連續(xù)的現(xiàn)象的出現(xiàn)給我們的規(guī)范和建模技術(shù)以及我們分析的能力提出了一個(gè)鼓舞性的挑戰(zhàn)。這促進(jìn)了新的發(fā)展和涌現(xiàn)更有效的模式，比如時(shí)控的和混合的自動(dòng)控制[]，以及新的驗(yàn)證方式，大部分顯著的檢測(cè)技術(shù)模式包括實(shí)時(shí)（和混合）方面的符號(hào)處理[10,17,6]。舉一個(gè)重要的例子,混合（嵌入）系統(tǒng)都是過(guò)程控制程序，它們都包括處理設(shè)備的數(shù)字控制，比如化學(xué)設(shè)備。具有相當(dāng)大實(shí)用性價(jià)值的過(guò)程控制器都利用可編程邏輯計(jì)算機(jī)或可編程邏輯控制器。不幸的是，可編程邏輯控制器和它們有關(guān)的設(shè)計(jì)語(yǔ)言沒(méi)有定義成正規(guī)的形式，語(yǔ)義學(xué)使可靠的控制器的設(shè)計(jì)和它們的分析變得復(fù)雜。為了混合系統(tǒng)的分析而對(duì)專(zhuān)業(yè)的正規(guī)模式和方法的效力進(jìn)行評(píng)估，EC混合系統(tǒng)驗(yàn)證研究項(xiàng)目已經(jīng)寫(xiě)出了許多項(xiàng)目論文。其中一篇論文談到了對(duì)于實(shí)驗(yàn)用的化學(xué)設(shè)備的可編程邏輯控制器程序的設(shè)計(jì)和驗(yàn)證。在這些論文中報(bào)導(dǎo)了為了對(duì)于特定設(shè)備的過(guò)程控制程序的驗(yàn)證以及最優(yōu)控制程序的推導(dǎo)而使用的SPIN模式檢測(cè)器。它是對(duì)進(jìn)程控制器的正確設(shè)計(jì)的一個(gè)指南。這種方法的目的是調(diào)查有多少種檢測(cè)SPIN/Promela 的環(huán)境的標(biāo)準(zhǔn)模型可以使用。盡管實(shí)時(shí)型檢測(cè)器的符號(hào)運(yùn)算器有可能很貴但測(cè)試開(kāi)發(fā)非實(shí)時(shí)型檢測(cè)器的效率是很有意思的，就像在有可能存在的工作區(qū)內(nèi)進(jìn)行SPIN一樣。在此項(xiàng)目中對(duì)可編程邏輯控制器的相關(guān)實(shí)時(shí)參數(shù)進(jìn)行處理并且這些可編程邏輯控制器都運(yùn)用時(shí)間抽象化技術(shù)。對(duì)于進(jìn)程在Promela中運(yùn)行一種所謂的預(yù)置時(shí)間程序。這項(xiàng)技術(shù)的研究足夠可以證明在合理的時(shí)間和空間的要求下驗(yàn)證控制器的設(shè)計(jì)和推導(dǎo)最優(yōu)程序。這篇論文其余的部分如下所示：第二章對(duì)混合設(shè)備進(jìn)行了描述，對(duì)于可編程邏輯控制器的特性和控制程序的描述在[12]中有詳細(xì)地說(shuō)明。第三章描述了設(shè)備的Promela模式和控制過(guò)程，以及在正式的驗(yàn)證和最優(yōu)化工作中的運(yùn)用。第四章對(duì)上述內(nèi)容做出總結(jié)。2　系統(tǒng)描述這項(xiàng)研究的系統(tǒng)基本上是嵌入的系統(tǒng)，由混合設(shè)備和一個(gè)可編程邏輯控制器組成，在下面都有對(duì)它們更詳細(xì)的描述。這項(xiàng)研究最初的目標(biāo)是編寫(xiě)一個(gè)控制程序以使具備此控制程序的設(shè)備和可編程邏輯控制器一起按照計(jì)劃運(yùn)轉(zhuǎn)。設(shè)計(jì)的動(dòng)作首先是不斷進(jìn)行混合，然后控制程序會(huì)定期優(yōu)化，也就是使進(jìn)行混合的平均時(shí)間最短?！』旌显O(shè)備的描述　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)43這項(xiàng)研究的混合設(shè)備（見(jiàn)圖1）是一個(gè)實(shí)驗(yàn)用的化學(xué)設(shè)備，最初是為學(xué)生實(shí)驗(yàn)而設(shè)計(jì)。下面我們來(lái)描述它的主要特性；在[9]上有更多細(xì)節(jié)的說(shuō)明。這個(gè)設(shè)備是用來(lái)混合濃鹽溶液（在B1容器中）和水（在B2容器中）來(lái)對(duì)溶液進(jìn)行稀釋。這些成分在B3容器中混合以得到被稀釋的溶液，然后運(yùn)送到B4容器中再送到B5容器中。在B5容器中進(jìn)行蒸發(fā)。被蒸發(fā)的水經(jīng)過(guò)一個(gè)冷凝器送到容器B6中，水被冷卻后又被抽回B2容器。B5容器中殘留的熱的濃鹽溶液被送到容器B7中，冷卻后抽回到容器B1中。被控的混合設(shè)備是一個(gè)明顯的混合系統(tǒng)。不連續(xù)的成分是控制程序以及閥，攪拌器，加熱器，冷卻器（開(kāi)/關(guān)，起動(dòng)/停止）的（抽象的）狀態(tài)。連續(xù)的成分是容器充滿程度，溫度，以及時(shí)間。后者在一方面可以分解成設(shè)備的實(shí)時(shí)狀態(tài)，比如容器填充，蒸發(fā)，混合，加熱和冷卻次數(shù)，程序執(zhí)行和反應(yīng)次數(shù)（可編程邏輯控制器掃描周期時(shí)間），另外混合設(shè)備的控制是一個(gè)很好的嵌入系統(tǒng)的例子：控制，數(shù)字設(shè)備是一個(gè)很大的具有特殊功能的實(shí)體系統(tǒng)的一部分。為了研究，決定固定混合劑量大?。涸鲜且环N濃度為5g/。用這些混合容器B1，B2，B4，B6和B7都可以容納兩個(gè)原料單位，B3和B5只能容納一個(gè)原料單位。在[9]中的設(shè)備描述還提到從一個(gè)容器到另一個(gè)容器的運(yùn)送步驟的持續(xù)時(shí)間。在（時(shí)控）設(shè)備模式中用這些持續(xù)時(shí)間作為基礎(chǔ)，盡管真實(shí)的持續(xù)時(shí)間有可能和它們不太一樣。B1－B3B2－B3B3－B4B4－B5heat B5B5B7 cool B6cool B7B6B2 B7B1320 240 70 350 1100 280 300 600 240 220表格1.　以秒為單位的設(shè)備程序的持續(xù)時(shí)間2．2　可編程邏輯控制器可編程邏輯控制器是有特殊設(shè)計(jì)控制任務(wù)的計(jì)算機(jī)。它們的應(yīng)用領(lǐng)域非常大。這里，簡(jiǎn)要地強(qiáng)調(diào)一下可編程邏輯控制器與普通計(jì)算機(jī)相對(duì)照的主要特性。最重要的不同之處是可編程邏輯控制器中的程序是永久循環(huán)運(yùn)行的這就是所謂的掃描周期。在一個(gè)掃描周期中可編程邏輯控制器中的程序執(zhí)行一次，程序的執(zhí)行取決于寄存器中存儲(chǔ)的變化的數(shù)值。一個(gè)掃描周期的長(zhǎng)度是以毫秒來(lái)計(jì)算的，它取決于程序的長(zhǎng)度。此外，在每一個(gè)掃描周期與外界都有一個(gè)數(shù)據(jù)交換：可編程邏輯控制器有輸入點(diǎn)經(jīng)一個(gè)接口與寄存器中的一個(gè)專(zhuān)用的輸入?yún)^(qū)域相連，并且可編程邏輯控　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)44制器的輸出點(diǎn)經(jīng)一個(gè)接口與寄存器的輸出區(qū)域相連。對(duì)于輸入點(diǎn)可編程邏輯控制器從傳感器上獲得數(shù)據(jù)，對(duì)于輸出點(diǎn)可編程邏輯控制器給執(zhí)行裝置發(fā)送數(shù)據(jù)。最后，在循環(huán)周期中操作系統(tǒng)還會(huì)執(zhí)行一些工作（自檢測(cè)，監(jiān)視等等）。操作系統(tǒng)本身很小并且很穩(wěn)定，它的必備條件是可靠的實(shí)時(shí)控制。可編程邏輯控制器的程序要用計(jì)算機(jī)在特殊的設(shè)計(jì)環(huán)境下開(kāi)發(fā)編譯并且可以裝載到可編程邏輯控制器上。許多不同的設(shè)計(jì)語(yǔ)言收集在[8]中。在應(yīng)用程序中采用順序功能圖表和PetriNet相關(guān)的圖形語(yǔ)言，并且每一個(gè)掃描周期程序的執(zhí)行都取決于當(dāng)時(shí)起作用的位。在這種直感的順序功能圖中提供了一種meta結(jié)構(gòu)并且應(yīng)用程序中的實(shí)際指令都被編寫(xiě)到指令序列當(dāng)中，就是一種匯編語(yǔ)言。與我們通常所涉及的設(shè)計(jì)語(yǔ)言不同的是在這些語(yǔ)言中有可能用到定時(shí)器?！　　　　　　　　　　　　　　√旖蚬こ處煼秾W(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)45圖 1　混合設(shè)備的 P/I 圖表這種掃描周期機(jī)制使可編程邏輯控制器與順序程序（緊密的循環(huán)控制）的控制相匹配?？墒?，一定要保證掃描周期的長(zhǎng)度總要少于設(shè)備控制整個(gè)系統(tǒng)所需要的最短反應(yīng)時(shí)間。在這項(xiàng)研究中掃描周期時(shí)間與反應(yīng)時(shí)間相比是一個(gè)非常小數(shù)量級(jí)。一個(gè)掃描周期的執(zhí)行時(shí)間只有幾毫秒。在這個(gè)范圍內(nèi)的定時(shí)操作與一些應(yīng)用程序有關(guān)，　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)46比如機(jī)床控制。而對(duì)于我們的化學(xué)設(shè)備則無(wú)關(guān)：一個(gè)閥早 10 毫秒或晚 10 毫秒關(guān)閉都沒(méi)有太大的關(guān)系。當(dāng)整個(gè)系統(tǒng)建模的時(shí)候與這個(gè)參數(shù)就有關(guān)了。這里，我們可以模仿可編程邏輯控制器就好像程序連續(xù)地運(yùn)行一樣，也就是說(shuō)一個(gè)掃描周期要發(fā)生在零點(diǎn)。在與可編程邏輯控制器的對(duì)比下這種設(shè)備很慢以至于不能與具備了真正形成理想的連續(xù)控制掃描周期的可編程邏輯控制器相提并論。更多關(guān)于模擬可編程邏輯控制器的細(xì)節(jié)的討論見(jiàn)[11]。　控制程序這一部分的要旨在于當(dāng)我們?cè)谝环N非正式的途徑運(yùn)用這種設(shè)備的時(shí)候關(guān)于這種設(shè)備和控制程序的觀點(diǎn)。它的正式的推導(dǎo)以及其它的驗(yàn)證操作在[12]中有介紹。在這個(gè)設(shè)備中我們加入了許多傳輸步驟，比如把 的鹽溶液從 B1 容器輸送到 B3容器中。所有可能發(fā)生的傳輸步驟，比如蒸發(fā)步驟和兩個(gè)冷卻步驟會(huì)導(dǎo)致許多相同的步驟。在每一個(gè)過(guò)程中的動(dòng)作都很簡(jiǎn)單比如打開(kāi)閥門(mén)，打開(kāi)攪拌器，抽水器或加熱器，并且當(dāng)這個(gè)步驟結(jié)束的時(shí)候，又關(guān)閉、斷開(kāi)了所有東西。每個(gè)步驟當(dāng)激活條件滿足的時(shí)候才開(kāi)始，否則就處于等待狀態(tài)。一個(gè)正在運(yùn)行的程序（狀態(tài)）直到它的停止條件滿足才停下來(lái)。然后它又回到等待狀態(tài)。用這種方法研究出了一種所謂的閉環(huán)控制：改變狀態(tài)的標(biāo)準(zhǔn)不再是時(shí)間觸發(fā)，而是由事件驅(qū)動(dòng)。這種程序結(jié)構(gòu)很容易在圖 2 的關(guān)于順序功能圖的介紹中找到。圖 2　順序功能圖的控制程序控制程序在“開(kāi)始”的狀態(tài)下啟動(dòng)（因?yàn)檗D(zhuǎn)換條件為真）并且立即分配 12 個(gè)相　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)47同的等待狀態(tài)。在等待狀態(tài)下的程序不運(yùn)行。如果控制器變成 Pi 狀態(tài)，那么只要控制器保持 Pi 狀態(tài)，帶有 Pi 狀態(tài)的程序就在每一個(gè)掃描周期內(nèi)運(yùn)行。帶有P1,……，P12 狀態(tài)的程序都包含在圖 3 有關(guān)所謂的指令序列格式中。指令序列里的指令都是匯編語(yǔ)句。這里，我們主要做的是讀出對(duì)于存儲(chǔ)器中的常數(shù)是真是假并且往存儲(chǔ)器中寫(xiě)入變量，也就是 Vi，代表變量。動(dòng)作的限制標(biāo)志 P1（在每一個(gè)程序的頂部）表示當(dāng)控制信號(hào)來(lái)到時(shí)這些指令有權(quán)僅在第一個(gè)掃描周期內(nèi)運(yùn)行；P0 表示當(dāng)控制在此位置時(shí)這些指令僅在最后一個(gè)掃描周期內(nèi)運(yùn)行。程序的主要的復(fù)雜性在于激活條件216。i。我們假設(shè)對(duì)于每一步都有一個(gè)變量PiX，Pi 表示控制信號(hào)是否在相應(yīng)的步驟里（這些變量在可編程邏輯控制器都是可用的）。程序開(kāi)始的條件如下所示：1． 容器的填充程序必須考慮到一個(gè)輸送步驟：上面的容器必須包含足夠的原料，下面的容器必須有足夠的空間等等。這些條件被編碼成圖4的變量216。i。2． 不能同時(shí)讓一個(gè)容器在兩個(gè)步驟中使用。也就是，當(dāng)把溶液從B4容器輸送到B5容器中時(shí)就不應(yīng)該發(fā)生從B3容器向B4 容器輸送原料的動(dòng)作。這個(gè)要求是由有關(guān)閥門(mén)的條件得出的：當(dāng)溶液從B4容器向B5 容器輸送時(shí)閥門(mén) V11必須在輸送過(guò)程中關(guān)閉。這些要求引出了一個(gè)在輸送過(guò)程的茅盾結(jié)構(gòu)。它要求控制信號(hào)不能同時(shí)出現(xiàn)在兩個(gè)茅盾的步驟中。這個(gè)條件分成兩個(gè)部分：首先，如果茅盾的步驟已經(jīng)發(fā)生那么控制信號(hào)就不能再去其他的步驟。這些條件被編碼成圖5中的變量216。i。其次，當(dāng)茅盾的步驟同時(shí)擁有控制信號(hào)時(shí)只有一個(gè)有優(yōu)先權(quán)。這些優(yōu)先權(quán)是固定的，并且它們的優(yōu)先權(quán)是自由循環(huán)的。它們就形成了圖6中的變量216。i?！　　　　　　　　　　　　　　√旖蚬こ處煼秾W(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)48圖3　步驟P1到P12 的指令序列程序這種可編程邏輯控制器的執(zhí)行機(jī)制保證了相同步驟的同步運(yùn)行：每一個(gè)掃描周期內(nèi)每一步驟的程序只執(zhí)行一次。這種同步機(jī)制使條件 216。i 達(dá)到預(yù)期的作用。圖 4　容器的填充條件　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)49圖 5　如果茅盾的發(fā)生步驟程序可能不能啟動(dòng)圖 6　兩個(gè)茅盾的步驟只能有一個(gè)擁有優(yōu)先權(quán)3 Spin的驗(yàn)證和優(yōu)化這部分描述了在圖 2 中的可編程邏輯控制器的驗(yàn)證和它的隨后的優(yōu)化的方法。對(duì)于驗(yàn)證，構(gòu)造了一種控制程序模式和 Promela 設(shè)備,完成采樣工作。我們用模式檢測(cè)器 SPIN 檢測(cè)所有能夠使混合工作不斷進(jìn)行的組合模式的執(zhí)行順序。這就意味著在理想的環(huán)境下，沒(méi)有原料在泄漏和蒸發(fā)以及不斷地混合的過(guò)程中損失，所謂的控制就　是使混合工作能夠不斷的進(jìn)行。有關(guān)驗(yàn)證程序的細(xì)節(jié)在第 3 章第一節(jié)中進(jìn)行說(shuō)明；技術(shù)上的總結(jié)在第 4 章中說(shuō)明。　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)50　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)51　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)52　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)53　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)54　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)55　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)56　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)57　　　　　　　　　　　　　　　天津工程師范學(xué)院 2022 屆畢業(yè)設(shè)計(jì)(論文)58