Made available in DSpace on 2015-04-14T14:48:59Z (GMT). No. of bitstreams: 1 401643.pdf: 1372723 bytes, checksum: 20c936d36ee28a143b6a71699d15fc8b (MD5) Previous issue date: 2007-03-02 / Muitos trabalhos sobre a an?lise de desempenho de Redes Ad Hoc podem ser encontrados na literatura. Estas an?lises podem ser atrav?s de ferramentas de simula??o ou por m?todos anal?ticos, como formalismos markovianos ou sistemas de equa??es. A movimenta??o ? um fator determinante no desempenho de Redes Ad Hoc e, para possibilitar esta an?lise, foram criados padr?es de movimenta??o para modelar o comportamento dos dispositivos de rede (os nodos). Neste trabalho s?o descritos alguns padr?es de movimenta??o existentes na literatura, sendo os padr?es Random Waypoint e Random Direction estudados em mais detalhes. S?o propostos modelos para representar e analisar estes dois padr?es, utilizando o formalismo markoviano de Redes de Aut?matos Estoc?sticos, possibilitando uma an?lise detalhada da Distribui??o Espacial de Nodos de acordo com as poss?veis varia??es destes padr?es. Algumas das varia??es considerados nesta modelagem: velocidade, tempo de pausa, tamanho dos movimentos, escolha de caminho. A consist?ncia destes modelos ? avaliada comparando os resultados obtidos com outros resultados da literatura, demonstrando um satisfat?rio grau de proximidade entre os resultados

Made available in DSpace on 2015-04-14T14:49:09Z (GMT). No. of bitstreams: 1 415453.pdf: 1512363 bytes, checksum: 42043724fd23719f6c7529ca1c04ff6a (MD5) Previous issue date: 2009-03-27 / A solu??o de modelos markovianos com grande espa?o de estados ? um dos maiores desafios da ?rea de avalia??o de desempenho de sistemas. Os formalismos estruturados, como as Redes de Aut?matos Estoc?sticos (SAN), foram propostos para descrever m?ltiplos componentes atrav?s de aut?matos, cujas transi??es s?o regidas por eventos locais ou sincronizantes, com taxas de ocorr?ncia constantes ou funcionais. Devido ? capacidade de representa??o modular de SAN, atrav?s do uso de ?lgebra tensorial (ou de Kronecker), armazena-se o gerador infinitesimal do modelo de forma compacta e eficiente em mem?ria. Os m?todos num?ricos de sol??o que calculam a distribui??o estacion?ria das probabilidades s?o adaptados a estas representa??es tensoriais. A opera??o b?sica ? a multiplica??o vetor-descritor, que ? produto de um vetor de probabilidades por termos tensoriais compostos por matrizes normalmente esparsas. O principal algoritmo chama-se Shuffle e ? caracterizado pelo acesso e embaralhamento de posi??es do vetor quando multiplicado pelas matrizes de cada termo. Este m?todo ? considerado extremamente eficaz no armazenamento em mem?ria, entretanto apresenta um tempo de processamento alto para a solu??o de modelos reais. Prop?e-se um algoritmo h?brido e mais flex?vel para a multiplica??o vetor-descritor, chamado Split, que coloca o algoritmo Shuffle em perspectiva, apresentando ganhos significativos no tempo de execu??o para diversas classes de modelos, sem onerar os recursos computacionais. Entretanto, quando os modelos aumentam em escala, este algoritmo num?rico torna-se inadequado devido ao problema da explos?o do espa?o de estados. Para mitigar o impacto deste problema prop?e-se o uso de solu??es alternativas de simula??o, as quais buscam estimar a distribui??o estacion?ria de probabilidades t?o pr?ximas quanto poss?vel das solu??es anal?ticas, baseando-se na execu??o de longas trajet?rias. Utiliza-se a t?cnica de simula??o baseada em amostragem perfeita (tamb?m chamada de simula??o exata), para fornecer amostras confi?veis da distribui??o estacion?ria atrav?s do casamento de trajet?rias, em tempo de simula??o reverso. Esta difere-se da simula??o tradicional por evitar o per?odo transiente e a escolha aleat?ria de um estado inicial. Mostra-se a viabilidade destes algoritmos aplicados a SAN, principalmente quando se detectam propriedades de monotonicidade nos modelos. Espa?os de estados parcialmente ordenados e propriedades de monotonicidade permitem a execu??o de um n?mero reduzido de trajet?rias em paralelo para obten??o de uma amostra. A an?lise num?rica iterativa e a simula??o de modelos estoc?sticos s?o abordagens que apresentam vantagens e limita??es quando aplicadas ? solu??o de modelos estruturados como SAN. A principal contribui??o desta tese foca na redu??o do impacto da explos?o do espa?o de estados de modelos markovianos descritos em SAN, propondo solu??es quando o tempo de computa??o das t?cnicas anal?ticas ? muito longo ou quando os requisitos de armazenamento do vetor de probabilidade excedem a capacidade de mem?ria das tecnologias correntes.

