Um mecanismo de comunicação de grupo é um serviço útil para a implementaçào de sistemas distribuídos, mas poucos trabalhos se preocuparam em especificar formalmente os protocolos usados para sua implementação. Esta dissertação descreve o protocolo de comunicação de grupo que foi implementado e os métodos formais usados. Foi implementado um protocolo de difusão de mensagens (broadcast) atômico usando um protocolo de confirmação em duas fases (two-phase commit) que seja tolerante a falhas. Este sistema foi escrito na linguagem Concert/C por causa do seu apoio para a comunicação entre processo Unix. Inicialmente, foi desenvolvido uam especificação formal para o protocolo e mostrada a sua validade. Em seguida, casos teste para a implementação final foram gerados a partir da especificação. A implementação do protocolo foi testada usando o conjunto de testes criados para mostrar sua conformidade com a especificaçào original

A group communication mechanism is a useful service for implementing distributed systems, but little work has been done in formally specifying and testing the protocols used to implement such mechanisms. This work dissertation describes the group-communication protocol that was implemented and the formal methods used. A fault tolerant two-phase-commit atomic-broadcast was implemented. Concert/C was the chosen implementation language because of its communication support for Unix processes. First a formal specification for the protocol was developed, and its validity was established. Next, test cases for the final implementation were generated from the specification. The protocol implementation was tested using the already-created test suite to show its conformance to the original specification