Publisher's Synopsis
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.
