Banca de QUALIFICAÇÃO: HANIEL MOREIRA BARBOSA
Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE: HANIEL MOREIRA BARBOSA
DATA: 06/08/2012
HORA: 10:00
LOCAL: DIMAp
TÍTULO:
Formal verification of PLC programs using the B Method
PALAVRAS-CHAVES:
PLC, IEC 61131-3, Método B, métodos formais, sistemas críticos.
PÁGINAS: 60
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:
Controladores Lógico Programáveis (PLCs - \emph{Programmable Logic Controllers}, em inglês)
desempenham funções de controle, recebendo informações do ambiente, processando-as e modificando este
ambiente de acordo com os resultados obtidos. São comumente utilizados na indústria nas mais diversas
aplicações, do transporte de massa a fábricas de bebidas. Com o crescente aumento da complexidade dessas
aplicações e do seu uso em sistemas críticos, faz-se necessária uma forma de verificação que propicie mais
confiança do que testes e simulação, padrões mais utilizados na indústria, mas que podem deixar falhas não
tratadas. Métodos formais podem prover maior segurança a este tipo de sistema, uma vez que permitem a sua
verificação matemática. Neste trabalho fazemos uso do Método B, que é usado com sucesso na indústria na
verificação de sistemas críticos, possui amplo apoio ferramental e suporte
a decomposição, refinamento e verificação de corretude em relação à especificação através de obrigações de
prova. O método desenvolvido e apresentado aqui consiste em gerar automaticamente modelos B a partir de programas para PLCs e verificá-los formalmente em relação a propriedades de segurança, estas derivadas manualmente a partir dos requisitos do sistema. O escopo do trabalho são as linguagens de programação para PLCs do padrão IEC 61131-3, mas sistemas com linguagens que apresentem modificações em relação ao padrão também são suportados. Esta abordagem visa facilitar a integração de métodos formais na indústria através da diminuição do esforço
para realizar a verificação formal de PLCs.
MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1694485 - MARCIO EDUARDO KREUTZ