Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-28T04:11:10.392Z Has data issue: false hasContentIssue false
  • English
  • Français

Parametric Verification of a Group Membership Algorithm

Published online by Cambridge University Press:  11 May 2006

AHMED BOUAJJANI  and
AGATHE MERCERON
AHMED BOUAJJANI
Affiliation:
LIAFA, University of Paris 7, Case 7014, 2 place Jussieu, 75251 Paris 5, France (e-mail: [email protected])
AGATHE MERCERON
Affiliation:
LIAFA and ESILV-GI, Technical University Leonard de Vinci, 92916 Paris La Défense, France (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

Formal verificationfault-tolerant protocolsparametric counter automataabstraction
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 6 , Issue 3 , May 2006 , pp. 321 - 353
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)