Made available in DSpace on 2015-04-14T14:49:24Z (GMT). No. of bitstreams: 1 425004.pdf: 1283916 bytes, checksum: 06a02199cf1e50a23c7a99c93e1147e3 (MD5) Previous issue date: 2010-01-27 / O processo de desenvolvimento de software ? uma tarefa que envolve um conjunto de atividades a serem realizadas, e em muitos casos, por equipes grandes que podem se encontrar geograficamente dispersas. Isso exige do desenvolvedor a utilizac?o de m?todos que proporcionem uma vis?o de todas as etapas desse processo de desenvolvimento. A UML (Unified Modeling Language) ? uma linguagem de modelagem que possibilita essa vis?o atrav?s do uso de diagramas que demonstram graficamente a estrutura do software em desenvolvimento. O diagrama de atividades ? utilizado para modelar o comportamento do sistema, atrav?s dos fluxos de execu??o de cada atividade desempenhada pelo mesmo. Com o objetivo de obter um modelo comportamental de sistemas computacionais apresentamos neste trabalho uma proposta de convers?o de diagramas de atividades para SAN (Stochastic Automata Networks), um formalismo matem?tico que possibilita a modelagem de sistemas em geral, a partir do qual ? poss?vel extrair ?ndices probabil?sticos relacionados aos estados, permitindo aos respons?veis pelo processo de desenvolvimento tomar decis?es sobre os recursos alocados no projeto. Com o intuito de demonstrarmos como executar a convers?o, usamos uma vers?o simplificada dos elementos do diagrama de atividades da UML, para descrever os par?metros e regras utilizadas para a convers?o proposta. Apresentamos ainda os resultados obtidos a partir do modelo SAN gerado.

Made available in DSpace on 2015-04-14T14:49:32Z (GMT). No. of bitstreams: 1 431853.pdf: 1050260 bytes, checksum: f000297f2655b6e67365f8fbd2031764 (MD5) Previous issue date: 2011-03-17 / O prop?sito desta disserta??o ? propor uma representa??o tensorial para Modelos Markovianos Ocultos (Hidden Markov Models HMM). A forma escolhida para alcan?ar esse objetivo passa pelo estudo de como converter um modelo HMM em um modelo SAN (Stochastic Automata Networks): estruturado e cujo formato tensorial ? conhecido. A estrat?gia de convers?o consiste na cria??o de dois aut?matos, um correspondendo ? cadeia de Markov oculta e outro para representar as emiss?es do modelo HMM. Esses aut?matos se relacionam por transi??es sincronizadas e depend?ncias funcionais s?o definidas. Um passo intermedi?rio ? necess?rio para mostrar a equival?ncia entre as representa??es SAN e HMM, sendo este passo a obten??o de uma cadeia de Markov global capaz de representar o modelo HMM. A igualdade entre as cadeias de Markov globais obtidas a partir de ambos os formalismos SAN e HMM constitui a prova de equival?ncia.

