【導(dǎo)讀】語的習(xí)慣，語句較通暢，層次較清晰。PLCs是用于各種自動控制系統(tǒng)和過程的可控網(wǎng)絡(luò)集線器。PLCs用軟件接口，標(biāo)準(zhǔn)計算器接口，專門的語言和網(wǎng)絡(luò)設(shè)備編程。最大數(shù)量的通道。觸點數(shù)量是輸入點和輸出點的總和。PLCs可以指定這些值的任。PLCs系統(tǒng)規(guī)則包括掃描。時間，指令數(shù)量，數(shù)據(jù)存儲和程序存儲。掃描時間是PLC需要的用來檢測輸入輸出。用于可編程邏輯控制器的輸入設(shè)備包括DC，AC，中間繼電器，熱電偶，RTD，頻率或脈沖，晶體管，三端雙向可控硅開關(guān)元件；PLC的編程設(shè)備包括控制面板，序執(zhí)行表，動作方塊圖，梯形圖，結(jié)構(gòu)文本，指令序列，五種語言，用國際標(biāo)準(zhǔn)加以規(guī)范，分別為SFC，F(xiàn)BD，LD，ST和IL。能支持順序選擇和并列選擇，二者擇其一即可。它在離散控制上與FBD是完全兼。邏輯程序的圖表表示法。所有的PLC系統(tǒng)有每秒鐘重復(fù)多次的四種基本運行階段。一段時間內(nèi)沒有復(fù)零，時間繼電器會引起錯誤，關(guān)閉PLC系統(tǒng)。輸出模塊也變化，在掃描結(jié)束時PLC的運行速度將大大減慢。

　　

【正文】 brid 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。 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 search first into those parts . . . where counterexamples are likely to be found.” Since this publication a new version of the realtime model checking tool UPPAAL has bee available that employs a costguided evaluation strategy for statespace exploration, viz., costoptimal UPPAAL [4]. This tool is a natural candidate to support the derivation of optimal control schedules in a realtime environment. This motivated us to carry out the optimization part of the case study again with costoptimal UPPAAL, both as an interesting exercise in its own right, and to collect data to interpret and pare with the results obtained with SPIN. The rest of this paper is anized as follows: Sect. 2 gives a description of the batch plant, the nature of PLC, and a description of the control program that was systematically designed in previous work [13]. Section 3 describes the Promela models for the plant and the control process, and their use for its formal verification and optimization. Section 4 then introduces a costoptimal UPPAAL model of the same processes, and presents the optimization results that were obtained using it. Section 5, finally, evaluates the work and presents our conclusions. 7 SOFTWARE BASED PLCS The dropping cost of personal puters is increasing their use in control, including the replacement of PLCs. Software is installed that allows the personal puter to solve ladder logic, read inputs from sensors and update outputs to actuators. These are important to mention here because they don’t obey the previous timing model. For example, if the puter is running a game it may slow or halt the puter. This issue and others are currently being investigated and good solutions should be expected soon. 8 SUMMARY A PLC and puter are similar with inputs, outputs, memory, etc. The PLC continuously goes through a cycle including a sanity check, input scan, logic scan, and output scan. While the logic is being scanned, changes in the inputs are not detected, and the outputs are not updated. PLCs use RAM, and sometime EPROMs are used for permanent programs. 9 PRACTICE PROBLEMS （ 1） Does a PLC normally contain RAM, ROM, EPROM and/or batteries? （ 2） What are the indicator lights on a PLC used for? （ 3） A PLC can only go through the ladder logic a few times per second. Why? （ 4） What will happen if the scan time for a PLC is greater than the time for an input pulse? Why? （ 5） What is the difference between a PLC and a desktop puter? （ 6） Why do PLCs do a self check every scan? （ 7） Will the test time for a PLC be long pared to the time required for a simple program? 10 PRACTICE PROBLEM SOLUTIONS （ 1） Every PLC contains RAM and ROM, but they may also contain EPROM or batteries. （ 2） Diagnostic and maintenance （ 3） Even if the program was empty the PLC would still need to scan inputs and outputs, and do a self check. （ 4） The pulse may be missed if it occurs between the input scans （ 5） Some key differences include inputs, outputs, and uses. A PLC has been designed for the factory floor, so it does not have inputs such as keyboards and mice (although some newer types can). They also do not have outputs such as a screen or sound. Instead they have inputs and outputs for voltages and current. The PLC runs user designed programs for specialized tasks, whereas on a personal puter it is unmon for a user to program their system. （ 6） This helps detect faulty hardware or software. If an error were to occur, and the PLC continued operating, the controller might behave in an unpredictable way and bee dangerous to people and equipment. The self check helps detect these types of faults, and shut the system down safely. （ 7） Yes, the self check is equivalent to about 1ms in many PLCs, but a single program instruction is about 1 micro second.