Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs

Automation and cybernetics: Control of a flexible one-link manipulator

States that control is of the essence in cybernetics. Summarizes the dynamic equations for a flexible one-link manipulator moving in the horizontal plane. Employs the finite element method, based on elementary beam theory, during the process of formulation. Develops and instruments a one-link flexible manipulator in order to control its vibration modes. Uses a simple second-order vibration model which permits vibrations on the rod to be estimated using the hub angle. The validation of the dynamic model and the structural analysis of the flexible manipulator is reached using proper infrared cameras and active light sources for determining actual positions of objects in space. Shows that the performance of the control is satisfactory, even under perturbation action.

IEEE 1451-based multi-interface module (I2M) for industrial processes automation

This paper describes the implementation of a multi-interface module (I2M) for automation of industrial processes, based on the IEEE1451 standard. Process automation with I2M can communicate through either wires or using wireless communication, without any hardware or software changes. We used FPGA resources to implement the I2M functions FPGA, with a NIOS II processor and ZigBee communication system (IEEE802.15), as well as RS232 serial standard. Part of the project was done in the SOPC Builder environment, which gave the designer flexibility and speed to implement the NIOS II-based microprocessor system. To test the I2M implementation, a didactic Industrial Hydraulic Module (MHI-01) was used to simulate two industrial processes to be controlled by the system proposed.

Automation in fault detection using neural network and model updating

In this article, an implementation of structural health monitoring process automation based on vibration measurements is proposed. The work presents an alternative approach which intent is to exploit the capability of model updating techniques associated to neural networks to be used in a process of automation of fault detection. The updating procedure supplies a reliable model which permits to simulate any damage condition in order to establish direct correlation between faults and deviation in the response of the model. The ability of the neural networks to recognize, at known signature, changes in the actual data of a model in real time are explored to investigate changes of the actual operation conditions of the system. The learning of the network is performed using a compressed spectrum signal created for each specific type of fault. Different fault conditions for a frame structure are evaluated using simulated data as well as measured experimental data.

An efficient methodological approach in the didatic of automation applied to integrated manufacturing

This work presents challenges and solutions for the teaching and learning of automation applied to integrated manufacturing by means of a methodological approach based on techniques, tools and industrial equipment directly applicable in the industry. The approach was implemented in a control and automation engineering course divided into expositive and laboratory classes. Since the success of the approach is mainly from the practical activities, the article focus more on activities developed in laboratory than theorical classes. Copyright © 2007 IFAC.

Digital system design process automation using place/transition petri nets

The constant increase in digital systems complexity definitely demands the automation of the corresponding synthesis process. This paper presents a computational environment designed to produce both software and hardware implementations of a system. The tool for code generation has been named ACG8051. As for the hardware synthesis there has been produced a larger environment consisting of four programs, namely: PIPE2TAB, AGPS, TABELA, and TAB2VHDL. ACG8051 and PIPE2TAB use place/transition net descriptions from PIPE as inputs. ACG8051 is aimed at generating assembly code for the 8051 micro-controller. PIPE2TAB produces a tabular version of a Mealy type finite state machine of the system, its output is fed into AGPS that is used for state allocation. The resulting digital system is then input to TABELA, which minimizes control functions and outputs of the digital system. Finally, the output generated by TABELA is fed to TAB2VHDL that produces a VHDL description of the system at the register transfer level. Thus, we present here a set of tools designed to take a high-level description of a digital system, represented by a place/transition net, and produces as output both an assembly code that can be immediately run on an 8051 micro-controller, and a VHDL description that can be used to directly implement the hardware parts either on an FPGA or as an ASIC.

Notes on microelectronic automation in Brazil

Includes bibliography

Desenvolvimento de um sistema de controle para avaliação de fontes de energias renováveis no bombeamento de água

Pós-graduação em Agronomia (Energia na Agricultura) - FCA

Provendo soluções de comunicação em ambientes industriais inóspitos via PLC - um estudo de caso aplicado a uma empilhadeira de bauxita da refinaria da Alunorte

