Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

• Ano de defesa: 2015
• Autor(a) principal: Fragoso, Paulo Ewerton Gomes
• Orientador(a): Deharbe, David Boris Paul
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Rio Grande do Norte
• Programa de Pós-Graduação: PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
• País: Brasil
• Palavras-chave em Português: Event-B; Solucionadores SMT; Plataforma Rodin; Obrigações de prova; Verificação formal
• Área do conhecimento CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
• Link de acesso: https://repositorio.ufrn.br/jspui/handle/123456789/19825

Event-B é um método formal de modelagem e verificação de sistemas de transição discretos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verificadas, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos. Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teoremas usados para verificar a satisfatibilidade de fórmulas lógicas considerando uma teoria (ou combinação de teorias) subjacente. Solucionadores SMT não apenas lidam com fórmulas extensas em lógica de primeira ordem, como também podem gerar modelos e provas, bem como identificar subconjuntos insatisfatíveis de hipóteses (núcleos insatisfatíveis). O suporte ferramental para Event-B é provido pela Plataforma Rodin: um IDE extensível, baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar à plataforma técnicas alternativas e eficientes de verificação. Neste trabalho foi implementada uma série de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na interface do usuário para quando obrigações de prova são reportadas como inválidas pelo plug-in. Adicionalmente, algumas características do plug-in, tais como suporte à geração de provas e extração de núcleo insatisfatível, foram modificadas de modo a tornaremse compatíveis com o padrão SMT-LIB para solucionadores SMT. Realizaram-se testes utilizando obrigações de prova aplicáveis para demonstrar as novas funcionalidades. As contribuições descritas podem, potencialmente, afetar a produtividade de forma positiva.