Verificação formal de sistemas instrumentados de segurança na indústria de petróleo e gás natural

Abstract

Esta dissertação apresenta um método automatizável para verificação formal de programas de CLP integrada à metodologia de desenvolvimento de Sistemas Instrumentados de Segurança (SIS) na indústria de petróleo e gás. As especificações de segurança relacionando os diversos sensores e atuadores de SIS são padronizadas em Matrizes de Causa e Efeito (MCE), que são sistematicamente traduzidas em fórmulas LTL. São apresentadas regras para tradução do programa de CLP em diagrama Ladder para um modelo formal em linguagem intermediária FIACRE que serve de entrada para realização de model checking através da cadeia de verificação TINA/SELT. A fim de lidar com a complexidade dos modelos formais para SIS reais, apresenta-se um método baseado em cone de influência para decomposição do processo de model checking}e simplificação dos modelos em FIACRE. Os contraexemplos resultantes são convertidos em diagramas de sinal ou em comandos para o simulador do CLP, que facilitam a interpretação das falhas identificadas. O método foi aplicado para verificação de um caso ilustrativo e para partes do código do SIS de uma plataforma de petróleo offshore real. Os resultados mostram que o método é eficaz em detectar, quando existem, incongruências entre as especificações de segurança e a programação do CLP. Porém em sistemas com um número elevado de entradas e saídas uma única etapa de redução não é suficiente para diminuir a complexidade do sistema, ao ponto do mesmo ser processável por computadores comuns. Nestes casos uma segunda etapa de redução, baseada nas regras LTL, foi criada com intuito de verificar esses casos. Entretanto algumas propriedades não são possíveis de serem reduzidas, sendo assim alguns casos a propriedade não pode ser verificada por este método.

Abstract : This work presents an automated method of formal verification PLC programs integrated to Safety Instrumented Systems (SIS) development methodology applied to oil and gas industry. The safety specifications relating inputs and outputs are standardized by Cause and Effect Matrices (CEM), which are translated into LTL formulas. This work presents rules for translating PLC programs in Ladder diagrams to a formal model intermediate language called FIACRE that make the model checking through the TINA/SELT verification chain. To handle the complexity of real SIS formal models, it is presented a method based on cone of influence to breakdown the model checking process and simplify FIACRE models. The resulting counterexamples are converted in signal diagrams or in commands for the PLC simulator to make analysis easier. The method was applied to verify an illustrative PLC code of a real offshore oil platform. The results show that the method is effective in detecting inconsistencies between the safety specifications and PLC programming. However in systems with a high number of inputs and outputs a single reduction step is not enough to reduce the complexity of the system. Therefore, a second reduction step, based on LTL rules, was created with the purpose of verifying these cases.