Several industrial standards address the development of the Programmable Logic Controller (PLC) which is included in theses systems in order to improve dependability and safety of critical automated systems. We can quote in particular the IEC 61508 standard that deals with functionality safety. This standard recommends formal methods using for the programmable devices of high Safety Integrated Level (SIL) systems. This explains why the companies which design logical controllers for critical systems are really interested in these methods and especially in formal verification by model checking.
However formal verification is not used at all during the development of industrial PLC programs up to now. Several reasons can explain this situation: difficulty for automation engineers to write formal properties in temporal logic, not understandable counterexamples, automatic translators absence to formal language in the PLC development environments, and, above all, too long, and even infinite, verification time, owing to the classical problem of state space explosion.
The goal of this work is to tackle out or to limit state space explosion by proposing a compact formal representation of the behavior of PLC programs. This representation is obtained by using two abstractions: data abstraction, which lessens the number of the variables which characterize each state and interpretation abstraction which reduces the number of states. In both cases, the abstract model will keep all the information that is useful for verification. The first result of this research, which were related to the number states reduction.
The next description on the context of this work: model checking of industrial programmable Logic Controller (PLC) programs. The principles which are retained for the construction of the formal model and to expose the method construction of this compact formal model from a PLC program will be described in another article. By these principles we will know the effectiveness of this formal representation.