Author(s):
Henriques, Daniela Pedro
Date: 2014
Persistent ID: http://hdl.handle.net/10451/15436
Origin: Repositório da Universidade de Lisboa
Subject(s): Sistemas distribuídos; Tolerância a falhas; Trocas de mensagens; Especificação de protocolos; Teses de mestrado - 2014
Description
Tese de mestrado, Engenharia Informática (Arquitectura, Sistemas e Redes de Computadores), Universidade de Lisboa, Faculdade de Ciências, 2014
Nos sistemas distribuídos tolerantes a falhas existem vários processos que comunicam entre si que podem falhar a qualquer momento, interferindo com o curso normal da comunicação, o que torna estes sistemas mais complexos e difíceis de implementar. Quando se escreve este código complexo todas as operações de comunicação têm que ser definidas de modo a que os processos saibam que operações executar, os tipos de mensagens e os processos envolvidos nas operações. Atualmente não existe nenhuma técnica comum para escrever este tipo de programas, assim cada programador usa as suas próprias técnicas, tornando este processo mais lento e difícil. Hoje em dia, são usadas diferentes abordagens para verificar que um programa que envolve trocas de mensagens está bem definido e funciona para cada situação possível. A abordagem mais comum consiste em passar o programa por uma série de testes criados pelo programador, o que pode demorado e pouco fiável pois é difícil testar todos os casos possíveis. Esta tese sugere uma abordagem que se certifica que o programa troca mensagens por uma ordem pré-estabelecida, mesmo na presença de falhas que afetam estas trocas, e que poderá tornar a verificação destes programas mais rápida e mais precisa. A nossa abordagem consiste em especificar todas as interações de comunicação através de uma linguagem de protocolos que descreve programas distribuídos tolerantes a falhas. Esta linguagem é usada para construir protocolos globais que especificam toda a comunicação do sistema. Através de regras de tradução, os protocolos globais são projetados para protocolos locais que especificam a comunicação do ponto de vista de cada processo. Por fim, é criado um programa que implementa as ações de cada um dos processos participantes no sistema. As operações de comunicação nestes programas seguem uma API da linguagem Erlang que definimos e que fornece uma forma comum de representar o envio/receção de mensagens. Usando esta API poderá ser possível futuramente fazer uma correspondência entre os protocolos locais e os programas de cada processo, de modo a verificar em tempo de compilação que os programas trocam mensagem por uma ordem correta.
Fault-tolerant distributed systems handle a variety of communication interactions between multiple participants that can fail at any moment, interfering with the normal flow of communications and therefore making the systems more complex to implement. When writing this complex code all communication operations need to be defined, so that participants know which operations they have to execute, the message types involved in the operations and who participates in the operations. Until today there is no common strategy to write this type of programs, so each programmer uses his own techniques, making the process slower and more difficult. Nowadays, to make sure that a message-passing program is well defined and works in every situation, it is possible to use different approaches. The most common consisting in passing a program through a series of tests, which can be time-consuming and lacks accuracy due to the difficulty of covering all possible cases. This thesys suggests an approach that makes sure a program exchanges messages in a pre-established order even in the presence of failures that affect the message-passing interactions. Besides, it could make the process of verifying a program faster and more accurate. It consists in specifying all the communication interactions using a language of protocols to describe fault-tolerant distributed systems. This language is used to create global protocols that specify all the communication of a system. Then translation rules are used to project global protocols into local protocols that specify the communication point of view of a process. Finally, for each process is created an individual program that implements its actions. The communication operations in these programs follow an API of the language Erlang that we created, which offers a common model to represent message-passing. In the future, we could use this API to find connections between the local protocols and the programs of each process that would help verify at compile time that the communication of the program is well defined.