Return to search

Abordagens paralelas para Model Checking de redes de aut?matos estoc?sticos

Made 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-25 / The 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. / O 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.

Identiferoai:union.ndltd.org:IBICT/oai:tede2.pucrs.br:tede/5235
Date25 March 2013
CreatorsOleksinski, Lucas Giaretta
ContributorsDotti, Fernando Lu?s
PublisherPontif?cia Universidade Cat?lica do Rio Grande do Sul, Programa de P?s-Gradua??o em Ci?ncia da Computa??o, PUCRS, BR, Faculdade de Inform?ca
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatapplication/pdf
Sourcereponame:Biblioteca Digital de Teses e Dissertações da PUC_RS, instname:Pontifícia Universidade Católica do Rio Grande do Sul, instacron:PUC_RS
Rightsinfo:eu-repo/semantics/openAccess
Relation1974996533081274470, 500, 600, 1946639708616176246

Page generated in 0.0017 seconds