Tradução de modelos de redes de automatos estocásticos para a linguagem do NUSMV

• Ano de defesa: 2013
• Autor(a) principal: Wondracek, Alberto do Carmo Sulzbacher
• Orientador(a): Dotti, Fernando Luís
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Pontifícia Universidade Católica do Rio Grande do Sul
• Programa de Pós-Graduação: Programa de Pós-Graduação em Ciência da Computação
• Departamento: Faculdade de Informáca
• País: BR
• Palavras-chave em Português: INFORMÁTICA; REDES DE AUTÔMATOS ESTOCÁSTICOS; SIMULAÇÃO E MODELAGEM EM COMPUTADORES
• Área do conhecimento CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
• Link de acesso: http://tede2.pucrs.br/tede2/handle/tede/5260

Stochastic 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 well