Please use this identifier to cite or link to this item: http://hdl.handle.net/1843/RAOA-BCDHWT
Type: Dissertação de Mestrado
Title: Verificação automática de sistemas descritos usando a linguagem Ladder
Authors: Alba Francine de Souza Caetano
First Advisor: Alair Dias Junior
First Referee: Diogenes Cecilio da Silva Junior
Second Referee: Ricardo de Oliveira Duarte
Abstract: Os Controladores Lógicos Programáveis (CLP) foram introduzidos na década de 1960 para realizar a modernização e manutenção do controle, sequenciamento e lógica de intertravamento das plantas industriais e, desde então, tornaram-se indispensáveis na automação e controle industrial. Um CLP é um computador digital construído para operar em ambientes industriais adversos e projetado para ser facilmente operado por equipes de manutenção. Por isso, oferece um conjunto de linguagens de programação direcionadas a esses profissionais. Uma dessas linguagens é a Ladder Diagram (LD), que é baseada na lógica de relés e ainda é uma das linguagens de programação de CLP mais usadas. A verificação dos programas de CLP é imprescindível para garantir a operação segura de plantas industriais e vários trabalhos abordaram esse assunto na literatura. No entanto, os métodos disponíveis para verificação de LD usualmente empregam uma abordagem de modelagem ingênua, não levando em conta a ordem de execução das rungs. Além disso, a maioria deles se concentra apenas nas operações booleanas, que são um subconjunto dos possíveis comandos disponíveis no LD. Este trabalho aborda esses dois problemas, fornecendo uma metodologia completa para traduzir automaticamente programas em Ladder para o NuSMV. A metodologia foi validada com relação à ordem de execução usando exemplos construídos e também construiu-se uma ferramenta para traduzir programas em LD exportado de um CLP amplamente utilizado na indústria para o NuSMV.
Abstract: Programmable Logic Controllers (PLC) were introduced in the 1960s to support modernization and maintenance of control, sequencing and interlocking logic of industrial plants and, since then, they became indispensable in industrial automation and control. A PLC is a digital computer built to operate in harsh industrial environments and designed to be easily operated by maintenance teams. Hence, it offers a set of programming languages directed to these professionals. One of such languages is the Ladder Diagram (LD), which is based on relay logic and still is one of the most used PLC programming languages. Verifying PLC programs is imperative to guaranteeing the safe operation of industrial plants and several works have addressed this issue in the literature. However, available methods for verification of LD usually employs a naive modelling approach, not taking into account the execution order of the rungs, which are program lines in LD. Besides, most of them focus only on Boolean operations, which are a subset of the possible commands available in LD. This work addresses both these issues, providing a complete methodology for translating Ladder Diagrams to NuSMV, which is the formal language. We validated the methodology with respect to execution order using constructed examples and also built a tool to translate LD exported from a PLC suite largely used in industry to NuSMV.
Subject: Engenharia elétrica
Automação
language: Português
Publisher: Universidade Federal de Minas Gerais
Publisher Initials: UFMG
Rights: Acesso Aberto
URI: http://hdl.handle.net/1843/RAOA-BCDHWT
Issue Date: 14-Dec-2018
Appears in Collections:Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
verificac_a_o_automa_tica_de_sistemas_descritos_usando_a_linguagem_ladder.pdf2.05 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.