Simulation and formal verification of industrial systems controllers

摘要

Actually, the safety control is one of the most important aspects studied by the international researchers, in the field ofdesign and development of automated production systems due to social (avoid work accidents, ...), economics (machine stop timereduction, increase of productivity,...) and technological aspects (less risks of damage of the components,...). Some researchers ofthe Engineering School of University of Minho are also studying these aspects of safety control, using simulation and modelcheckingtechniques 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 FormalVerification. 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, itexists 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 twotechniques, the developed PLC programs are more robust and not subject to errors. It is desirable the use of simulation before usingformal verification in the analysis of a system control program because with the simulation of some possible system behaviors it ispossible to eliminate a set of program errors in reduced intervals of time and that would not happen if these errors were detectedonly through the use of formal verification techniques. Conciliating these two techniques it can be substantially reduced the timenecessary 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 timedautomata).