Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/40178
Título: | Conversão sistemática do comportamento definido nos blocos funcionais da norma IEC 61 131-3 para autómatos finitos temporizados |
Outro(s) título(s): | Systematic conversion of the behaviour defined in the funtion blocks of IEC 61 131-3 standard to timed automata |
Autor(es): | Galvão, Joel Maurício Rocha |
Orientador(es): | Machado, José |
Palavras-chave: | Blocos funcionais da norma IEC 61 131-3 Simulação de sistemas automatizados Sistemas de eventos discretos Verificação formal Model-In-the-loop Model checking Autómatos finitos temporizados Sequential function chart UPPAAL IEC 61 131-3 function blocks Simulation of automation systems Discrete event systems Formal verification Timed automata |
Data: | 2015 |
Resumo(s): | Nesta dissertação é proposto um conjunto de modelos de alguns blocos funcionais da norma IEC 61
131-3 tendo em conta a Simulação e a verificação formal da especificação de comando de um sistema
mecatrónico. A modelação destes blocos funcionais é feita utilizando TA (Timed Automata) e o software
de simulação e verificação (UPPAAL), que permite simular e realizar model checking sobre modelos em
TA.
Todos os comportamentos dos blocos funcionais considerados relevantes foram transponíveis para
um modelo em autómatos finitos temporizados e foi possível tirar conclusões sobre a Simulação e
verificação formal do comportamento dos mesmos. Um estudo de caso foi considerado para ilustração
dos resultados obtidos e, também, permitiu extrapolar conclusões tiradas, para outros casos similares. In this dissertation, a series of models of same function blocks of the standard IEC 61 131-3 are proposed, taking into account the simulation and formal verification of the command specification of a mechatronic system. The modelling of these function blocks is done using TA and software of simulation and verification (UPPAAL) that allows the simulation and model checking of models in TA. The behavior of all the function blocks that were considered relevant were converted to TA models and it was possible to take conclusions about the simulation and formal verification of said models. A case study was considered to demonstrate the results obtained and also extrapolate the conclusions to other similar cases. |
Tipo: | Dissertação de mestrado |
Descrição: | Dissertação de mestrado integrado em Engenharia Mecânica |
URI: | https://hdl.handle.net/1822/40178 |
Acesso: | Acesso aberto |
Aparece nas coleções: | BUM - Dissertações de Mestrado DEM - Dissertações de Mestrado / MSc Thesis |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Dissertação_Joel Galvão_2015.pdf | 2,31 MB | Adobe PDF | Ver/Abrir |