Parametric Verification of a Group Membership Algorithm

TL;DR

This paper presents a parametric verification method for a group membership algorithm in the TTP protocol, ensuring the non-clique property for arbitrary station counts and fault numbers using automata models and automated tools.

Contribution

It introduces an abstraction using parametric counter automata to verify clique avoidance in the TTP protocol for any number of stations and faults.

Findings

Verified non-clique property for one fault case

Used ALV and LASH tools for automated model checking

Demonstrated the effectiveness of parametric automata modeling

Abstract

We address the problem of verifying clique avoidance in the TTP protocol. TTP allows several stations embedded in a car to communicate. It has many mechanisms to ensure robustness to faults. In particular, it has an algorithm that allows a station to recognize itself as faulty and leave the communication. This algorithm must satisfy the crucial 'non-clique' property: it is impossible to have two or more disjoint groups of stations communicating exclusively with stations in their own group. In this paper, we propose an automatic verification method for an arbitrary number of stations $N$ and a given number of faults $k$. We give an abstraction that allows to model the algorithm by means of unbounded (parametric) counter automata. We have checked the non-clique property on this model in the case of one fault, using the ALV tool as well as the LASH tool.