基于形式化方法的PLC建模和检测-毕业论文外文文献翻译.docx

《基于形式化方法的PLC建模和检测-毕业论文外文文献翻译.docx》由会员分享，可在线阅读，更多相关《基于形式化方法的PLC建模和检测-毕业论文外文文献翻译.docx（21页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、外文文献译文设计(论文)题目: S7-200系列PLC实现电梯模型控制 专业与班级: 学生姓名: 指导教师: 年月日10 J. Software Engineering & Applications, 2010, 3, 1054-1059 doi:10.4236/jsea.2010.311124 Published Online November 2010 (http:/www.SciRP.org/journal/jsea) CopyrightPLC Modeling and Checking Based on Formal Method* Yueshan Zheng1,2, Guiming

2、Luo1,2, Junbo Sun1,2, Junjie Zhang1,2, Zhenfeng Wang1,2 1Tsinghua National Laboratory for Information Science and Technology, Tsinghua University, Beijing, China; 2School of Software, Tsinghua University, Beijing, China. Email: championkop, gluo Received September 5th, 2010; revised September 16th,

3、2010; accepted September 24th, 2010. ABSTRACTHigh reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of co

4、mplex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduc

5、e the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the PROMAL language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example

6、 is found. Although the probability of this logic error occurs very small, it could result in system crash fatally. Keywords: Model Checking, PLC Modeling, PLC-Checker, Formal Method1. Introduction PLC is an automatic control device that can receive information from sensors, computing device or othe

7、r PLC logic input signal, and output the logic signal processed. The control algorithm can be written using standard language, such as Ladder Diagram (LD), Structured Text (ST) or Instruction List (IL) 1. The technique of PLC using programmable language to control large scale integrated circuit has

8、been widely used in industry 2. Because of safety critical software can cause serious damage to life or property, verification of safety critical software has become an indispensable step required to assure software quality. The present verifying method for the PLC is still stuck by simulation and t

9、esting. However, they cannot cover all possible cases, especial whether the design model of PLC to meet the demand. Therefore, the model checking technology is introduced into the field of PLC. To give theoretical analysis of PLC design becomes important. The primary step of PLC model checking is to

10、 the establishment of PLC model, such as establish a model from Function Charts 3. The PLC model focuses on the establishment of the time attributes 4. It can be modeled by the method of timed automata 5 or time period modeling method 6. Thus state space of the model will be decreased compared to ti

11、med automata. Either way one choose, eventually an abstract model can be given 7. How to build a good PLC abstract model is the most important issue to the checking. As the manually modeling is easy to introduce many errors, so the establishment of an integrated modeling and testing tool is very imp

12、ortant, and this is one of the issues of concern to this paper. PLC control program runs in real-time operating sys-tem (multi-task or single-task); this paper is mainly based on multi-task scheduling PLC system. Section 2 of the article has an introduction to the modeling method of PLC system. Sect

13、ion 3 gives the analysis and improvement of this model as we need to reduce the probability of pseudo-errors. Section IV designs a model checking tool PLC-Checker to check the established model, including introduce the way of converting PLC program into SPINs input language PROMELA code. Finally, a

14、classical PLC example is applied to check and a critical counter-example is found by the PLC-Checker.2. PLC Modeling There are three steps of model checking: modeling, property description, and verification. The most important is how to build the system model. In the system, PLC controller is not is

15、olated, but has interaction with its working environment, driver and human 8. Therefore, these factors should also be modeling. The environment, human, and the PLC controller is independent and concurrent with each other in logic. Also, the model checker SPINs input language PROMELA is focused on de

16、scribing the concurrent, so starting from this idea, we build these factors into several concurrent processes to fit the checking from SPIN, it will also accurately describe the system. To describe conveniently, they will be called concurrent entities. PLC controller interacts with the concurrent en

17、tities through the symbols in image table. The symbols of PLC system include I (input port), Q (output port), and M (intermediate relay). Figure 1 is a diagram of PLC system model. Time interval modeling strategy: using the flag which specific the bit state of concurrent entities to represent the co

18、ncurrent entities in the state, without regard to the system clock. This may neglect the time difference of states, thus simplifying the PLC model. The modeling strategy does not add the system clock properties, not fully corresponds with the original PLC model. That is mainly due to join the system

19、 clock will cause PLC system model become too large, there is no for model checking tool to deal with such a large model. The starting point for modeling the state like this is not to consider the number of PLC scans when a migration is experienced. No matter how many scans it experienced, they will

20、 all include in this model. In other words, the real model will be a subset of the built model (Time interval model). The real PLC environment is complex, and includes a variety of hardware and human behavior. The following we will give an analysis of different kinds of PLC environment concurrent en

21、tities1) Hardware entity Hardware entity of the PLC system is mainly some equipment that PLC controls. The state of these equipments can be the input of PLC controller. Therefore, the hardware entity binding with its associated I and Q, while the hardware has its own workflow, this workflow is decid

22、ed by the hardware requirements. This work flow can be abstracted into automata. This automata is used to describe the working status of the hardware. Definition 2.1. A Hardware entity is a tuple Env = , where Ienv is the I port binding with the hardware entity, Qenv is the Q port binding with the e

23、ntity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. The states of hardware entities is a subset of I symbols, and the Is sign each state are all mapped to True, False,

24、the I symbol do not appear in the state can be either True or False (that is: act arbitrarily). The transfer of the hardware entities directly expressed with the subset of Q symbols, said that all Q symbols in the subset be true at the same time will drive migration between states. The state transit

