Defesa de Dissertação de Mestrado – Luiz Paulo Enádio dos Reis – 15/02/2018
15/02/2018 17:13
| Defesa de Dissertação de Mestrado | ||
| Aluno | Luiz Paulo Enádio dos Reis | |
| Orientador
Coorientador |
Prof. Max Hering de Queiroz, Dr. – DAS/UFSC
Prof. Jean-Marie Alexandre Farines, Dr. – DAS/UFSC |
|
| Data | 15/02/2018 (quinta-feira) – 14h00
Sala PPGEAS I (piso superior) |
|
| Banca | Prof. Max Hering de Queiroz, Dr. – Presidente – DAS/UFSC;
Prof. Marcelo Lopes de Lima, Dr. – CENPES/Petrobras; Prof. Rodrigo Tacla Saad, Dr. – TREKKEN; Prof. Fábio Luis Baldissera, Dr. – DAS/UFSC. |
|
| Título | Verificação Formal de Sistemas Instrumentados de Segurança na Indústria de Petróleo e Gás Natural | |
| Resumo: O trabalho 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. | ||
