Simulation and formal verification of industrial systems controllers
José Machado, Eurico Augusto Rodrigues Seabra, José Creissac Campos, Filomena Soares, Celina P. Leão · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2008
Abstract. Actually, the safety control is one of the most important aspects studied by the international researchers, in the field of design and development of automated production systems due to social (avoid work accidents,...), economics (machine stop time reduction, increase of productivity,...) and technological aspects (less risks of damage of the components,...). Some researchers of the Engineering School of University of Minho are also studying these aspects of safety control, using simulation and model-checking techniques in the development of Programmable Logic Controllers (PLC) programs. The techniques currently used for the guarantee of automated production systems control safety are the Simulation and the Formal Verification. If the Simulation is faster to execute, has the limitation of considering only some system behavior evolution scenarios. Using Formal Verification it exists the advantage of testing all the possible system behavior evolution scenarios but, sometimes, it exists the limitation of the time necessary for the attainment of formal verification results. In this paper it is shown, as it is possible, and desirable, to conciliate these two techniques in the analysis of PLC programs. With the simultaneous use of these two techniques, the developed PLC programs are more robust and not subject to errors. It is desirable the use of simulation before using formal verification in the analysis of a system control program because with the simulation of some possible system behaviors it is