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
Notícia cadastrada em: 17/08/2012 15:15
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa06-producao.info.ufrn.br.sigaa06-producao