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/5260
Registro completo de metadados
Campo DCValorIdioma
dc.creatorWondracek, Alberto do Carmo Sulzbacher-
dc.contributor.advisor1Dotti, Fernando Luís-
dc.contributor.advisor1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4782513J6por
dc.date.accessioned2015-04-14T14:50:13Z-
dc.date.available2014-07-10-
dc.date.issued2013-03-25-
dc.identifier.citationWONDRACEK, Alberto do Carmo Sulzbacher. Tradução de modelos de redes de automatos estocásticos para a linguagem do NUSMV. 2013. 268 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/5260-
dc.description.resumoRedes de autômatos estocásticos (SAN) é um formalismo que permite a descrição de sistemas a fim de realizar avaliações quantitativas. O objetivo deste trabalho é possibilitar avaliações qualitativas de modelos SAN através de sua tradução para a linguagem de um verificador existente. O trabalho propõe, detalha e exemplifica o mapeamento de um subconjunto de modelos SAN para a linguagem de entrada do NuSMV. Conforme o resultado observado, os modelos para o NuSMV gerados pelo tradutor preservam a semântica dos respectivos modelos SAN originais pois apresentam sistemas de transição de estados isomórficos. A verificação de propriedades em CTL (Computation Tree Logic) sobre os modelos SAN é exemplificadapor
dc.description.abstractStochastic Automata Network (SAN) is a formalism that allows the description of systems in order to evaluate them quantitatively. The aim of this work is to enable the qualitative evaluation on SAN models through its translation to the language of an existent model checker. This work proposes, details and exemplifies the mapping of a subset of SAN models to the NuSMV input language. As observed, the NuSMV models generated by the translator preserve the semantic of its originals SAN models because they have an isomorphic transition state system. The model checking through CTL (Computation Tree Logic) on SAN models is exemplified as welleng
dc.description.provenanceMade available in DSpace on 2015-04-14T14:50:13Z (GMT). No. of bitstreams: 1 459162.pdf: 4186967 bytes, checksum: 6dd4e203f8e1da6979a67d378beb6228 (MD5) Previous issue date: 2013-03-25eng
dc.formatapplication/pdfpor
dc.thumbnail.urlhttp://tede2.pucrs.br:80/tede2/retrieve/15331/459162.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.titleTradução de modelos de redes de automatos estocásticos para a linguagem do NUSMVpor
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 
459162.pdfTexto Completo4,09 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.