25、ion diagram of hardware entities also need to specify an initial state, the transitions graph starts from this state. The hardware entities states of transition diagram are based on the division of symbol I, and time properties are not taken into account. Hardware entities state transition diagram i

26、s actually an abstract of hardware entity ignored time, the abstract simulation required reference of the hardware. 2) Simple output entity Simple output entity only binding with the Q port without using I port, that means the simple output entities does not have a state transition diagram. Simple o

27、utput entity is the equipment that shows the work state of PLC, like a signal light. The usage of the simple output entity is to bind with the Q port such that the PLC can make its logical design.3) Human behavior entity Definition 2.2. A Human behavior entity is a tuple Env = , where Ienv is the I

28、port binding with the hardware entity, Qenv is the Q port binding with the entity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. Human behavior entity is similar with Ha

29、rdware entity; they have the same state definition. It is difficult to simulate the behavior of people, especially the design of a PLC to a number of individuals involved. In response to these difficulties, human behavior modeling should take an iterative process: First, a simple behavior model is b

30、uilt use the model validation; then, if not find a counter example, a more complex model is built, and validate, until find a counter-example or hard to be more complex; Finally, if not previously find a meaningful counter-ex-ample, then generate a completely random person behavior model (that is: h

31、uman behavior is a complete graph with all transfers be true) to verification. However, completely random behaviors verification will cause state space increases dramatically, so how to choose a suitable model of human behavior is the difficulty in modeling. If the persons input is relatively simple

32、, we can use completely random behavior modeling, otherwise, you need to seriously consider the establishment of a rational model of human behavior. We build model to PLC environment and the human behaviors above, and then we will model the PLC controller. PLC controller will be in a loop when it is

33、 turned on. PLC read all the input from I ports. PLC compute all the logic units. PLC set all the Q ports. PLC process on the basic unit called Network. All the networks will operate in order according to the number set when design. Basic logic operation network of PLC controller includes: S Trigger

34、, R Trigger, SR flip-flop, EQ trigger, RS flip-flop, POS rising edge detector, NEG falling edge detector and so on. To the basic logic operation network modeling, we use direct mapping strategy, namely: PLC controller model of network behavior and the logical behavior of the network is completely eq

35、uivalent. Where S trigger, R trigger, SR flip-flop, EQ trigger, RS flip-flop can directly use Boolean expressions to mapped to their behavior. 3. PLC Models Analysis and Improvement The previous section describes the modeling of a PLC system, according to this strategy; we can abstract a PLC system

36、as a formal model for model checking. Therefore, this model will have a direct decision of the credibility of the model checking results. If the model does not fully cover the original system (we call smaller than the original system), there may cause some errors are not detected; model can be compl

37、etely covered if the real system, but it contains many states that the original system does not exist (we call it larger than the original system), this may introduce some errors that real system do not exist. Here called it pseudo-error. So there are two requirements for modeling strategy. First, i

38、n order to find all the errors in the system, we shall build a model large enough to cover all the states in the original system; second, require the model be close to the real system as much as possible. This will not only reduce the state space, but also improve efficiency. Base on the requirement

39、s, we will give an analysis about the Time interval model. Proposition 1 If time interval model conforms the property, real PLC system model also conforms. The correctness of Proposition 1 can be concluded from the relationship between the two models. That means all the situations that real model wi

40、ll happen are included by the time interval model, time interval model is larger than the real model. If you couldnt find a counter-example by using a time interval model, you can prove the correctness of the real PLC model; the other hand, if we find a counter-example, we cannot determine whether t

41、here are errors in the real PLC system. That is to say the converse of proposition 1 is wrong. Then manual intervention is required to analyze the anti-cases to determine whether it is a pseudo-error. Time interval modeling strategy can get an abstract PLC model, many research based on NuSMV also us

42、e the strategy similar to time interval model to model PLC system. However, the “time interval model” has large deviation with the real model, it needs to be improved. The deviation is: “time interval model” does not reflect the high-speed scanning characteristics of PLC and low-speed characteristic

43、s of concurrent entities. That is, all the changes in the environment should be scanned by the high-speed PLC, but the time interval model ignores the high-speed characteristics of PLC, which makes changes in the external environment may not be scanned. To address the above issues, taking into accou

44、nt the external high-speed scanning and low-speed concurrent physical characteristics, time interval modeling strategy shall be improved by adding a notice-waiting mechanism. Base on the time interval model, each concurrent state entity must be blocked and wait after the transfer took place. Only if

45、 the PLC controller completely scans at least once, the notice-waiting mechanism will sent messages to concurrent entities to remove the block and go on working. Then the transfer finished. The process that concurrent entities work to complete the migration by notice-waiting mechanism is shown in Fi

46、gure 2: t0: Transfer start, block and notice the PLC controller. t1-tm: PLC completely scanned m times (m is one at least). tm+1: The concurrent entities get the notice from the PLC, transfer finish. This mechanism ensures every state change of concurrent entities can be scanned at least once by PLC

47、 controller. Proposition 2 After add the notice-waiting mechanism, the model become a subset of the time interval model. At the same time, the model can also include the entire situation in real model. That is to say, if a model which adds the notice-waiting mechanism conforms the property, real PLC

48、 system model also conforms. It is similar to prove proposition 2 with proposition 1. By proposition 2 we can see, after add the notice-waiting mechanism the model still has a good nature. As previously mentioned, an abstract system model has two requirements: first, to fully contain the real system, followed by the model as close to real systems. The first proposition is proved that the time interval model includes the r