Made available in DSpace on 2015-04-14T14:49:41Z (GMT). No. of bitstreams: 1 436196.pdf: 3266895 bytes, checksum: af63490ff68d65f3eb3aa355bb1c1e97 (MD5) Previous issue date: 2011-03-21 / This study aims to develop a tool to visually simulate Stochastic Automata Networks (SAN). The SAN formalism uses the PEPS tool for numerical solution, evaluating unexpected behaviors. These numerical solutions are the core for structured formalisms since they provide numerical results based on mathematical relationships. It is very interesting to complement the numerical solution with visual simulations because it adds more detailed information about models, making them more understandable for broader audiences of researchers and general users. The present dissertation describes a tool for modeling and visual simulation of SAN models, since its internal structure defines a compact storage schema (a Descriptor) for the transition matrix representing the underlying Markov Chain and uses tensor algebra to deal with the vector-descriptor multiplication. The proposed tool will allow both academic users and enthusiasts of the SAN formalism to manipulate models abstracting a deeper knowledge of this structured formalism. / O objetivo deste trabalho ? fornecer uma ferramenta para simula??o visual de SAN. O formalismo SAN, atrav?s da ferramenta PEPS, utiliza solu??es num?ricas para calcular erros de avalia??es condicionais ou comportamento n?o esperado de sistemas modelados atrav?s deste formalismo. Estas solu??es num?ricas s?o a base para os formalismos estruturados na medida em que fornecem resultados num?ricos por meio de rela??es matem?ticas. Complementar a efici?ncia de solu??es num?ricas com a simula??o visual ? bastante interessante, pois adiciona informa??es mais detalhadas sobre o modelo o que facilita que usu?rios acad?micos iniciantes ou pesquisadores tenham um maior entendimento da aplicabilidade do formalismo estruturado. Esta disserta??o descreve uma ferramenta para modelagem e simula??o visual de SAN que em sua estrutura define um esquema de armazenamento compacto para a matriz de transi??o da cadeia de Markov e usa a ?lgebra tensorial para lidar com as multiplica??es de vetores de base da matriz. Esta ferramenta permitir? aos usu?rios acad?micos ou entusiastas do formalismo SAN manipular modelos sem a preocupa??o de um dom?nio profundo dos conceitos deste formalismo estruturado.

Made available in DSpace on 2015-04-14T14:49:42Z (GMT). No. of bitstreams: 1 437824.pdf: 998259 bytes, checksum: 86aed75c028c71b8918c33ddb60ad22f (MD5) Previous issue date: 2007-03-20 / This research proposes a method to build the SAN, using information extracted from UML diagrams defined according to Unified Process methodology. A framework was formalized to translate the UML state diagrams into SAN structures. The UML state diagrams are basically used to describe the system features. The SAN provided reflect a usage model of the system, what can be used to generate software test cases. This research proposal is to generate the models considering two approaches: the first just focus on functionalities available for the system user, and the second one consider the whole system. This last approach also specifies a simplified function to reduce the SAN status to be visible in the PEP2003 Tool. Based on the framework proposed, a prototype was developed to generate the SAN automatically, based on UML diagrams provided by Rational Rose Tool. Finally, this search describes a case of study, where this framework is described in a real example. / Esse trabalho apresenta m?todo para a construc?o de SAN, a partir de informac?es extra?das de diagramas UML concebidos sob a abordagem do Processo Unificado. Nele foi formalizado umframework para a transcric?o de diagramas de estado UML, utilizados para a descric?o comportamental de um sistema, para uma estrutura equivalente em SAN. Essa SAN ? utilizada como um modelo de uso do sistema, de onde ? poss?vel a extrac?o de casos de teste de software, conforme verificado em estudo anteriores. Foi proposta a gerac?o dos modelos sob duas ?ticas: a primeira focada nas funcionalidades disponibilizadas aos usu?rios do sistema, e a segunda analisando o sistema como um todo. Para essa ?ltima, foi especificado um m?todo de simplificac?o da SAN, viabilizando assim a sua an?lise na ferramenta PEPS2003. Baseado no framework descrito, foi implementado um prot?tipo para a construc?o autom?tica de SAN, a partir de arquivos gerados pelo Rational Rose, arquivos esses contendo informac?es sobre os diagramas UML utilizados na descric?o do sistema. O trabalho tamb?m descreve um estudo de caso, onde s?o aplicadas as t?cnicas descritas.

