Utilize este identificador para referenciar este registo: https://hdl.handle.net/1822/75710

TítuloLightweight trustworthy high-level software design
Autor(es)Liu, Chong
Orientador(es)Cunha, Alcino
Macedo, Nuno
Palavras-chaveConcepção formal de software
Alloy
Linhas de produtos de software
Variabilidade
Refatoração
Clone-and-own
Formal software design
Software product lines
Variability
Refactoring
Data20-Dez-2021
Resumo(s)A modelação e análise formal de software é essencial para obter um projecto de software confiável antes da implementação. O Alloy, uma linguagem de especificação com uma ferramenta de análise automática, é uma abordagem popular para esta tarefa. Frequentemente, um projecto de software inclui muitas variantes com grande partilha de código. Em vez de considerar cada variante individualmente, o desenvolvimento de software orientado à funcionalidade procura desenvolver em conjunto toda a família de variantes, também designada por linha de produtos de software (LPS). Aspectos em comum são organizados em funcionalidades, implementando cada variante um sub-conjunto das mesmas. Existem duas abordagens típicas para implementação de uma LPS: abordagens composicionais, onde cada funcionalidade é implementada num módulo distinto, e abordagens anotativas, onde o código específico de cada funcionalidade é assinalado com uma anotação. A primeira é melhor para adicionar grandes blocos de código a uma funcionalidade, por exemplo uma nova classe, enquanto que a segunda suporta melhor pequenas extensões, tais como adicionar uma instrução a um método. O primeiro objectivo desta tese é propor uma extensão anotativa para o Alloy, para suportar a concepção formal de software orientada à funcionalidade. A ideia é suportar pequenas extensões a um modelo mas sem os problemas de compreensão que derivam das típicas anotações #ifdef usadas na implementação de uma LPS. Para tal, permitimos cores de fundo para identificar os fragmentos associados com cada funcionalidade, dando origem à linguagem Colorful Alloy. Também propusemos uma técnica de análise amalgamada para verificar toda uma família de variantes de uma só vez. O segundo objectivo é propor uma técnica para migração de um conjunto de variantes, possivelmente desenvolvidos com a abordagem clone-and-own, para um único modelo em Colorful Alloy. Para tal, propusemos um catálogo de refatorações e mostramos como podem ser usadas para iterativamente migrar modelos Alloy clonados para um único modelo “colorido”. Também desenvolvemos uma técnica de migração que automatiza todo este processo. Este trabalho foi avaliado com recurso a vários casos de estudo de LPSs, desenvolvidos quer pro-activamente com Colorful Alloy, quer com a abordagem clone-and-own com Alloy normal. Esta avaliação mostrou que a técnica de análise amalgamada pode aumentar consideravelmente a eficiência da verificação de uma família de variantes, quando comparada com a análise variante a variante. Também mostrou que a técnica de migração (incluindo a completamente automática) pode reduzir significativamente a quantidade de código clonado, o que em princípio permitirá simplificar a compreensão de um projecto de uma LPS.
Formal modeling and analysis is essential to achieve a trustworthy software design prior to its implementation. Alloy, a specification language with a lightweight model finder, is a popular approach to accomplish this task. Frequently, a software design encompasses many variants with a large commonality between them. Instead of considering each variant individually, feature-oriented software development tackles at once the whole family of variants, also known as a software product line (SPL). Commonalities are organized as features, with each variant implementing a particular set of features. SPL implementation techniques mainly fall into two groups: compositional approaches, which implement features in distinct modules, and annotative approaches, that wrap feature-specific code with annotations. The former is well suited to coarse-grained feature extensions, such as adding a new class, while the latter is better for fine-grained extensions, like adding a statement in a method. The first goal of this thesis is to propose an annotative extension to Alloy, to support formal featureoriented software design. Our aim was to easily support fine-grained extensions to a model, but without the comprehension obstacles of the typical #ifdef annotations used in SPL implementation. To that end, we added support for background colors to identify the fragments associated with each feature, ending up with the Colorful Alloy language. We also proposed an amalgamated analysis technique that can verify a full family of design variants at once. Our second goal was to propose a technique for migrating a collection of variants, possibly developed with the clone-and-own approach, into a single managed Colorful Alloy design. To achieve this, we proposed a catalog of refactorings and showed how they can be used to iteratively merge cloned Alloy models into a colorful model. We also proposed a one-step merging strategy that automates this technique. We evaluated our work with several SPL case studies that were either developed proactively directly with Colorful Alloy or using clone-and-own using normal Alloy. The evaluation showed that the amalgamated analysis strategy can considerably speed-up the verification of a full family of design variants, when compared to the iterative and separate analysis of each variant. It also showed that the clone merging technique (including the automatic one) can substantially reduce the amount of cloned code, which in principle simplifies the understanding of an SPL design.
TipoTese de doutoramento
DescriçãoPrograma de doutoramento em Informática
URIhttps://hdl.handle.net/1822/75710
AcessoAcesso aberto
Aparece nas coleções:BUM - Teses de Doutoramento
HASLab - Teses de Doutoramento
DI - Teses de doutoramento

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
thesis_chong.pdf4,65 MBAdobe PDFVer/Abrir

Este trabalho está licenciado sob uma Licença Creative Commons Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID