University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Our PVS papers

Formal Verification of the TTP Group Membership Algorithm

Holger Pfeifer

Presented at the
IFIP TC6/WG6.1 International Conference on
Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII)
and
Protocol Specification, Testing and Verification (PSTV XX)
FORTE/PSTV2000
Pisa, Italy, October 10-13, 2000
© Kluwer Academic Publishers

 Abstract

The paper describes the formal verification of a fault-tolerant group membership algorithm that constitutes one of the central services of the Time-Triggered Protocol (TTP). The group membership algorithm is formally specified and verified using a diagrammatic representation of the algorithm. We describe the stepwise development of the diagram and outline the main part of the correctness proof. The verification has been mechanically checked with the PVS theorem prover.

 Online Copy

  • Paper:
    Available as Postscript (188 KB) or gzip'ed Postscript (71 KB)

  • PVS specification and proof files:
    Save the dump file membership.dump (289 KB, or gzip'ed, 26 KB) in a new directory.
    It contains a strategy file pvs-strategies so be careful not to overwrite your own. Unpack the theories with M-x undump-pvs-files. The top-level theory is ttp.pvs.

 BibTeX Entry

  
@InProceedings{Pfe00,
  author =    "Holger Pfeifer",
  title =     "Formal Verification of the TTP Group Membership Algorithm",
  year =      2000,
  booktitle = "Formal Methods for Distributed System Development
               Proceedings of FORTE XIII / PSTV XX 2000",
  editor =    "Tommaso Bolognesi and Diego Latella",
  pages =     "3--18",
  publisher = "Kluwer Academic Publishers",
  address =   "Pisa, Italy",
  month =     "October"
}

Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - October 16, 2000