4. Empirical Findings and Analysis
4.6 Environmental Attractiveness
Visando possibilitar a an´alise dos MCs, estudos na literatura inclu´ıdos na primeira catego- ria prop˜oem a transforma¸c˜ao desses MCs para nota¸c˜oes formais. Segundo [22], as quatro propostas mais promissoras para a an´alise de um MC s˜ao baseadas no mapeamento dos MCs para Satisfiability (SAT) [53], CSP [30], Binary Decision Diagram (BDD) [37] e Ontologia [55].
Na Ciˆencia da Computa¸c˜ao, “satisfazibilidade” (SAT ) [53] corresponde ao pro- blema de estabelecer se as vari´aveis de uma f´ormula Booleana ou Proposicional podem ser atribu´ıdas de modo a fazer a mesma avaliar como verdadeira. Igualmente importante ´e a quest˜ao de determinar se n˜ao existem atribui¸c˜oes, o que implicaria que a fun¸c˜ao expressa pela f´ormula ´e falsa para todas as atribui¸c˜oes poss´ıveis vari´aveis. Nesse ´ultimo caso, a fun¸c˜ao ´e “insatisfaz´ıvel” [53].
Outros estudos prop˜oem a transforma¸c˜ao de um MC para CSP [30] que s˜ao problemas matem´aticos definidos como um conjunto de objetos cujo estado deve satisfazer uma s´erie de restri¸c˜oes ou limita¸c˜oes. CSP representa as entidades em um problema como um conjunto homogˆeneo de restri¸c˜oes finitas sobre vari´aveis, que ´e resolvido por m´etodos
de satisfa¸c˜ao de restri¸c˜ao [29]. Em geral, o uso de CSP est´a associado a t´ecnicas de programa¸c˜ao restritiva. A programa¸c˜ao restritiva ´e um paradigma que se refere ao uso de restri¸c˜oes na constru¸c˜ao de rela¸c˜oes entre vari´aveis. Consiste em especificar para uma solu¸c˜ao que crit´erios (restri¸c˜oes) esta tem de cumprir. De uma forma geral, as restri¸c˜oes s˜ao implementadas como uma extens˜ao de uma linguagem j´a existente. Essas operam sobre dom´ınios espec´ıficos, sendo os mais usuais: booleanos, n´umeros inteiros e racionais, lineares, finitos e mistos (v´arios dos anteriores). Apesar dos v´arios dom´ınios dispon´ıveis, o mais usado ´e o dom´ınio finito. Na pr´atica, o interpretador cria inicialmente o dom´ınio para as vari´aveis do problema e restringe cada dom´ınio `a medida que avalia as restri¸c˜oes. Ao final desse processo, obtˆem-se uma ou v´arias solu¸c˜oes que satisfa¸cam as restri¸c˜oes ou, caso essas n˜ao sejam “satisfaz´ıveis”, nenhuma solu¸c˜ao [29].
Uma estrat´egia diferente prop˜oe transformar um MC para um BDD [37], que ´e um grafo ac´ıclico dirigido com v´ertices n˜ao terminais, arcos e dois v´ertices terminais, o qual permite representar e manipular fun¸c˜oes booleanas. Os v´ertices n˜ao terminais possuem vari´aveis bin´arias e os arcos que saem desses v´ertices s˜ao rotulados com 0 ou 1. Um v´ertice terminal ´e rotulado com 0 e o outro com 1, representando os valores booleanos falso e verdadeiro. Como cada v´ertice n˜ao terminal representa uma vari´avel da fun¸c˜ao, para descobrir o valor atribu´ıdo a uma determinada entrada da fun¸c˜ao basta percorrer o grafo a partir da raiz at´e um terminal. Os valores das vari´aveis bin´arias definem um caminho no grafo que pode levar ao terminal rotulado com 1 ou ao terminal rotulado com 0. Ao longo de um caminho, se uma vari´avel de controle vale 0, deve-se seguir o arco rotulado com 0 e, se vale 1, o arco rotulado com 1. Da´ı a express˜ao decis˜ao bin´aria, porque cada n´o n˜ao terminal s´o tem dois sucessores poss´ıveis [36].
Outra abordagem prop˜oe um conjunto de regras para traduzir os MCs em ontologias que s˜ao processadas usando ferramentas espec´ıficas para executar a an´alise autom´atica das representa¸c˜oes dos MCs. Uma ontologia, denominada OWL-DL [55], foi definida para formalizar os MCs, checar a consistˆencia e detectar conflitos no MC por meio de regras pr´e-definidas. Por exemplo, Zaid et al. [158] fornecem uma especifica¸c˜ao formal para MCs baseada em ontologia. Esses autores fornecem meios para integrar os modelos, verificar a consistˆencia e detectar conflitos. Eles prop˜oem o uso de OWL para modelagem e o Reasoner Pellet [116] para a an´alise.
vadores de Teoremas1
. Exemplos de Provadores de Teoremas incluem SAT Solvers, exclusivos para problemas especificados usando l´ogica proposicional (SAT ), CSP Solvers, voltados para problemas descritos usando programa¸c˜ao restritiva, ou BDD Solvers, usados para solucionar problemas especificados usando diagramas de decis˜ao bin´aria [65].
Os trabalhos relacionados na segunda categoria abordam o desenvolvimento de aplica¸c˜oes geradas a partir uma LPMSC e que permitem o acesso transparente `a informa- ¸c˜ao atrav´es de dispositivos diferentes e heterogˆeneos, visando possibilitar a adapta¸c˜ao [152]. A adapta¸c˜ao de software est´a relacionada ao processo necess´ario para modificar uma aplica¸c˜ao, incluindo a detec¸c˜ao de mudan¸cas no contexto, tais como eventos e infor- ma¸c˜oes que podem levar `a uma mudan¸ca, planejamento e execu¸c˜ao dessas mudan¸cas na aplica¸c˜ao. Em geral, a literatura classifica a adapta¸c˜ao de software em dois tipos: adap- ta¸c˜ao est´atica e adapta¸c˜ao dinˆamica. A adapta¸c˜ao est´atica se refere `a mudan¸cas que s˜ao realizadas em tempo de desenvolvimento. A adapta¸c˜ao dinˆamica refere-se `a mudan¸cas que ocorrem enquanto a aplica¸c˜ao est´a em execu¸c˜ao [101].
Na terceira categoria, est˜ao agrupadas as abordagens que relacionam as t´ecni- cas de modelagem que tˆem sido usadas para a constru¸c˜ao e manuten¸c˜ao de MCs comple- xos. Essas t´ecnicas consistem em dividir os MCs em modelos menores e mais gerenci´aveis. No entanto, uma necessidade intr´ınseca `a essa t´ecnica est´a em garantir que as rela¸c˜oes semˆanticas entre os elementos das diferentes vis˜oes sejam preservadas. Dessa forma, ´e ne- cess´ario garantir a corretude e a consistˆencia dos modelos constru´ıdos, a consistˆencia dos relacionamentos semˆanticos entre esses modelos e a corretude dos produtos configurados e dos produtos adaptados devido `a mudan¸cas no contexto.