Título: Cálculo de Ambientes Tipado Sensível ao Contexto para Aplicações Pervasivas

Aluno: Douglas Pereira Pasqualin

Orientadora: Profa. Juliana Kaizer Vizzotto

Juliana Kaizer Vizzotto, Dra. (UFSM) (Presidente/Orientadora)

Álvaro Freitas Moreira, Dr. (UFRGS)

Eduardo Kessler Piveta, Dr. (UFSM)

Iara Augustin, Dra. (UFSM) – Suplente

Data: 25/05/2012

Hora: 14:30

Local: Sala 321

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 pode ser utilizada para caracterizar uma entidade. Com base em informações contextuais, as aplicações podem se adaptar dinamicamente aos ambientes em que estão inseridas, tornando-se pró-ativas e transmitindo a ideia da invisibilidade. Novas linguagens de programação ou até mesmo novos paradigmas estão sendo desenvolvidos, tentando tornar mais intuitiva a programação de aplicações pervasivas. A maioria dessas linguagens tentam adicionar novas funcionalidades em linguagens já existentes. Porém, alguns autores defendem que devem 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 do sistema estão corretamente modeladas. Nesse sentido, este trabalho estuda um modelo formal que pode servir como base para 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. Sistema de tipos ajudam a garantir que um sistema se comporta de acordo com a sua especificação, ou seja, é 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 foram modelados dois cenários reais utilizando o CASC, demonstrado 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.