Prova automática de satisfatibilidade módulo teoria aplicada ao método B
| dc.contributor.advisor | Déharbe, David Boris Paul | pt_BR |
| dc.contributor.advisorID | por | |
| dc.contributor.advisorLattes | http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5 | por |
| dc.contributor.author | Tavares, Cláudia Fernanda Oliveira Kiermes | pt_BR |
| dc.contributor.authorID | por | |
| dc.contributor.authorLattes | http://lattes.cnpq.br/5850072430267997 | por |
| dc.contributor.referees1 | Abrantes, Jorge César | pt_BR |
| dc.contributor.referees1ID | por | |
| dc.contributor.referees1Lattes | http://lattes.cnpq.br/1424808046858622 | por |
| dc.date.accessioned | 2014-12-17T15:47:48Z | |
| dc.date.available | 2008-12-05 | pt_BR |
| dc.date.available | 2014-12-17T15:47:48Z | |
| dc.date.issued | 2007-07-27 | pt_BR |
| dc.description.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 | por |
| dc.format | application/pdf | por |
| dc.identifier.citation | 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. | por |
| dc.identifier.uri | https://repositorio.ufrn.br/jspui/handle/123456789/17984 | |
| dc.language | por | por |
| dc.publisher | Universidade Federal do Rio Grande do Norte | por |
| dc.publisher.country | BR | por |
| dc.publisher.department | Ciência da Computação | por |
| dc.publisher.initials | UFRN | por |
| dc.publisher.program | Programa de Pós-Graduação em Sistemas e Computação | por |
| dc.rights | Acesso Aberto | por |
| dc.subject | Método B | por |
| dc.subject | Obrigações de prova | por |
| dc.subject | Verificação formal | por |
| dc.subject | Teoria dos conjuntos | por |
| dc.subject | Satisfatibilidade módulo teoria. | por |
| dc.subject.cnpq | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO | por |
| dc.title | Prova automática de satisfatibilidade módulo teoria aplicada ao método B | por |
| dc.type | masterThesis | por |
Arquivos
Pacote Original
1 - 1 de 1
Carregando...
- Nome:
- ClaudiaFCKT.pdf
- Tamanho:
- 512.8 KB
- Formato:
- Adobe Portable Document Format
Carregando...