|
|
Tipo de Mídia:
Texto
|
|
Formato:
.pdf
|
Tamanho:
428,74
KB
|
|
|
|
|
|
|
|
|
|
|
|
|
Título: |
|
Verificação distribuída de modelos: investigando o uso de grades computacionais |
Autor: |
|
Paulo Eduardo
|
Categoria: |
|
Teses e Dissertações |
Idioma: |
|
Português |
Instituição:/Parceiro |
|
[cp] Programas de Pós-graduação da CAPES
|
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. |
|
|
|
|
|
|
|
|
|