Systematic conversion of the behaviour defined in the funtion blocks of IEC 61 131-3 standard to timed automata

Dissertação de mestrado integrado em Engenharia MecânicaNesta 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