Detalhes bibliográficos
| Ano de defesa: |
2014 |
| Autor(a) principal: |
Lemos Junior, Luiz Carlos |
| Orientador(a): |
Cavalheiro, Simone André da Costa |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal de Pelotas
|
| Programa de Pós-Graduação: |
Programa de Pós-Graduação em Computação
|
| Departamento: |
Centro de Desenvolvimento Tecnológico
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Área do conhecimento CNPq: |
|
| Link de acesso: |
http://guaiaca.ufpel.edu.br/handle/prefix/8594
|
Resumo: |
A computacao e empregada diariamente no mundo moderno, atraves de sistemas que estao a cada dia mais complexos. A ocorrencia de erros no funcionamento desses programas vem aumentando prejudicando as pessoas. Portanto, e necessario utilizar meios que aumentem o nıvel de confianca dos sistemas. Uma forma de desenvolver sistemas mais confiaveis e utilizando metodos formais. Dentro destas tecnicas encontra-se a especificacao e a verificacao formal. Uma linguagem atraente para especificacao formal e a gramatica de grafos (GG), pois e visual e baseada em um mecanismo simples de reescrita de regras. Ja a verificacao pode ser realizada pela tecnica de prova de teoremas, que permite a prova de propriedades para sistemas com espaco de estados grande ou ate mesmo infinito. A abordagem para o uso da tecnica de prova de teoremas para a verificacao de sistemas descritos em GG ja e conhecida. Nessa abordagem GG foi traduzida para a linguagem Event-B, o que possibilitou utilizar a plataforma Rodin para a prova de propriedades. No momento da verificacao sao geradas obrigacoes de prova, as quais devem ser demonstradas. Algumas delas sao descarregadas de forma automatica e outras necessitam da intervencao do usuario com certa experiencia. Essa intervencao, na maioria das vezes, n ao ´e trivial e acaba por restringir o uso da tecnica. Este trabalho visa otimizar o processo de verificacao, propondo taticas de prova para demonstrar as obrigacoes interativas, as quais auxiliam o desenvolvedor no momento da verificacao. Primeiramente sao apresentadas taticas para os padroes de obrigaçoes de prova de um sistema de GG. Logo apos, taticas para demonstrar obrigacoes de propriedades especficas s ao propostas. A apresentacao das taticas e feita atraves da descricao dos passos necessarios para as demonstracoes das propriedades consideradas, descrevendo as arvores de prova e propondo arvores de uso. Em qualquer uma das formas e possıvel realizar a prova da obrigacao correspondente. |
