Defesa de Dissertação de Mestrado – Günther Sgandella Klüsener – 30/9/2020

14/10/2020 18:07
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

(https://meet.google.com/zdz-vdpn-rrk)

 

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.