Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/jspui/handle/123456789/18061
Title: Formal verification of PLC programs using the B Method
Other Titles: Formal verification of PLC programs using the B method
Authors: Barbosa, Haniel Moreira
Keywords: PLC. IEC 61131-3. Método B. Métodos formais. Sistemas críticos;PLC. IEC 61131-3. B method. Formal methods. Safety critical systems
Issue Date: 1-Nov-2012
Publisher: Universidade Federal do Rio Grande do Norte
Citation: BARBOSA, Haniel Moreira. Formal verification of PLC programs using the B method. 2012. 177 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2012.
Portuguese Abstract: Controladores Lógico Programáveis (PLCs Programmable Logic Controllers, em inglês) desempenham funções de controle, recebendo informações do ambiente, processando-as e modificando este ambiente de acordo com os resultados obtidos. São comumente utilizados na indústria nas mais diversas aplicações, do transporte de massa à indústria do petróleo, gás e energias renováveis. Com o crescente aumento da complexidade dessas aplicações e do seu uso em sistemas críticos, faz-se necessária uma forma de verificação que propicie mais confiança do que testes e simulação, padrões mais utilizados na indústria, mas que podem deixar falhas não tratadas. Métodos formais podem prover maior segurança a este tipo de sistema, uma vez que permitem a sua verificação matemática. Neste trabalho fazemos uso do Método B, que é usado com sucesso na indústria para a verificação de sistemas críticos, possui amplo apoio ferramental e suporte à decomposição, refinamento e verificação de corretude em relação à especificação através de obrigações de prova. O método desenvolvido e apresentado aqui consiste em gerar automaticamente modelos B a partir de programas para PLCs e verificá-los formalmente em relação a propriedades de segurança, estas derivadas manualmente a partir dos requisitos do sistema. O escopo do trabalho são as linguagens de programação para PLCs do padrão IEC 61131-3, mas sistemas com linguagens que apresentem modificações em relação ao padrão também são suportados. Esta abordagem visa facilitar a integração de métodos formais na indústria através da diminuição do esforço para realizar a verificação formal de PLCs
Abstract: 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
URI: https://repositorio.ufrn.br/jspui/handle/123456789/18061
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
HanielMB_DISSERT.pdf4,81 MBAdobe PDFThumbnail
View/Open


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