Cálculo de ambientes tipado sensível ao contexto para aplicações pervasivas
Fecha
2012-05-25Metadatos
Mostrar el registro completo del ítemResumen
Atualmente, a computação móvel está mais presente na rotina das pessoas. Celulares,
notebooks, smartphones e redes sem fio fazem parte do cotidiano. Com essa tecnologia disponível,
as pesquisas na área de computação pervasiva crescem a cada dia. A ideia da computação
pervasiva surgiu com um artigo escrito por Mark Weiser em 1991, com uma visão pessoal de
como seria a computação no século 21. Weiser descreveu que a computação faria parte do cotidiano
das pessoas, e estaria acessível em todos os ambientes. Além disso, seria tão natural
que passaria a ideia de estar invisível no ambiente. Para tornar a computação invisível, as
aplicações devem ser pró-ativas, solicitando o mínimo de intervenção do usuário para o seu
funcionamento. Um conceito importante que surge na computação pervasiva é a sensibilidade
ao contexto . Contexto é qualquer informação que possa ser utilizada para caracterizar
uma entidade. Com base em informações contextuais, as aplicações podem se adaptar dinamicamente
aos ambientes nos quais estão inseridas, tornando-se pró-ativas e transmitindo a
ideia da invisibilidade. Novas linguagens de programação ou até mesmo novos paradigmas
de programação estão sendo desenvolvidos, tentando tornar mais intuitiva a programação de
aplicações pervasivas. A maioria dessas linguagens tenta adicionar novas funcionalidades em
linguagens já existentes. Porém, alguns autores defendem que deveriam existir novos formalismos
que ajudem a modelar as propriedades dos sistemas pervasivos, em especial a sensibilidade
ao contexto. A descrição formal de um sistema modelado através de métodos formais pode ser
utilizada para demonstrar que algumas propriedades de um sistema estão corretamente modeladas.
Nesse sentido, este trabalho estuda um modelo formal que pode servir como base para
a especificação de novas linguagens de programação, chamado Cálculo de Ambientes Sensível
ao Contexto (CASC), proposto para descrever ambientes móveis e aplicações pervasivas. Outro
método formal que é utilizado para especificar linguagens de programação são os sistemas de
tipos. Sistemas de tipos ajudam a garantir que um sistema se comporta de acordo com a sua
especificação, ou seja, são uma maneira de provar formalmente a ausência de comportamentos
indesejados dentro de um sistema. Dessa forma, a principal contribuição deste trabalho é
a definição de um sistema de tipos para o CASC com o foco no controle de comunicação entre
processos. Como estudo de caso, dois cenários reais foram modelados utilizando o CASC,
demonstrando o uso do sistema de tipos desenvolvido. A propriedade preservation (ou subject
reduction) do sistema de tipos foi provada formalmente, demostrando que o sistema de tipos
está correto, ou seja, atingindo o objetivo principal do trabalho.
Palavras-chave: Sistema de Tipos. Cálculo de Ambientes. Computação Pervasiva. Sensibilidade
ao Contexto.