Esta dissertação de mestrado especifica os aspectos de mobilidade de um protocolo de comunicação para computação móvel usando o Ditributed Join-Calculus. A especificação foi utilizada para a verificação das características do protocolo com relação à mobilidade. Além disso, estudamos como o uso do Distrubuted Join-Calculus pode ajudar numa melhor visão e compreensão do comportamento de agentes móveis. O Join-Calculus é um modelo formal de concorrência, com conceitos de mobilidade e distribuição, que pode ser visto de duas formas: como um cálculo de processos e como uma linguagem de programação baseada em técncas de desenvolvimento formal. O formalismo utilizado foi o Distributed Join-Calculus, uma extensão do Join-Calculus com primitivas para mobilidade e localidades explícitas. O protocolo escolhido para a especificação foi o RDP (Result Delivery Protocol). Implementando o modelo para RDP, no Distributed Join-Calculus, em relação às características de mobilidade, analisamos e verificamos se algumas das propriedades esperadas pelo protocolo RDP são atendidas. Além disso, analisamos o uso do Distributed Join-Calculus com relação à especificação do protocolo e às dificuldades de se especificar um protocolo de mobilidade. Para isso, o nosso trabalho foi dividido em três fases: a especificação de um modelo simples e restrito das características de mobilidade do protocolo RDP, para um melhor entendimento do seu funcionamento e das propriedades que analisamos, a especificação deste protocolo de forma global, e a análise final com a verificação de algumas propriedades

not available