Verificação formal de Sistemas Instrumentados de Segurança na indústria de petróleo e gás natural
LUIZ PAULO ENADIO DOS REIS1; Max Hering de Queiroz1; Jean-Marie Farines1; Marcelo Lopes de Lima2; Mario Cesar Mello Massa de Campos}2
1 Universidade Federal de Santa Catarina; 2 CENPES, Petrobras
Baixar PDF doi:10.20906/CPS/CBA2018-0788
Resumo
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 \textit{Ladder} para um modelo formal em linguagem intermediária FIACRE que serve de entrada para realização de \textit{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 \textit{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 \textit{offshore} real.
Palavras-chave: CLP; model checking; Sistema Instrumentado de Segurança; Verificação formal; Matriz Causa e Efeito,