Industrial programs written on Programmable Logic Controllers (PLCs) have become an essential component of many modern industries, including automotive, aerospace, manufacturing, infrastructure, and even amusement parks. As these safety-critical systems become larger and more complex, ensuring their continuous error-free operation has become a significant and important challenge. Formal methods are a potential solution to this issue but have traditionally required substantial time and expertise to deploy. This usability issue is compounded by the fact that PLCs are highly proprietary and have substantial licensing costs, making it difficult to learn about or deploy formal methods on them. This thesis presents the OPPP (Open-source Proving of PLC Programs) system as a solution to this usability issue. The OPPP system allows the end-to-end creation and verification of PLC programs from within the development environment. The system is created with an emphasis on being easy to use, with formal constraints presented in English phrases that require no special knowledge to understand. The system uses entirely open-source components, including modified versions of both the OpenPLC development environment and the PLCverif verification platform. The OPPP system is then demonstrated to formalize the requirements of two college-level introductory PLC programming problems. It is further demonstrated to correctly find errors in and verify the correctness of a known good and known bad solution to each problem.

This master thesis deals with the design of a wastewater treatment plant, which will be controlled by a PLC. The theoretical part describes the types of wastewater and sewage systems that are important in the design of wastewater treatment plants. The thesis also describes programmable logic controllers, theirs programming languages, SCADA (Supervisory Control And Data Acquisition) systems and automation.The thesis also deals with theoretical description of wastewater treatment plants, their functions and security. Next part describes the design of the wastewater treatment plant. The last part of the thesis describes implementation of the wastewater treatment plant controlled by a PLC.

The aim of this diploma thesis is detail description of theory, design process and final realization of single-purpose machine for pressing canister funnels. Theoretical section of this work covers manufacturing standards of the electrical cabinets, options for the single-purpose machine control with focus on the programmable logic controller e.g. PLC, PLC control program concept with definition of the main alarm states and description of two types of electrical cabinet. Practical part contains description of the electrical cabinet, its block diagram, photo documentation of the wiring (chapter 4.), chosen PLC type, its advantages and detail program description using Ladder diagram notation, communication with operator realized with touch LCD panel, programming environment for this LCD panel and program realization process. Finalized machine description and its photo documentation in manufacturing process is covered in the end. This diploma thesis is based and extends previously successfully defended semester project.

Made available in DSpace on 2016-12-12T17:38:31Z (GMT). No. of bitstreams: 1 SUZANA RIBAS DE ALMEIDA.pdf: 2655112 bytes, checksum: 346dca905796b24136deb70b7263fb5b (MD5) Previous issue date: 2012-02-15 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Nowadays the competition between companies is increasing. In a production system, efficiency, speed and flexibility are important means for cost reductions. The complexity of automation systems has been increasing, which makes necessary the implementation of more efficient control programs, free of errors and easy to maintain. However, in most practical applications the solution of these problems is dependent on designer's experience and doesn t follow a formal methodology, which results in programs with errors and difficulties to understand and maintain, since only the designer understands the adopted solutions. The Supervisory Control Theory (SCT) is a method extensively researched in academic circles for the synthesis of control logic of automated systems. It allows control problems to be solved in a formal way, ensuring a minimally restrictive and no blocking solution that meets the control specifications. However, this theory is not widely used in industrial environments yet, once the methods for implementation of supervisors obtained by TCS are still deficient. Thus, the intention of this Dissertation consists of showing a methodology for implementation of supervisory control in Programmable Logic Controllers (PLCs). In this work, the synthesis of supervisors is made in accordance to local modular approach, which brings the benefits of a formal methodology and allows exploring the modularity of the plant and the control specifications. The implementation is based on an architecture structured in three levels: supervisor, interface and system to be controlled. For the implementation in CLP three different programming languages are applied: the high-level languages Sequential Function Charts (SFC) and Structured Text and the low-level Ladder Diagram language in some parts. The development of the methodology was based on two works: a doctoral thesis by Vieira (2007) and master thesis by Cruz (2011) and brought together the advantages presented in each one of these. To compare the proposed methodology and the two mentioned methods, several tests were made on a manufacturing cell available at PUCPR and simulations on a PLC and computer as well. The results show that the use of the methodology proposed in this work makes possible to implement PLC programs that are able to treat all non-controllable events occurred in the system to be controlled and treat one controllable event by each control cell in the same scan cycle. Furthermore, the use of high-level languages results in a program of easier interpretation and maintenance, also enabling reutilization of codes. In this work some problems related to CLPs implementations are also showed and proposals for solving them are presented, as properties as well that, if accepted, ensure that the problem does not occur. / Hoje em dia a competitividade entre as empresas está cada vez maior. Em um sistema de produção, a eficácia, a velocidade e a flexibilidade são importantes, pois significam redução de custos. Os sistemas de automação atuais estão cada vez mais complexos, justificando a necessidade de programas de controle mais eficientes, sem erros e de fácil manutenção. Entretanto, na maioria das aplicações práticas a solução destes problemas é feita com base na experiência do projetista, não seguindo uma metodologia formal, o que resulta em programas com erros e de difícil entendimento e manutenção, uma vez que só o projetista entende perfeitamente as soluções adotadas. A Teoria de Controle Supervisório (TCS) é um método para a síntese da lógica de controle de sistemas automatizados. Ela permite que problemas de controle sejam solucionados de modo formal, garantindo uma solução minimamente restritiva e não bloqueante e que atenda às especificações de controle. Entretanto, esta teoria ainda não é amplamente adotada em ambientes industriais, sendo a carência de métodos de implementação dos supervisores obtidos via TCS um elemento que contribui para que isso aconteça. Assim, esta dissertação se propõe a apresentar uma metodologia de implementação de controle supervisório em Controladores Lógicos Programáveis (CLPs). Neste trabalho, a síntese de supervisores é feita de acordo com a abordagem modular local, que traz os benefícios de uma metodologia formal e ainda permite explorar a modularidade da planta e das especificações de controle. A implementação é baseada numa arquitetura estruturada em três níveis: supervisor, interface e sistema a ser controlado. Para a implementação em CLP são empregadas três linguagens distintas de programação, as linguagens de alto nível Sequential Function Charts (SFC) e Structured Text, bem como a linguagem Ladder Diagram em algumas partes. O desenvolvimento da metodologia foi baseado em dois trabalhos: a tese de doutorado de Vieira (2007) e a dissertação de mestrado de Cruz (2011) e permitiu reunir as vantagens apresentadas em cada um destes. Para comparação entre a metodologia proposta e as duas metodologias citadas, foram feitos diversos testes em uma célula de manufatura existente na PUCPR, bem como simulações em CLP e em computador. Os resultados mostram que a metodologia proposta neste trabalho permite a implementação de programas em CLP que, num mesmo ciclo de varredura, são capazes de tratar todos os eventos não controláveis ocorridos na planta e ainda um evento controlável por célula de controle. Além disso, o uso de linguagens de alto nível resulta em um programa de mais fácil interpretação e manutenção, possibilitando ainda o reaproveitamento de códigos. Nesta dissertação também são abordados alguns problemas de implementação da estrutura de controle supervisório em CLPs, apresentando-se propostas para solucioná-los, bem como propriedades que, se atendidas, garantem que o problema não ocorra.