Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B.
Event-B, Solucionadores SMT, Plataforma Rodin, Obrigações de prova, Verificação formal.
Event-B é um método formal de modelagem e verificação de sistemas de transição discre- tos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verifica- das, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos, bem como certificá-los em relação aos requisitos do sistema modelado. Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teoremas usados para ve- rificar 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 identi- ficar núcleo insatisfatível. 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. Este trabalho propõe uma série de complementos ao plug-in para solucionadores SMT em Rodin, a sa- ber, melhorias de usabilidade que podem impactar positivamente a produtividade quando obrigações de prova são reportadas como inválidas (isto é, satisfatíveis ou desconhecidas) pelo plug-in. Adicionalmente, algumas modificações na forma como o plug-in lida com resultados válidos − por exemplo, ao manipular provas e núcleos insatisfatíveis − para gerar novas regras de prova são também consideradas.