Please use this identifier to cite or link to this item: http://repositorio.ufc.br/handle/riufc/18674
Type: Tese
Title: PRECISE - Um processo de verificação formal para modelos de características de aplicações móveis e sensíveis ao contexto
Title in English: PRECISE - A Formal Verification Process for Feature Models for Mobile and Context-Aware Applications
Authors: Marinho, Fabiana Gomes
Advisor: Andrade, Rossana Maria de Castro
Keywords: Engenharia de software;Linha de produtos de software;Computação móvel e sensível ao contexto;Verificação e validação;Modelos de características;Verificação formal
Issue Date: 2012
Citation: MARINHO, Fabiana Gomes. PRECISE - Um processo de verificação formal para modelos de características de aplicações móveis e sensíveis ao contexto. 2012. 181 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012.
Abstract in Brazilian Portuguese: As LPSs, além do seu uso em aplicações tradicionais, têm sido utilizadas no desenvolvimento de aplicações que executam em dispositivos móveis e são capazes de se adaptarem sempre que mudarem os elementos do contexto em que estão inseridas. Essas aplicações, ao sofrerem alterações devido a mudanças no seu ambiente de execução, podem sofrer adaptações inconsistentes e, consequentemente, comprometer o comportamento esperado. Por esse motivo, é essencial a criação de um processo de verificação que consiga checar a corretude e a consistência dessas LPSS, bem como checar a corretude tanto dos produtos derivados como dos produtos adaptados dessas LPSs. Sendo assim, nesta tese de doutorado é proposto o PRECISE - um Processo de Verificação Formal para Modelos de Características de Aplicações Móveis e Sensíveis ao Contexto. O PRECISE auxilia na identificação de defeitos na modelagem da variabilidade de uma LPS para aplicações móveis e sensíveis ao contexto e, assim, minimiza problemas que ocorreriam durante a execução dos produtos gerados a partir dessa LPS. É importante ressaltar que o PRECISE é definido com base em uma especificação formal e em um conjunto de propriedades de boa formação elaborados usando Lógica de Primeira Ordem. Essa especificação é um pré-requisito para a realização de uma modelagem da variabilidade sem ambiguidades. Para avaliar o PRECISE, uma validação é realizada a partir da especificação formal e das propriedades de boa formação definidas no processo. Essa validação tem como objetivo mostrar que o PRECISE consegue identificar defeitos, anomalias e inconsistências existentes em um modelo de variabilidades de uma LPS para aplicações móveis e sensíveis ao contexto. Nessa validação, cinco técnicas diferentes são utilizadas: Perfil UML, OCL, Lógica Proposicional, Prolog e Simulação. Além de minimizar os defeitos e inconsistências dos modelos de variabilidades das LPSs, o PRECISE ainda se beneficia da generalidade e flexibilidade intrínsecas à notação formal usada na sua especificação.
Abstract: SPLc have been used to develop different types of applications, including the ones that run on mobile devices and are able to adapt when the context elements in which they are located change. These applications can change due to variations in their execution environment and inconsistent adaptations can occur, compromising the expected behavior. Then there is a need for creating a verification process to check the correctness and consistency of these SPLs as well as to check the correctness of both derived products and adapted products from these SPLs. Thus, this work proposes PRECISE - A Formal Verification Process for Feature Models of Mobile and Context-Aware Applications. PRECISE helps to identify defects in the variability modeling of an SPL for mobile and context-aware applications, minimizing problems that can take place during the execution of products generated from this SPL. It is worth noting that PRECISE is defined based on a formal specification and a set of well-formedness properties developed using First-Order Logic, which are prerequisites for the achievement of an unambiguous variability modeling. To evaluate PRECISE, a validation is performed from the formal specification and well-formedness properties defined in the process. This validation intends to show that PRECISE is able to identify defects, anomalies and inconsistencies in a variability model of an SPL for mobile and context-aware applications. In this validation, five different techniques are used: UML Profile, OCL, Propositional Logic, Prolog and Simulation. While minimizing the defects and inconsistencies in the variability models of an SPL, PRECISE still benefits from the generality and flexibility intrinsic to the formal notation used in its specification.
URI: http://www.repositorio.ufc.br/handle/riufc/18674
Appears in Collections:DCOMP - Teses defendidas na UFC

Files in This Item:
File Description SizeFormat 
2012_tese_fgmarinho.pdf4,98 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.