Made available in DSpace on 2015-04-14T14:49:54Z (GMT). No. of bitstreams: 1 443170.pdf: 1479067 bytes, checksum: 6992d7b626a852b264ada088113d267b (MD5) Previous issue date: 2012-08-31 / Projects performance evaluation is an important aspect of global software development. Companies and institutions can obtain benefits by the use of performance evaluation of teams working in different sites. The objective of this work is to discuss a stochastic model definition to performance evaluation of Follow-The-Sun (FTS) projects aspects such as time, quality and cost. Example issues that can be addressed using this FTS model are provided with performance evaluation results. / Avalia??o de desempenho de projetos ? um aspecto importante em desenvolvimento de software Distribu?do. Empresas e institui??es podem obter benef?cios atrav?s da utiliza??o de an?lise de performance em times trabalhando em diferentes locais. Este trabalho tem como objetivo apresentar uma defini??o de modelagem estoc?stica para projetos Follow-The-Sun (FTS) em diferentes aspectos como tempo, qualidade e custo. Exemplos de uso do modelo s?o apresentados em conjunto com os resultados de avalia??o dos mesmos.

Made available in DSpace on 2015-04-14T14:49:54Z (GMT). No. of bitstreams: 1 443491.pdf: 1136202 bytes, checksum: c2049d25a95c861594c26fc8f318b4e0 (MD5) Previous issue date: 2012-08-09 / Currently, there is a growing trend for exposing software, through the Internet, as services. This new business model is called Software as a Service , where applications are no longer sold as a product, but instead are rented as a service and used by customers, who pay only according to use. However, solutions that were not developed with a focus on integration, can not easily enter into this new trend. PEPS (Performance Evaluation of Parallel Systems) and PLAT (Production Line Analysis Tool) are examples of tools into this situation. Although they are efficient and reliable solutions to solve, respectively, Stochastic Automata Networks models and theoretical performance models of serial production lines, neither have mechanisms for integration. Thus, this work proposes: Firstly, the specification of a generic and reusable framework for the provision of legacy codes as services; and secondly, the implementation of this framework for the provision of PEPS and PLAT as services. / Atualmente, existe uma crescente demanda por se disponibilizar, atrav?s da Internet, software na forma de servi?os. Este novo modelo de neg?cio ? denominado de Software como Servi?o, aonde aplica??es n?o s?o mais vendidas como um produto, mas sim cedidas na forma de um servi?o e utilizados por clientes, que pagam apenas de acordo com a utiliza??o. Entretanto, solu??es que n?o foram desenvolvidas com o foco em integra??o, n?o conseguem entrar facilmente nesta nova tend?ncia. PEPS (Performance Evaluation of Parallel Systems) e PLAT (Production Line Analysis Tool) s?o exemplos de ferramentas que se enquadram nesta situa??o. Apesar de serem solu??es eficientes e confi?veis para a solu??o de, respectivamente, modelos de Redes de Aut?matos Estoc?sticos e modelos te?ricos de linhas de produ??o seriais, nenhuma das duas possui mecanismos de integra??o. Neste sentido, este trabalho prop?e: Primeiro, a especifica??o de um framework gen?rico e reutiliz?vel para a disponibiliza??o de ferramentas na forma de servi?os; Segundo, as implementa??es deste framework para a disponibiliza??o dos software PEPS e PLAT na forma de servi?os.

Made 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-26 / The 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 tool / A 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 ferramenta

Made 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-25 / 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 / Redes 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 ? exemplificada