Simulation and formal verification of industrial systems controllers

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 modelchecking 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 possible to eliminate a set of program errors in reduced intervals of time and that would not happen if these errors were detected only through the use of formal verification techniques. Conciliating these two techniques it can be substantially reduced the time necessary for the attainment of results through the use of the formal verification technique. For the analysis of a system control program for simulation and formal verification it is used the Dymola for the Simulation (through the creation of system models with Modelica language) and UPPAAL (through the creation of system models with timed automata).