Modelagem de programas e sua verificação para controladores programáveis.

• Ano de defesa: 2008
• Autor(a) principal: Sarmento, Cleber Alves
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Biblioteca Digitais de Teses e Dissertações da USP
• Palavras-chave em Português: Controladores programáveis; Linguagem de programação; Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs); Modeling and verification of extended finite state machines (EFSM); Programmable logic controllers; Programming language
• Link de acesso: http://www.teses.usp.br/teses/disponiveis/3/3152/tde-02042008-120021/

Os sistemas produtivos (SPs) podem utilizar controladores programáveis (CPs) como dispositivos de realização do controle. Neste contexto, programas de controle executados por estes CPs podem ser desenvolvidos de forma que não estejam em conformidade com as especificações de projeto, o que poderá provocar o surgimento de erros funcionais associados à execução de tais programas de controle, erros estes que podem levar os SPs sob controle a um estado que poderá implicar em acidentes envolvendo equipamentos, pessoas e o meio-ambiente. 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 destes erros e garantir, conseqüentemente, maior confiabilidade operacional. O presente trabalho tem por objetivo identificar a existência de erros em programas de controle baseados em LD (Ladder Diagram). Para isto, propõe-se um procedimento de desenvolvimento de modelos baseados em máquinas de estados finitos estendidas (MEFEs), que são gerados a partir do mapeamento de cada um dos rungs contidos no programa de controle que se deseja identificar erros. Uma vez desenvolvidos os modelos em MEFEs, torna-se possível a utilização de uma ferramenta computacional de verificação, própria para estabelecer se os modelos verificados satisfazem determinadas proposições estabelecidas em lógica temporal. Uma proposição em lógica temporal está relacionada a um estado específico do programa de controle modelado, sendo que o objetivo da verificação é o de estabelecer se a proposição estipulada é atendida ou não. Se um determinado estado específico for, por exemplo, um estado indesejado do programa de controle modelado, e este estado for possível de ser alcançado como resultado do processo de verificação realizado, isto impactará na não conformidade do programa de controle com as especificações comportamentais estipuladas na forma de proposição em lógica temporal, indicando haver, portanto, um erro neste programa de controle modelado. Palavras-chave: Controladores programáveis. Linguagem de programação LD. Modelagem e verificação de máquinas de estados finitos estendidas (MEFEs).