Please use this identifier to cite or link to this item:

TitleSimulation and formal verification of industrial systems controllers
Author(s)Machado, José Mendes
Seabra, Eurico
Campos, J. Creissac
Soares, Filomena
Leão, Celina Pinto
KeywordsDependable systems
Safety control
Formal verification
Timed systems
Issue date2008
PublisherAssociação Brasileira de Engenharia e Ciências Mecânicas (ABCM)
Abstract(s)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).
TypeConference paper
AccessOpen access
Appears in Collections:HASLab - Artigos em atas de conferências internacionais (texto completo)
DEM - Artigos em revistas de circulação internacional com arbitragem científica

Files in This Item:
File Description SizeFormat 
PUBLICAÇÃO - SSM3_III_09 - PUBLICADO EM 2008.pdf332,54 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID