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 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 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 entities.

1) 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 decided 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 Ienvs the I port binding with the hardware entity, Qenvis 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 s0is 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}, he 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 transition diagram of hardware entities also need to specify an initial state, the transitions graph starts from this state. The hardware entities’ statesof transition diagram are based on the division of symbol I, and time properties are not taken into account. Hardware entities state transition diagram is 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 output 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

59

that the PLC can make its logical design. 3) Human behavior entity

Definition 2.2.A Human behavior entity is a tuple Env = < Ienv, A>, where Ienv is the I 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 Hardware 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 built 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-example, then generate a completely random person behavior model (that is: human behavior is a complete graph with all transfers be true) to verification. However, completely random behavior’s verification will cause state space increases dramatically, sohow to choose a suitable model of human behavior is the difficulty in modeling. If he person's input is relatively simple, 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 turned on.

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, 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 equivalent. Where Strigger, R trigger, SR flip-flop, EQ trigger, RS flip-flop can directly use Boolean expressions to mapped to their behavior.

60

3. PLC Model’s Analysis and Improvement

The previous section describes the modeling of a PLC system, according to this strategy; we can abstract a PLC system 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 completely 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, in 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 requirements, 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 thatreal model will happen are included by the time interval model, time interval model is larger than the real model. If you couldn’t find acounter-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 there 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 use 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 characteristics 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 account the external high-speed scanning and low-speed concurrent physical characteristics, time

61

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 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 Figure 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 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 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 real systems, as long as the use of model checking tools to prove that this abstract model satisfies a certain property, then the true nature of the system will also satisfy this. But this model and the real model is not entirely equal, it should be far greater than the real model. Compare to time interval model, this model further reduced the distance between the real systems, greatly reduce the chance that finding out pseudo-errors. Model checking tool will give out a counter-example violate the property of the system; it is easy to manually determine the counter-examples in the real system is true or not. If the errors in the original system really exist, then we find a counter-example. Otherwise, this error is because the abstract model is larger than the real system, it is a pseudo-error. Therefore, although this time interval model and the original system are not fully equivalent, but by this model, we can judge a system meets a certain property, if not we can finda specific counter-example (still needs more examine to determine whether it is a pseudo-error). Model is not equivalent with the original system, mainly because there are many factors difficult to model in real systems, some of which may give rise to error. If all the factors are modeled, that will lead to the establishment of a huge model

62

that cannot check, or simply cannot be achieved. Time interval model abstract the key factors from the real system and model them, greatly reducing the state space, and reduce the time complexity. Meanwhile, add by the notice-waiting mechanism, the model become much closer to real systems, not only reduces the time complexity, while it reduced the pseudo-errors mentioned before.

4.PLC Model Checking

PLC is widely used in many applications, and has many devices; this is a large area of research. Any PLC work in the environment that includes different equipment and people, so PLC system is concurrent. At the same time, a PLC system difficult to find if there are some errors, mostly because of the logicaldesign errors, but not the calculation error. So we focus on the detection of PLC program logic process, and this logic can be completely escribed by bit logic. Therefore, in order to simplify the PLC program model, focused on model checking, we make the following settings: PLC is a logic control program, all the control variables only has two states 0 and 1; PLC program is run in concurrent environment. In this case, PLC programming is more likely to have ome errors not easy to find. In respect of the above characteristics, we use the model checking tool SPIN (our tools PLC-Checker also Copyright ? 2010 SciRes. JSEA PLC Modeling and Checking Based on Formal Method 1058 realized NuSMV) on the above established model for checking. We made a series of transformation rules, build the above model into SPIN's input language Promela, the system property also need to be translated into Promela, SPIN will put them together and then perform detection. PROMELA language is a C class language, they are similar in semantic. So we will only give some examples to show the basic concept of the translation. To see the details of PROMELA language, please visit www.spinroot.com. We will introduce the three part of a PROMELA file as the input of SPIN. 1) Code of PLC controller PLC controller is composed of multiple networks. Code of PLC controller is also generated from the network. Of course, before that, you should declare the variables you need. Each network has its input ports and output ports, each port can be indicate by a Boolean expression. We assign the output port’s value through the logic computing of all the input port. This is the translation approach of PLC network. Here is an example of converting SR network:

2) Code of concurrent entities We consider each concurrent entity a unique process,

63