Verificação distribuída de modelos: investigando o uso de grades computacionais. - BARBOSA, Paulo Eduardo e Silva. (2007)
Todo programador ou engenheiro de software lida com um problema crônico na concepção de seus sistemas: violações das especiﬁcaçõ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 progressonotávelnodesenvolvimentodetécnicaseferramentasqueveriﬁcamautomaticamente requisitos e projeto. A abordagem em maior evidência chama-se veriﬁcação de modelos (model-checking). Veriﬁcação de modelos é uma técnica formal e algorítmica de se fazer veriﬁcação de propriedades de sistemas com um espaço de estados ﬁnito. 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 veriﬁcação. Este trabalho concentra-se em veriﬁcaçã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íﬁcos para o processo de veriﬁcaçã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 veriﬁcação e os recursos distribuídos compartilhados existentes e comparamos os quesitos desempenho e escala nos sistemas a serem veriﬁcados em relação às versões centralizadas de veriﬁcadores. 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 ﬁlosoﬁa. Durante o trabalho, essas vantagens são comparadas com suas desvantagens, como o alto custo de comunicação e a diﬁculdade 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 veriﬁcação CTL que age de duas maneiras distintas, sendo on-the-ﬂy durante a geração do espaço de estados ou sobre esse espaço de estados distribuído representado explicitamente seguindo a mesma ﬁlosoﬁa de comunicação e versões simpliﬁcadas de simuladores de sistemas concorrentes sob alguns formalismos baseados em redes de Petri. Resultados experimentais sobre a aplicação deste ferramental são apresentados.