Autor(es):
Machado, José Mendes 
; Seabra, Eurico ; Campos, J. Creissac ; Oliveira, Filomena ; Leão, Celina Pinto
Data: 2008
Identificador Persistente: http://hdl.handle.net/1822/18403
Origem: RepositóriUM - Universidade do Minho
Assunto(s): Dependable systems; Safety control; Formal verification; Simulation; Timed systems
Descrição
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).