Este trabalho tem como principal objetivo fazer um estudo sobre um sistema comunicação de dados, utilizando-se a rede elétrica existente entre equipamentos, como meio físico em um ambiente industrial inóspito. Nesse caso, foi implementado um piloto em uma refinaria de alumina, localizada em Barcarena no estado do Pará, em uma máquina móvel de empilhamento de bauxita, que possuía um sistema de comunicação de dados via rádio, no qual ocorriam muitas falhas de comunicação devido às interferências eletromagnéticas, RFI, etc. prejudicando o processo de produção da refinaria. Como alternativa, apresentar-se-á uma tecnologia menos susceptível a problema da interferência que permite melhorar o desempenho do sistema de comunicação entre equipamentos. Trata-se da tecnologia PLC - Power Line Communication- que é full-duplex e utiliza modulação OFDM, o que reduz o efeito indesejável de interferências. Na conclusão, foram feitos comentários pertinentes aos resultados obtidos e os esperados acerca da confiabilidade da tecnologia, bem como sua utilização para futuras aplicações, nas diversas áreas onde a mesma pode ser utilizada.

Análise e desempenho de tráfego triple play em redes PLC de baixa tensão

Este trabalho faz uma análise de desempenho de aplicações triple play através da tecnologia Power Line Communication, fazendo uma abordagem direcionada para qualidade de serviço e qualidade de experiência. Apresenta resultados obtidos em cenários residenciais onde o uso desta tecnologia como última milha mostra-se uma solução passível de implementação diante dos testes realizados com transmissões de chamadas VoIP, transmissões de vídeo em alta definição e dados. O conceito de rede doméstica, interligando todos os pontos de uma casa, vem representando um novo rumo na definição de um padrão global, no qual a transmissão de dados por meio da fiação elétrica será uma das tecnologias empregadas e de maior destaque. Também será mostrado o desempenho das métricas avaliadas como jitter, largura de banda, perda de pacotes, PSNR, MOS, VQM, SSIM e suas correlações.

Sistema de controle baseado em lógica fuzzy para regulagem de temperatura em aquecedor de óleo térmico da planta de anodo verde da Albrás

Neste trabalho são apresentados os resultados de uma técnica que permitiu implementar a estratégia de controle de temperatura do aquecedor de óleo térmico da fabrica de Anodo Verde da Albrás Alumínio Brasileiro S/A. No projeto utilizou-se um sistema hierarquizado baseado em conjuntos e lógica Fuzzy. O uso dessa metodologia fez com que o sistema fosse capaz de reagir adequadamente diante das variações do ponto de operação do aquecedor, pois o controle Fuzzy exibe algumas características do aprendizado humano, sendo considerado um exemplo de inteligência artificial. O aquecedor de óleo térmico é fundamental no processo de fabricação de blocos inódicos, utilizados como pólo positivo no processo de eletrólise na obtenção do alumínio primário. O sistema de óleo térmico aquece os misturadores e pré-aquecedor de coque, mantendo a temperatura desses equipamentos dentro dos limites estabelecidos pela engenharia de processo. A variável temperatura impacta diretamente na energia de mistura da pasta e na qualidade do produto final, que é o bloco anódico. A metodologia apresentada permitiu alcançar um controle de temperatura que atendeu satisfatoriamente os parâmetros de processo. O programa foi desenvolvido em linguagem ladder é executado em controladores lógicos programáveis (CLP’S) da Rockwell Automation. O controle já está em plena operação nas fábricas de anodos e os resultados obtidos demonstram a eficácia e viabilidade do sistema, que futuramente estará sendo implementado no controle de outros equipamentos da Albrás.

Desenvolvimento de experiências de acionamento e controle do movimento angular de motores de indução trifásico

This paper aims to show practical and effectiveexperiencesfor lessons Industrial Automation Laboratory taught inundergraduate degreein ElectricalEngineering from the University Júlio MesquitaFilho - UNESP, Guaratinguetá. Experiments carriedsimulatecontrol and drive systems of electric three phase induction motors (MIT)widely usedinindustries. The experiments simulate a manufacturing environment where there isa need to control the activation and continuous operation ofelectricmotors. Seven experimentsthat simulatethe firing of electrical motors through a controlsystem, a driver along with asimulator loads coupled to the electric motor was developed. Experiments usinga Programmable Logic Controller (PLC) as acontroller,an inverter frequencyasdriver, and MagneticBrake, as simulatorengine loads . The experiments were divided accordingto the speed reference signal used fordrivingand operating the electric motor: digital and analog. The first five experiments performing the drive control and operation of the electric motor via digital signals. The sixth and seventh experiments using an analog signal as a reference speed for the electric motor

Alocação de modem PLC utilizando SNR em uma rede elétrica de baixa tensão

Pós-graduação em Engenharia Elétrica - FEIS