@conference {MachadoSCSLS:2007,
	title = {Simulation and Formal Verification of Industrial Systems Controllers},
	booktitle = {19th International Congress of Mechanical Engineering - COBEM},
	year = {2007},
	month = {November },
	publisher = {ABCM},
	organization = {ABCM},
	address = {Bras{\'\i}lia, Brazil},
	abstract = {<p>Actually, the safety control is one of the most important aspects studied by the international researchers, in the field of<br />
 design and development of automated production systems due to social (avoid work accidents, ...), economics (machine stop time<br />
 reduction, increase of productivity,...) and technological aspects (less risks of damage of the components,...). Some researchers of<br />
 the Engineering School of University of Minho are also studying these aspects of safety control, using simulation and modelchecking<br />
 techniques in the development of Programmable Logic Controllers (PLC) programs.<br />
 The techniques currently used for the guarantee of automated production systems control safety are the Simulation and the Formal<br />
 Verification. If the Simulation is faster to execute, has the limitation of considering only some system behavior evolution scenarios.<br />
 Using Formal Verification it exists the advantage of testing all the possible system behavior evolution scenarios but, sometimes, it<br />
 exists the limitation of the time necessary for the attainment of formal verification results. In this paper it is shown, as it is possible,<br />
 and desirable, to conciliate these two techniques in the analysis of PLC programs. With the simultaneous use of these two<br />
 techniques, the developed PLC programs are more robust and not subject to errors. It is desirable the use of simulation before using<br />
 formal verification in the analysis of a system control program because with the simulation of some possible system behaviors it is<br />
 possible to eliminate a set of program errors in reduced intervals of time and that would not happen if these errors were detected<br />
 only through the use of formal verification techniques. Conciliating these two techniques it can be substantially reduced the time<br />
 necessary for the attainment of results through the use of the formal verification technique.<br />
 For the analysis of a system control program for simulation and formal verification it is used the Dymola for the Simulation<br />
 (through the creation of system models with Modelica language) and UPPAAL (through the creation of system models with timed<br />
 automata).</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jccampos/files/publicacao_-_ssm3_iii_09_-_publicado_em_2008.pdf},
	author = {J. Machado and E. Seabra and Jos{\'e} Creissac Campos and F. Soares and C. Le{\~a}o and J.F. Silva}
}