1. TEDE PUCRS
  2. Teses e Dissertações dos Programas de Pós-Graduação da PUCRS
  3. Programa de Pós-Graduação em Ciência da Computação
Exportar este item: EndNote BibTex

Use este identificador para citar ou linkar para este item: https://tede2.pucrs.br/tede2/handle/tede/5225
Registro completo de metadados
Campo DCValorIdioma
dc.creatorCorrea, Claiton Marques-
dc.creator.Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4495661D3por
dc.contributor.advisor1Dotti, Fernando Luís-
dc.contributor.advisor1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4782513J6por
dc.date.accessioned2015-04-14T14:50:03Z-
dc.date.available2013-07-12-
dc.date.issued2013-03-26-
dc.identifier.citationCORREA, 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.por
dc.identifier.urihttp://tede2.pucrs.br/tede2/handle/tede/5225-
dc.description.resumoA 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 ferramentapor
dc.description.abstractThe 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 tooleng
dc.description.provenanceMade available in DSpace on 2015-04-14T14:50:03Z (GMT). No. of bitstreams: 1 449321.pdf: 6617499 bytes, checksum: 57811360aff324876ce7118b02859e61 (MD5) Previous issue date: 2013-03-26eng
dc.formatapplication/pdfpor
dc.thumbnail.urlhttp://tede2.pucrs.br:80/tede2/retrieve/15371/449321.pdf.jpg*
dc.languageporpor
dc.publisherPontifícia Universidade Católica do Rio Grande do Sulpor
dc.publisher.departmentFaculdade de Informácapor
dc.publisher.countryBRpor
dc.publisher.initialsPUCRSpor
dc.publisher.programPrograma de Pós-Graduação em Ciência da Computaçãopor
dc.rightsAcesso Abertopor
dc.subjectINFORMÁTICApor
dc.subjectREDES DE AUTÔMATOS ESTOCÁSTICOSpor
dc.subjectSIMULAÇÃO E MODELAGEM EM COMPUTADORESpor
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAOpor
dc.titleGeração de contraexemplos e testemunhas para um verificador de modelos descritos em redes de autômatos estocásticospor
dc.typeDissertaçãopor
Aparece nas coleções:Programa de Pós-Graduação em Ciência da Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
449321.pdfTexto Completo6,46 MBAdobe PDFThumbnail

Baixar/Abrir Pré-Visualizar
Mostrar registro simples do item Recomendar este item Visualizar estatísticas


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.