| Share record |
|
Export this record:
Please use this identifier to cite or link to this item:
https://tede2.pucrs.br/tede2/handle/tede/5225| Document type: | Dissertação |
| Title: | Geração de contraexemplos e testemunhas para um verificador de modelos descritos em redes de autômatos estocásticos |
| Author: | Correa, Claiton Marques  |
| Advisor: | Dotti, Fernando Luís |
| Abstract (native): | 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 |
| Abstract (english): | 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 |
| Keywords: | INFORMÁTICA REDES DE AUTÔMATOS ESTOCÁSTICOS SIMULAÇÃO E MODELAGEM EM COMPUTADORES |
| CNPQ Knowledge Areas: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO |
| Language: | por |
| Country: | BR |
| Publisher: | Pontifícia Universidade Católica do Rio Grande do Sul |
| Institution Acronym: | PUCRS |
| Department: | Faculdade de Informáca |
| Program: | Programa de Pós-Graduação em Ciência da Computação |
| Citation: | CORREA, Claiton Marques. Geração de contraexemplos e testemunhas para um verificador de modelos descritos em redes de autômatos estocásticos. 2013. 107 f. Dissertação (Mestrado em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul, Porto Alegre, 2013. |
| Access type: | Acesso Aberto |
| URI: | http://tede2.pucrs.br/tede2/handle/tede/5225 |
| Issue Date: | 26-Mar-2013 |
| Appears in Collections: | Programa de Pós-Graduação em Ciência da Computação |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 449321.pdf | Texto Completo | 6.46 MB | Adobe PDF |  Download/Open Preview |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.