Document details

Conselho Nacional de Desenvolvimento Científico e Tecnológico

Uma linha de produtos de software (LPS) é definida como um conjunto de sistemas de software que compartilham características em comum, mas que são suficientemente distintos entre si, desenvolvidos a partir de um conjunto de artefatos reusáveis. Modelos de features e configuração são usados para possibilitar a geração automática de produtos a partir destes artefatos. Um modelo de features representa o conjunto de possíveis configurações de produto de uma LPS, enquanto o modelo de configuração estabelece o mapeamento entre features e implementação. Por exemplo, associando expressões de features, na forma de proposições lógicas, a artefatos. Os benefícios de produtividade que a abordagem de LPS fornece tornam possível que uma LPS seja capaz de gerar milhares de produtos. Neste contexto, erros cometidos ao especificar o modelo de configuração podem resultar em produtos inválidos - o problema da composição segura. Este problema pode ser difícil de ser detectado manualmente, já que os modelos de features e configuração podem tornar-se muito complexos. Gerar todos os produtos de uma LPS pode não ser prático, dado que existem LPS em que é possível gerar milhares de produtos. No entanto, mesmo modelos de configuração que não permitem a geração de produtos inválidos podem ter problemas na sua estrutura interna, como complexidade e duplicação, especialmente no contexto de LPS grandes, onde sua manutenção pode se tornar difícil. Precisamos nos certificar de que não introduzimos erros ao corrigir estes problemas. Neste trabalho, é proposta uma abordagem automática de verificação de composição segura para LPS baseadas em modelos de configuração. Esta abordagem é baseada na tradução de instâncias específicas de modelos de features e configuração em lógica proposicional, usando uma teoria codificada com Alloy. O suporte ferramental fornecido pelo Alloy Analyzer auxilia a verificação. Também é proposto um catálogo de refatoramentos simples para modelos de configuração, como uma maneira de evitar erros ao corrigir problemas na estrutura interna de tais modelos. Este catálogo é formalizado usando uma teoria geral para modelos de configuração especificada com o Prototype Verification System (PVS). Nós avaliamos a abordagem de verificação usando sete versões de uma LPS, com modelos de features que possibilitam a geração de até 272 produtos. Os resultados demonstram a vantagem de usar esta abordagem ao invés de gerar todos os produtos da LPS, já que o tempo médio para compilar um único produto da LPS é maior que o tempo para analisá-la na maior das versões analisadas. Também avaliamos o catálogo de refatoramento provando consistência (soundness) dos refatoramentos propostos no provador de teoremas de PVS