Navegando por Autor "Barbosa, Haniel Moreira"
Agora exibindo 1 - 2 de 2
- Resultados por página
- Opções de Ordenação
Dissertação Formal verification of PLC programs using the B Method(Universidade Federal do Rio Grande do Norte, 2012-11-01) Barbosa, Haniel Moreira; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/6657126741011519; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255Controladores Lógico Programáveis (PLCs 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 à indústria do petróleo, gás e energias renováveis. 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 para a verificação de sistemas críticos, possui amplo apoio ferramental e suporte à 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 PLCsTese Novas técnicas de instanciação e produção de demonstrações para a resolução SMT(2017-09-05) Barbosa, Haniel Moreira; Deharbe, David Boris Paul; http://lattes.cnpq.br/2985658685449858; https://orcid.org/0000-0003-0188-2300; http://lattes.cnpq.br/6657126741011519; Reynolds, Andrew; Dubois, Catherine; Ábrahám, Erika; Almeida, João Marcos de; https://orcid.org/0000-0003-2601-8164; http://lattes.cnpq.br/3059324458238110; Fontaine, Pascal; Rümmer, Philipp; Merz, StephanEm muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de solucionadores de satisfatibilidade módulo teorias (SMT) como backends para resolver automaticamente condições que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribuição é fornecer um arcabouço uniforme e eficiente para raciocinar com fórmulas quantificadas em solucionadores SMT, em que, geralmente, várias técnicas de instanciação são empregadas para lidar com quantificadores. Mostramos que as principais técnicas de instanciação podem ser lançadas neste arcabouço unificador para lidar com fórmulas quantificadas com igualdade e funções não interpretadas. O arcabouço baseia-se no problema de E-ground (dis)unificação, uma variação do problema clássico de E-unificação rígida. Apresentamos um cálculo correto e completo para resolver esse problema na prática: Fechamento de Congruência com Variáveis Livres (CCFV). Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração em várias bibliotecas de referência, decorrentes de aplicações do mundo real. Nossa segunda contribuição é uma estrutura para o processamento de fórmulas ao mesmo tempo que produz demonstrações detalhadas. Nosso objetivo é aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de raciocínio automatizado similares, fornecendo justificativas que podem ser verificadas com eficiência de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstração, por exemplo, geralmente requerem a reconstrução da justificação fornecida pelo solucionador em uma determinada obrigação de prova. Os principais componentes da nossa estrutura de produção de demonstrações são um algoritmo genérico de recursão contextual e um conjunto extensível de regras de inferência. Clausificação, Skolemização, simplificações específicas de teorias e expansão das expressões "let" são exemplos dessa estrutura. Com estruturas de dados adequadas, a geração de demonstrações cria apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas em tempo linear. Também implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do código, aumentando o número de problemas para os quais demonstrações detalhadas podem ser produzidas.