Use este identificador para citar ou linkar para este item:
https://repositorio.ufrn.br/handle/123456789/17984
Título: | Prova automática de satisfatibilidade módulo teoria aplicada ao método B |
Autor(es): | Tavares, Cláudia Fernanda Oliveira Kiermes |
Orientador: | Déharbe, David Boris Paul |
Palavras-chave: | Método B;Obrigações de prova;Verificação formal;Teoria dos conjuntos;Satisfatibilidade módulo teoria. |
Data do documento: | 27-Jul-2007 |
Editor: | Universidade Federal do Rio Grande do Norte |
Referência: | TAVARES, Cláudia Fernanda Oliveira Kiermes. Prova automática de satisfatibilidade módulo teoria aplicada ao método B. 2007. 136 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2007. |
Resumo: | Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B |
URI: | https://repositorio.ufrn.br/jspui/handle/123456789/17984 |
Aparece nas coleções: | PPGSC - Mestrado em Sistemas e Computação |
Arquivos associados a este item:
Arquivo | Descrição | Tamanho | Formato | |
---|---|---|---|---|
ClaudiaFCKT.pdf | 512,8 kB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.