Por favor, use este identificador para citar o enlazar este ítem:
https://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 |
Editor: | Pontifícia Universidade Católica do Rio Grande do Sul |
Programa: | Programa de Pós-Graduação em Ciência da Computação |
Fecha de Publicación: | 2013 |
Palabras clave: | INFORMÁTICA REDES DE AUTÔMATOS ESTOCÁSTICOS SIMULAÇÃO E MODELAGEM EM COMPUTADORES |
Resumen: | 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 en las colecciones: | Dissertação e Tese
|
Todos los ítems en el Repositorio de la PUCRS están protegidos por derechos de autor, con todos los derechos reservados, y están bajo una licencia de Creative Commons Reconocimiento-NoComercial 4.0 Internacional. Sepa más.