Portal Domínio Público - Biblioteca digital desenvolvida em software livre  
Missão
Política do Acervo
Estatísticas
Fale Conosco
Quero Colaborar
Ajuda
 
 
Tipo de Mídia: Texto
Formato:  .pdf
Tamanho:  428,74 KB
     
  Detalhe da ibra
Pesquisa Básica
Pesquisa por Conteúdo
Pesquisa por Nome do Autor
Pesquisa por Periodicos CAPES
 
     
 
Título:  
  Verificação distribuída de modelos: investigando o uso de grades computacionais
Autor:  
  Paulo Eduardo   Listar as obras deste autor
Categoria:  
  Teses e Dissertações
Idioma:  
  Português
Instituição:/Parceiro  
  [cp] Programas de Pós-graduação da CAPES   Ir para a página desta Instituição
Instituição:/Programa  
  UFCG/CIÊNCIA DA COMPUTAÇÃO
Área Conhecimento  
  CIÊNCIA DA COMPUTAÇÃO
Nível  
  Mestrado
Ano da Tese  
  2007
Acessos:  
  1.052
Resumo  
  Todo programador ou engenheiro de software lida com um problema crônico na concepção de seus sistemas: violações das especificações ou requisitos de projeto. Essas violações necessitam de uma captura imediata, pois geralmente originam falhas que só podem ser descobertas tardiamente, a um custo de reparo bastante elevado. Nos últimos anos, pesquisadores da ciência da computação estão conseguindo um progresso notável no desenvolvimento de técnicas e ferramentas que verificam automaticamente requisitos e projeto. A abordagem em maior evidência chama-se verificação de modelos (model-checking). Verificação de modelos é uma técnica formal e algorítmica de se fazer verificação de propriedades de sistemas com um espaço de estados finito. Suas principais vantagens são o poder de automação e a qualidade dos resultados produzidos. Porém, esta técnica sofre de um problema fundamental — a explosão do espaço de estados — que se deve ao crescimento exponencial na estrutura que representa o comportamento de sistemas e à falta de recursos computacionais disponíveis para lidar com grandes quantidades de informação sobre o comportamento dos sistemas sob verificação. Este trabalho concentra-se em verificação de modelos utilizando plataformas de distribuição como tentativa de aliviar o problema citado. Mais detalhadamente, investigamos o uso de grades computacionais que rodam aplicações bag-of-tasks e formulamos algoritmos específicos para o processo de verificação. Aplicações bag-of-tasks são aplicações paralelas cujas tarefas são independentes entre si. Elas são as aplicações mais apropriadas para grades computacionais por permitirem heterogeneidade dos recursos. Aplicamos ferramentas de grades computacionais como uma camada entre a ferramenta de verificação e os recursos distribuídos compartilhados existentes e comparamos os quesitos desempenho e escala nos sistemas a serem verificados em relação às versões centralizadas de verificadores. A plataforma empregada na distribuição é muito atrativa no quesito custo, controle e escala. Através do compartilhamento de uma simples máquina, o engenheiro de sistemas ganha acesso a uma comunidade provedora de uma grande quantidade de recursos heterogêneos e automaticamente gerenciados para se fazer computação paralela seguindo sua filosofia. Durante o trabalho, essas vantagens são comparadas com suas desvantagens, como o alto custo de comunicação e a dificuldade de particionar o processo, por exemplo. O trabalho envolveu a produção das seguintes ferramentas: uma API genérica para a geração distribuída de grafos que representam o comportamento de sistemas concorrentes sobre plataformas de grades computacionais bag-of-tasks, um protótipo de verificação CTL que age de duas maneiras distintas, sendo on-the-fly durante a geração do espaço de estados ou sobre esse espaço de estados distribuído representado explicitamente seguindo a mesma filosofia de comunicação e versões simplificadas de simuladores de sistemas concorrentes sob alguns formalismos baseados em redes de Petri. Resultados experimentais sobre a aplicação deste ferramental são apresentados.
     
    Baixar arquivo