Nowadays, mobile computing is more present in daily life. Mobile phones, notebooks,
smart phones and wireless networks are part of everyday life. With this technology available,
the research in pervasive computing is growing. The idea of pervasive computing was introduced
by Mark Weiser in 1991, with a personal vision of how would be computing in the 21st
century. Weiser s idea was that information processing would become part of everyday life, and
would be available everywhere. Furthermore, it would be so natural as being invisible in the
ambient. To make computing invisible, applications must be proactive, asking for a minimum of
user intervention for its operation. An important concept that arises with pervasive computing is
the context awareness . Context is any information that can be used to characterize an entity.
Based on contextual information, applications can dynamically adapt to the environments in
which they operate, becoming proactive and conveying the idea of invisibility. New programming
languages or even new paradigms are being developed trying to make more intuitive the
programming of pervasive applications. Most of these programming languages attempt to add
new features into existing programming languages. However, some authors argue that there
must be new formalisms that help to model the properties of pervasive systems, in particular the
context awareness. The formal description of a system modeled by formal methods can be used
to demonstrate that some properties of the system are correctly modeled. In this sense, this work
studies a formal model that can be used as a basis for specifying a new programming language,
called Calculus of Context-aware Ambients (CCA), proposed to describe mobile and pervasive
applications. Another formal method used in the specification of programming languages are
the type systems. Type systems helps to ensure that the system behaves according to the specification,
that is, is a way to formally prove the absence of undesirable behavior in a system.
Thus, the main contribution of this work is the definition of a type system for the CCA with
the focus in the communication between processes. As a case study two real scenarios were
modeled using the CCA, demonstrating the use of the type system developed. The preservation
(or subject reduction) property of the type system was formally proved, demonstrating that the
type system is correct, i.e., achieving the main purpose of the present work. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsm.br:1/5401 |
| Date | 25 May 2012 |
| Creators | Pasqualin, Douglas Pereira |
| Contributors | Vizzotto, Juliana Kaizer, Moreira, álvaro Freitas, Piveta, Eduardo Kessler |
| Publisher | Universidade Federal de Santa Maria, Programa de Pós-Graduação em Informática, UFSM, BR, Ciência da Computação |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFSM, instname:Universidade Federal de Santa Maria, instacron:UFSM |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | 100300000007, 400, 300, 300, 300, 300, 05cfea7a-2f9a-458f-8d0a-d0ebfed22202, 586f7108-cb48-4aa4-963a-166a7c2c2a7b, 1d1b14ca-61c6-4466-9e47-8b6888c6a6ea, deff8c52-5f3b-4d6f-845c-f8292592f73c |
Page generated in 0.0026 seconds