Made available in DSpace on 2014-06-12T15:56:44Z (GMT). No. of bitstreams: 2
arquivo2985_1.pdf: 5101466 bytes, checksum: 86a375e15b77076e9eb9adffbe664c52 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2010 / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2323 |
| Date | 31 January 2010 |
| Creators | Motta Teixeira, Leopoldo |
| Contributors | Henrique Monteiro Borba, Paulo |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0017 seconds