  Group communication is becoming a more and more popular infrastructure for
efficient distributed applications. It consists in representing locally a group
of remote objects as a single object accessed in a single step; communications
are then broadcasted to all members. This paper provides models for automatic
verification of group-based applications, typically for detecting deadlocks or
checking message ordering. We show how to encode group communication, together
with different forms of synchronisation for group results. The proposed models
are parametric such that, for example, different group sizes or group members
could be experimented with the minimum modification of the original model.
