Behavioural Models for Group Communications

TL;DR

This paper introduces models for automatically verifying group communication systems in distributed applications, focusing on deadlock detection and message ordering, with flexible parameters for different group configurations.

Contribution

It presents novel parametric models that enable automatic verification of group communication protocols, accommodating various group sizes and synchronization methods.

Findings

Models effectively detect deadlocks in group communication

Models verify message ordering constraints

Flexible for different group sizes and synchronization types

Abstract

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.