Made available in DSpace on 2013-08-07T18:42:20Z (GMT). No. of bitstreams: 1 000415453-Texto+Completo-0.pdf: 1512363 bytes, checksum: 42043724fd23719f6c7529ca1c04ff6a (MD5) Previous issue date: 2009 / The solution of Markovian models with large state spaces is one of the major challenges in performance evaluation. Structured formalisms such as Stochastic Automata Networks (SAN) were proposed to describe multiple components through the use of automata, whose transitions are determined by local or synchronizing events, having constant or functional rates. Due to the inherent modular representation of SAN, it is possible through tensor (Kronecker) algebra to store the model infinitesimal generator in memory, in a compact and efficient manner. The numerical methods that calculate the stationary probabilities distribution are adapted to these structured representations. The basic operation is the vector-descriptor multiplication, which is the product of a probability vector by tensor products composed by sparse matrices. The traditional Shuffle algorithm is characterized by the access and shuffling positions of the vector when multiplied by each matrix of a tensor product term. This approach is considered highly memory-efficient, however, presents a high processing time for the solution of real models. We propose a more flexible and hybrid algorithm for the vector-descriptor product called Split, putting the Shuffle approach in perspective, presenting significant improvements in the execution time for a diverse set of models without impairing the computational resources. Nevertheless, increasing the state space of models, this algorithm also becomes unsuitable to obtain a numerical solution. To mitigate the impact of state space explosion, it is proposed the use of simulations to estimate the stationary probability distribution as close as possible to analytical solutions, executing long-run trajectories. We propose the application of perfect sampling techniques (also called exact simulation) to produce reliable samples through trajectory couplings, in reverse simulation time. This technique is distinguished from traditional simulation by avoiding transient periods and the initial state to be chosen. It is discussed the feasibility of these algorithms applied to SAN, specially focusing on partially ordered state spaces and monotonicity properties allowing the execution of less parallel trajectories for the generation of a sample. The iterative numerical analysis and the simulation of stochastic models are approaches that present advantages and limitations when applied to the solution of structured models such as SAN. The main contribution of this thesis focuses on the reduction of the impact of state space explosion of Markovian models described in SAN, proposing solutions when the computational time of analytical techniques is too long or when the memory requirements for the probability vector exceeds current technologies storage capacity. / 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 2013-08-07T18:42:18Z (GMT). No. of bitstreams: 1 000401643-Texto+Completo-0.pdf: 1372723 bytes, checksum: 20c936d36ee28a143b6a71699d15fc8b (MD5) Previous issue date: 2008 / Several studies about the performance analysis of Ad Hoc Networks can be found in the literature. These analyses use simulation tools or analitycal methods, such Markovian models or equation systems. The mobility is a deterministic factor in the performance of Ad Hoc Networks and, to make possible these analyses, several mobility models are proposed in the literature. In this work some existing mobility models found in the literature are described, and the Random Waypoint and Random Direction models are studied in more detail. Models are proposed to represent and analyze these two mobility models, using the Markovian formalism of Stochastic Automata Networks, making possible a detailed analysis of the Spacial Node Distribution in accordance to the possible variations of these mobility models. Some of the variations considered in this modeling are: speed, pause time, size of moves, routing strategies. The consistency of the results achieved is evaluated comparing with other results from the literature, demonstrating a satisfactory degree of precision. / 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 2013-08-07T18:42:36Z (GMT). No. of bitstreams: 1 000443491-Texto+Completo-0.pdf: 1136202 bytes, checksum: c2049d25a95c861594c26fc8f318b4e0 (MD5) Previous issue date: 2012 / 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 2013-08-07T18:42:44Z (GMT). No. of bitstreams: 1 000443170-Texto+Completo-0.pdf: 1479067 bytes, checksum: 6992d7b626a852b264ada088113d267b (MD5) Previous issue date: 2012 / 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 2013-08-07T18:42:51Z (GMT). No. of bitstreams: 1 000431853-Texto+Completo-0.pdf: 1050260 bytes, checksum: f000297f2655b6e67365f8fbd2031764 (MD5) Previous issue date: 2011 / The purpose of this Master Thesis is to propose a tensor representation for Hidden Markov Models (HMM). The chosen way to reach this goal goes through the study of how to convert an HMM into a SAN model (Stochastic Automata Networks – SAN): structured and with a known tensor format. The convertion strategy consists on the the creation of two automata, one corresponding to the hidden Markov chain and another to represent the HMM model emissions. These automata interact with each other by means of synchronized transitions and some defined functional dependencies. An intermediate step is necessary to show the equivalence between the SAN and HMM representations, being this step the obtainment of a global Markov chain capable of representing the HMM model. The equality between the global Markov chains obtained from both the SAN and HMM formalisms constitutes the equivalence proof. / 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 2013-08-07T18:42:52Z (GMT). No. of bitstreams: 1 000436196-Texto+Completo-0.pdf: 3266895 bytes, checksum: af63490ff68d65f3eb3aa355bb1c1e97 (MD5) Previous issue date: 2011 / 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 2013-08-07T18:43:06Z (GMT). No. of bitstreams: 1 000425004-Texto+Completo-0.pdf: 1283916 bytes, checksum: 06a02199cf1e50a23c7a99c93e1147e3 (MD5) Previous issue date: 2010 / The process of software development is a task that involves a set of activities to be performed and, in many cases, by large and geographically dispersed teams. This requires the utilization of methods that renders a broad vision of all stages of the development process. The UML (Unified Modeling Language) is a modeling language that enables this vision through the use of diagrams that graphically demonstrates the software structure being developed. The activity diagram is used to model the behavior of the system with executing flows for every defined activity In order to obtain a behavioral model of computational systems, this work presents a proposal to converter activity diagrams to SAN (Stochastic Automata Networks), a mathematical formalism for modeling probabilistic index extraction related to the states, allowing decisions making for project resources allocated. To demonstrate how to execute the conversion, we use a simplified version of the elements from the UML activity diagrams to describe both parameters and rules associated to de conversion. We also present the results generated from the SAN model. / 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 2014-07-11T02:02:28Z (GMT). No. of bitstreams: 1 000459162-Texto+Completo-0.pdf: 4186967 bytes, checksum: 6dd4e203f8e1da6979a67d378beb6228 (MD5) Previous issue date: 2013 / 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.

Made available in DSpace on 2013-08-07T18:43:33Z (GMT). No. of bitstreams: 1 000437824-Texto+Completo-0.pdf: 998259 bytes, checksum: 86aed75c028c71b8918c33ddb60ad22f (MD5) Previous issue date: 2006 / 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 2013-08-07T18:43:35Z (GMT). No. of bitstreams: 1 000449321-Texto+Completo-0.pdf: 6617499 bytes, checksum: 57811360aff324876ce7118b02859e61 (MD5) Previous issue date: 2013 / 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.