Detalhes bibliográficos
| Ano de defesa: |
2010 |
| Autor(a) principal: |
Motta Teixeira, Leopoldo |
| Orientador(a): |
Henrique Monteiro Borba, Paulo |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
eng |
| Instituição de defesa: |
Universidade Federal de Pernambuco
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://repositorio.ufpe.br/handle/123456789/2323
|
Resumo: |
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 |
