Identificação de erros em programas de controle escritos em Ladder

Os sistemas produtivos (SPs) podem utilizar controladores program veis (CPs) como dispositivos de realiza o do controle. Neste contexto, programas de controle executados por CPs podem ser desenvolvidos de forma a n o estarem em conformidade com as especifica es de projeto, o que poder provocar o surgimento de erros funcionais associados execu o destes programas. Tais erros podem levar os SPs sob controle a situa es de acidentes. Esta quest o tem motivado o surgimento de diversas abordagens para identificar a exist ncia de erros em programas de controle de CPs, de forma a permitir a corre o dos mesmos, e garantir, consequentemente, maior confiabilidade operacional. Esta obra tem por objetivo ilustrar como identificar a exist ncia de erros em programas de controle baseados em linguagem Ladder (LD). Para isto, prop e-se um processo de cria o de modelos em M quinas de Estados Finitos Estendidas (MEFEs), que s o gerados a partir do mapeamento dos rungs contidos no programa de controle que se deseja identificar os erros. Uma vez desenvolvidos tais modelos, poss vel a utiliza o da ferramenta de model checking UPPAAL, a qual indicar a exist ncia (ou n o) destes erros.