Formal verification of PLC programs using the B method

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 PLCsPLCs (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 PLC