Defesa de Dissertação de Mestrado – Günther Sgandella Klüsener – 30/9/2020
Defesa de Dissertação de Mestrado | |
Aluno | Günther Sgandella Klüsener |
Orientador | Prof. Max Hering de Queiroz, Dr. – DAS/UFSC |
Coorientador | Prof. Rodrigo Tacla Saad, Dr. – PPGEAS/UFSC
Prof. Fábio Luis Baldissera, Dr. – DAS/UFSC |
Data | 30/9/2020 (quarta-feira) – 9h
Videoconferência |
Banca |
Prof. Max Hering de Queiroz, Dr. – DAS/UFSC (presidente);
Prof. Marcelo Lopes de Lima, Dr. – CENPES/PETROBRAS; Prof. Eric Aislan Antonelo, Dr. – DAS/UFSC; Prof. Felipe Gomes de Oliveira Cabral, Dr. – DAS/UFSC. |
Título | Uso de Teste baseado em Aprendizagem para a Validação de Programas de CLP na Indústria de Petróleo e Gás Natural |
Resumo: A exploração de Petróleo e Gás Natural é uma atividade complexa e de alto risco. Por este motivo a segurança nesta indústria é organizada em camadas de proteção independentes e regidas por normas. Dentre estas camadas estão os Sistemas Instrumentados de Segurança (SIS), a última alternativa para a extinção de acidentes. Esse sistema automático, composto por um Controlador Lógico Programável (CLP), sensores e atuadores deve ser testado a fim de identificar falhas em sua lógica de atuação. Esta dissertação apresenta um método automático para teste de conformidade baseado em especificação utilizando princípios de aprendizagem computacional. Os casos de teste são gerados e testados no CLP iterativamente. O comportamento do CLP frente aos testes é modelado através do algoritmo de aprendizado a cada iteração. A partir das especificações de segurança descritas na forma de Matriz de Causa e Efeito, são extraídas fórmulas de lógica proposicional. Estas fórmulas são verificadas no modelo por um algoritmo de model checking. Eventualmente, contraexemplos serão encontrados, que podem ser inconformidades apenas do modelo ou também da lógica implementada no CLP. Os contraexemplos são executados como testes e o oráculo compara a saída do CLP com o modelo, fornecendo o veredicto a respeito da inconformidade. O algoritmo encerra sua execução ao encontrar uma falha no sistema ou por critério de parada. Esta técnica é aplicada a um modelo simplificado. A técnica proposta identificou a inconformidade contida no modelo simplificado, inconformidade esta não detectada através da execução do conjunto de testes gerados pelo método CEG-BOR. |