Métodos para Especificação Formal de Sistemas Distribuídos


Lorena Santiago
Laboratório de Sistemas Distribuídos(LaSiD) - CPD/UFBA



Apresentação da descrição do funcionamento dos protocolos de comunicação entre processos distribuídos: Protocolo de validação em duas fases (Two Phase Commit Protocol) e Protocolo de ordem causal relativa da plataforma BCG (Base Confiável de Comunicação em Grupo), com suas respectivas especificações, utilizando as linguagens algébricas, LOTOS (Language of Temporal Ordering Specification) e CSP (Communicating Sequential Processes). O primeiro protocolo trata da validação ou não de transações computacionais, cujos agentes estão espalhados por vários componentes de um sistema distribuído. Já o segundo trata de sincronizar a comunicação em grupo, respeitando a ordem causal das mensagens, trocadas entre os processos que compõem o grupo.