The first criterion is to extent the scan cycles are modeled. Usually, a program on a PLC is executed cyclically. However when doing only static program analysis the cyclical execution is not interest: models have to take only a single execution of program into account. The most realistic way of modeling PLC is to build the cyclical execution into the model equipped with some real-time information about the duration of each cycle. In some cases, the precise duration of a scan cycle is not of interest, but the cyclic behavior is. Finally when the environment is much slower than the scan cycle length we can use models where program execution is instantaneously. PLCs are embedded systems, and correctness of such system concerns the interaction between a controller and its environment. Therefore, a composition of two models has to be analyzed: one models the PLC with its program and one models the environment. The different ways of modeling scan cycles characterize the abstraction levels on which environment and PLC are composed.
Models without scan cycle
Program models that do not consider the scan cycle are intended mainly for static program analysis. They are not composed together with an environmental model. The models typically do not include real time. The properties that can be investigated based on such models are e.g. data independence between parallel components, unreachable code, safe structure of programs, etc. it can be checked whether a program conforms to some programming guidelines. It is reasonable to restrict formal analysis only to well constructed program, e.g. not every syntactically correct program, but programs using a certain programming discipline.
Models with explicit scan cycle
Generally, for each program execution there are a lower and an upper time bound. The lower time bound results from the time needed for update an output and input and the self checks of the operation system. The upper time bound depends on the longest execution path in the program. Under the assumptions it is important that we don’t consider interrupts, they make it difficult to predict a scan cycle duration.