Programming Research Group
Technical Report TR-1-99
TTP : a case study in combining induction and data independence
Sadie Creese and
A.W. Roscoe
January 1999, 21 pp.
Abstract
The TTP, or Time Triggered Protocol, is designed as an efficient mechanism for diagnosing faulty members of a network of peer processes. it exists in a number of versions and can be considered at a number of levels of abstraction. We take as our starting point the version presented by Katz et al in [10]. We first examine briefly how it can be modelled in CSP and particular instances analysed on FDR. This gives some useful insights into the model checking process and in particular the role of bisimulation as a compression mechanism, and also uncovers a flaw in the protocol as presented in the original version of [10]. We generalise the protocol in several ways to make it data independent in the types of nodes, and show how this can lead to an inductive proof that is checkable on FDR.
This paper is available as a 85633 gzipped PostScript file.