Export this record: EndNote BibTex

Please use this identifier to cite or link to this item: http://tede2.pucrs.br/tede2/handle/tede/5235
Full metadata record
DC FieldValueLanguage
dc.creatorOleksinski, Lucas Giaretta-
dc.creator.Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4407302A6por
dc.contributor.advisor1Dotti, Fernando Luís-
dc.contributor.advisor1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4782513J6por
dc.date.accessioned2015-04-14T14:50:05Z-
dc.date.available2013-09-24-
dc.date.issued2013-03-25-
dc.identifier.citationOLEKSINSKI, Lucas Giaretta. Abordagens paralelas para Model Checking de redes de autômatos estocásticos. 2013. 123 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/5235-
dc.description.resumoO emprego de sistemas complexos e críticos para automação de tarefas do cotidiano faz crescer a dependência das pessoas, gerando desconforto em relação à segurança de tais sistemas. Nos últimos anos algumas técnicas têm sido desenvolvidas visando facilitar as atividades relacionadas à validação de projetos nos estágios iniciais do ciclo de desenvolvimento. Verificação de modelos é uma técnica formal automática que permite a verificação de sistemas concorrentes de estados finitos sob propriedades descritas em lógicas temporais através do emprego de algoritmos que avaliam exaustivamente o sistema sob consideração. Entretanto, esta técnica é custosa no que tange ao armazenamento em memória e processamento, justificando o desenvolvimento de algoritmos paralelos e distribuídos para poderosos agregados computacionais. Esta dissertação relata o estudo e desenvolvimento de algoritmos de verificação de modelos descritos em Redes de Autômatos Estocásticos e propriedades descritas na lógica temporal Computation Tree Logic para ambientes que endereçam espaços de memória de maneira distribuída.por
dc.description.abstractThe use of critical and complex systems at automation of daily tasks increases the people s dependence, generating unease about the safety of such systems. In the last years several techniques have been developed to facilitate activities related to design validation in the early stages of the development cycle. Model Checking is an automatic formal technique that allows verification of finite-state concurrent systems under properties described in temporal logics by employing verification algorithms that exhaustively assess the correctness of the system under consideration. Indeed, this technique is costly with respect to storage and processing, justifying the development of parallel and distributed algorithms for powerful computing clusters. This dissertation reports the study and development of verification algorithms for models described in Stochastic Automata Networks and properties written in Computation Tree Logic temporal logic for environments that address memory spaces in a distributed way.eng
dc.description.provenanceMade available in DSpace on 2015-04-14T14:50:05Z (GMT). No. of bitstreams: 1 451032.pdf: 3224202 bytes, checksum: 0ed1399ff0656c16c4c22f4f6e16cb87 (MD5) Previous issue date: 2013-03-25eng
dc.formatapplication/pdfpor
dc.thumbnail.urlhttp://tede2.pucrs.br:80/tede2/retrieve/15427/451032.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.subjectLÓGICA TEMPORAL (COMPUTAÇÃO)por
dc.subjectSIMULAÇÃO E MODELAGEM EM COMPUTADORESpor
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAOpor
dc.titleAbordagens paralelas para Model Checking de redes de autômatos estocásticospor
dc.typeDissertaçãopor
Appears in Collections:Programa de Pós-Graduação em Ciência da Computação

Files in This Item:
File Description SizeFormat 
451032.pdfTexto Completo3.15 MBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.