VERIFICAÇÃO FORMAL DE SISTEMAS INSTRUMENTADOS DE SEGURANÇA NA INDÚSTRIA DE PETRÓLEO E GÁS NATURAL

Abstract

Este trabalho apresenta um método automatizável para verificação formal de programas de CLP integrado à 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 do código do SIS de uma plataforma de petróleo offshore real.