【正文】 avor. EPROMs have also been a popular choice for programming PLCs. The EPROM is programmed out of the PLC, and then placed in the PLC. When the PLC is turned on the ladder logic program on the EPROM is loaded into the PLC and run. This method can be very reliable, but the erasing and programming technique can be time consuming. EEPROM memories are a permanent part of the PLC, and programs can be stored in them like EPROM. Memory costs continue to drop, and newer types (such as flash memory) are being available, and these changes will continue to impact PLCs. 6 Verification and optimization of a PLC control schedule The verification of hybrid systems is a research area of rapidly growing importance in the formal methods munity. The presence of both discrete and continuous phenomena in such systems poses an inspiring challenge for our specification and modelling techniques, as well as for our analytic capacities. This has led to the development of new, expressive models, such as timed and hybrid automata [3, 16], and new verification methods, most notably model checking techniques involving a symbolic treatment of realtime (and hybrid) aspects [7, 11, 17].An important example of hybrid (embedded) systems are process control programs, which involve the digital control of processing plants, ., chemical plants. A class of process controllers that are of considerable practical importance are those that are implemented using Programmable Logic Controllers or PLC. Unfortunately, both PLC and their associated programming languages have no welldefined formal models or semantics, which plicates the design of reliable controllers and their analysis. To assess the capacity of stateoftheart formal methods and tools for the analysis of hybrid systems, the EU research project VHS (Verification of Hybrid Systems) has defined a number of case studies. One of these studies concerns the design and verification of a PLC program for an experimental chemical plant. In this article we report on the use of two model checkers for the verification of a process control program for the given plant and the derivation of optimal control schedules. It is a panion paper to [13], which concentrates on the correct design of the process controller. The original intention of our approach was to see how much could be achieved using the standard model checking environment of SPIN/Promela [8]. As the symbolic calculations of realtime model checkers can be quite expensive it is interesting to try and exploit the efficiency of established nonrealtime model checkers like SPIN in those cases where promising workarounds seem to exist. In our case we handled the relevant realtime properties of the PLC controller using a timeabstraction technique。 （ 7） 是的，在許多 PLC 系統(tǒng)中，自檢大約需要 1ms，但一個(gè)單一程序需 1mms。 （ 4） 如果在兩次輸入掃描之間發(fā)生，脈沖就會(huì)丟失。這些對(duì)于維持是很重要的，因?yàn)樗麄儾挥米袷匾郧暗挠?jì)時(shí)模式 .例如，計(jì)算機(jī)正運(yùn)行一個(gè)游戲，就可能減慢或停止計(jì)算機(jī) .這個(gè)以及其它問(wèn)題現(xiàn)在正被研究，好的解決方案不久就會(huì)出現(xiàn)。在這個(gè)文章中，我們?cè)趦蓚€(gè)樣板的檢驗(yàn)員檢測(cè)的基礎(chǔ)上報(bào)告為給定的系統(tǒng)和最佳的控制引出預(yù)定。存儲(chǔ)器的價(jià)錢一直在下降，新類型正變得可被利 用，這些變化將繼續(xù)對(duì) PLC 系統(tǒng)發(fā)生影響。當(dāng)有電時(shí) ，RAM 的內(nèi)容被保存，但是問(wèn)題在于當(dāng)供給存儲(chǔ)器的電源失去時(shí)會(huì)發(fā)生什么。 圖 6 核驗(yàn) PLC第一次掃描的程序 5 存儲(chǔ)器類型 有幾種基本的現(xiàn)在經(jīng)常使用的計(jì)算機(jī)存儲(chǔ)器類型： RAM（隨機(jī)存儲(chǔ)器） — 這種存儲(chǔ)器速度很快，但是當(dāng)沒(méi)電時(shí)，它 的內(nèi)容將被丟失。 PLC 的狀態(tài)也能被梯形邏輯圖檢測(cè)。通常指示燈表明： 電源啟動(dòng) — 只要 PLC 帶電，它將被啟動(dòng)。如圖 5 所示，梯形圖第一行將檢測(cè)輸入并把輸出 X 置 1，得到相同的值。在繼電器邏輯圖中，程序的每個(gè)元件將盡可能快地開(kāi)關(guān)。這個(gè)邊境效應(yīng)是如果在一段持續(xù)時(shí)間內(nèi)如果一個(gè)輸入變化太短，它可能在輸入掃描之間會(huì)減少或者丟失。 — 這會(huì)表明梯形圖沒(méi)有被正常掃描。最初被第一次接通時(shí)，它會(huì)檢測(cè)它的硬件和軟件是否有錯(cuò)誤。 輸入電路 — 連續(xù)輸入 芯片就像一個(gè)直流 24V 的輸入卡。 圖 2 輸入輸出方向結(jié)構(gòu)圖 在這個(gè)圖表中數(shù)據(jù)通過(guò)輸入設(shè)備進(jìn)入左邊。 2 指令 對(duì)于簡(jiǎn)單的編程，繼電器型 PLC是有效的。繼電器梯形圖或梯形圖是適用于可編程邏輯控制器的重要的編程語(yǔ)言。 SFC 是一種圖表語(yǔ)言，它提供了編程順序的配合，就能支持順序選擇和并列選擇，二者擇其一即可。指令是用于 PLC 軟件（例如數(shù)學(xué)運(yùn)算）的標(biāo)準(zhǔn)操作。 PLCs 用軟件接口，標(biāo)準(zhǔn)計(jì)算器接口，專門(mén)的語(yǔ)言和網(wǎng)絡(luò)設(shè)備編程。 簽名： 年 月 日 注： 請(qǐng)將該封面與附件裝訂成冊(cè)。最大數(shù)量的通道是在一個(gè)擴(kuò)展系統(tǒng)中輸入和輸出通道的最大總數(shù)量。這些語(yǔ)言包括 IEC611313，順序執(zhí)行表（ SFC），動(dòng)作方塊圖（ FBD），梯形圖（ LD），結(jié)構(gòu)文本 （ ST），指令序列（ IL），繼電器梯形圖（ RIL），流程圖， C 語(yǔ)言和 Basic 語(yǔ)言。 ST 是一種文 本語(yǔ)言，用于復(fù)雜的數(shù)學(xué)過(guò)程和計(jì)算，不太適用于圖表語(yǔ)言。 BASIC 語(yǔ)言是用于處理數(shù)據(jù)的連續(xù)的數(shù)字采集和接口運(yùn)行的高級(jí)語(yǔ)言。輸出被送到屏幕。如果我們把個(gè)人計(jì)算機(jī)看作一個(gè)控制器，它通過(guò)在屏幕上輸出激勵(lì)和輸入來(lái)自鼠標(biāo)和鍵盤(pán)的響應(yīng)來(lái)控制用戶。 用普通個(gè)人計(jì)算機(jī)可以運(yùn)行 PLC，雖然則并不被提倡做。 PLC 此時(shí)將從自我檢測(cè)開(kāi)始重新啟動(dòng)這個(gè)過(guò)程，這個(gè)過(guò)程很明顯地每秒鐘重復(fù) 10 到 100 次，正如圖 3 所示 。 輸入輸出掃描經(jīng)常會(huì)令初學(xué)者感到迷惑，但是他們是很重要的。這樣做的主要原因是如果一個(gè)程序在多個(gè)地方用一個(gè)輸入值，那么輸入值的變化將使其邏輯關(guān)系無(wú)效。在第二層，沿著梯形邏輯圖移動(dòng)之前，將先解釋分支。并且梯形圖的第一行將無(wú)效。最普通的按鈕是一個(gè)運(yùn)行 /編程選擇開(kāi)關(guān)，當(dāng)在保持狀態(tài)時(shí)，它將被調(diào)到編程；當(dāng)在生產(chǎn)狀態(tài)時(shí)，它將被調(diào)到運(yùn)行。根據(jù)例子中的邏輯關(guān)系，第一次掃描將封上 “ 變亮 ” ，直到 “ 清除 ” 被啟動(dòng)。 EEPROM（電可擦除可編程只讀存儲(chǔ)器） — 這種存儲(chǔ)器能像 ROM 一樣存放程序。當(dāng) PLC 被啟動(dòng)時(shí)，在 EPROM 上的梯形邏輯程序被下載 PLC 并且運(yùn)行。令人失望的是 PLC 和他們組成的系統(tǒng)語(yǔ)言都沒(méi)有好標(biāo)準(zhǔn)，不能用正式的模型來(lái)設(shè)計(jì)復(fù)雜可靠的控制器。這篇文章開(kāi)始部分介紹 PLC 性質(zhì)。 9 實(shí)際問(wèn)題 （ 1） 一個(gè) PLC 系統(tǒng)通常包括 RAM， ROM， EPROM 和 /或電池嗎？ （ 2） PLC 的指示燈用于什么？ （ 3） 為什么一個(gè) PLC 系統(tǒng)每秒鐘只能掃描梯形圖幾次？ （ 4） 如果一個(gè) PLC 系統(tǒng)的掃描時(shí)間比輸入脈沖長(zhǎng)，會(huì)發(fā)生什么 ?為什么？ （ 5） 一個(gè) PLC 系統(tǒng)與一部臺(tái)式計(jì)算機(jī)的不同是什么？ （ 6） 為什么 PLC 系統(tǒng)每次掃描要做自我檢查？ （ 7） PLC 檢測(cè)時(shí)間會(huì)比簡(jiǎn)單程序所需時(shí)間長(zhǎng)嗎？ 圖 7 梯形示意圖 10 實(shí)際問(wèn)題解答 （ 1） 每個(gè) PLC 系統(tǒng)包括 RAM 和 ROM，但是他們也包括 EPROM 或電池。 （ 6） 這能幫助檢測(cè)硬件和軟件錯(cuò)誤。 for the scheduling we implemented in Promela a socalled variable time advance procedure [15]. For this case study these techniques proved sufficient to verify the design of the controller and derive (time) optimal schedules with very reasonable time and space requirements. A first report on our experiences has been published as [5], whose findings are further extended and elaborated in this article. One of the conclusions of our initial experiments as reported in the initial publication [5] was that “. . . it would be useful to be able to influence the search strategy of the model checker more directly and guide the