PRECISE - Um processo de verificaÃÃo formal para modelos de caracterÃsticas de aplicaÃÃes mÃveis e sensÃveis ao contexto / PRECISE - A Formal Verification Process for Feature Models for Mobile and Context-Aware Applications
AUTOR(ES)
Fabiana Gomes Marinho
FONTE
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia
DATA DE PUBLICAÇÃO
27/08/2012
RESUMO
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.
ASSUNTO(S)
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 software product line mobile and context-aware computing verification and validation feature model formal verification software - desenvolvimento computaÃÃo mÃvel gerenciamento de configuraÃÃes de software software de aplicaÃÃo software - validaÃÃo
ACESSO AO ARTIGO
http://www.teses.ufc.br/tde_busca/arquivo.php?codArquivo=8478Documentos Relacionados
- Estudos das caracterÃsticas tribolÃgicas de filmes de DLC para aplicaÃÃes em sistema de lubrificaÃÃo seca.
- CaracterÃsticas de vento da regiÃo nordeste: AnÃlise, modelagem e aplicaÃÃes para projetos de centrais eÃlicas
- CMF: um framework multi-plataforma para desenvolvimento de aplicaÃÃes para dispositivos mÃveis
- Using ontological modeling in a context-aware summarization system to adapt text for mobile devices
- M-CODE: um modelo para mediÃÃo de confidencialidade e desempenho para aplicaÃÃes mÃveis seguras