Utilize este identificador para citar ou criar um atalho para este documento: http://hdl.handle.net/10923/1684
Tipo: masterThesis
Título: Geração de contraexemplos e testemunhas para um verificador de modelos descritos em redes de autômatos estocásticos
Autor(es): Correa, Claiton Marques
Orientador: Dotti, Fernando Luís
Editora: Pontifícia Universidade Católica do Rio Grande do Sul
Programa: Programa de Pós-Graduação em Ciência da Computação
Data de Publicação: 2013
Palavras-chave: INFORMÁTICA
REDES DE AUTÔMATOS ESTOCÁSTICOS
SIMULAÇÃO E MODELAGEM EM COMPUTADORES
Resumo: A possibilidade de geração de contraexemplos e testemunhas é um dos principais atrativos da técnica de Verificação de Modelos. Os contraexemplos são uma boa fonte para depuração do sistema, pois são gerados quando uma especificação é refutada pelo modelo. Já as testemunhas ratificam a satisfação de uma especificação pelo modelo através de uma execução do sistema. Esta dissertação de Mestrado é parte de um projeto de construção de um verificador de modelos para modelos descritos em Redes de Autômatos Estocásticos e trata da implementação da geração de contraexemplos e testemunhas para a ferramenta.
The counterexamples and witnesses generation is one of the main attractive features of Model Checking. Counterexamples are a great data source to debug the system, because they are generated when a specification is violeted by a model of the system. On other hand, witnesses show that a model of the system holds for an specification, through an execution trace of the system. This dissertation is part of a project aimed to the construction of a Model Checker for Stochastic Automata Networks and focuses in the generation of counterexamples and witnesses for the tool.
URI: http://hdl.handle.net/10923/1684
Aparece nas Coleções:Dissertação e Tese

Arquivos neste item:
Arquivo Descrição TamanhoFormato 
000449321-Texto+Completo-0.pdfTexto Completo6,46 MBAdobe PDFAbrir
Exibir


Todos os itens no Repositório da PUCRS estão protegidos por copyright, com todos os direitos reservados, e estão licenciados com uma Licença Creative Commons - Atribuição-NãoComercial 4.0 Internacional. Saiba mais.