Skip to main content
Erschienen in:
Buchtitelbild

2000 | OriginalPaper | Buchkapitel

Formal Verification of the TTP Group Membership Algorithm

verfasst von : Holger Pfeifer

Erschienen in: Formal Methods for Distributed System Development

Verlag: Springer US

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

This 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.

Metadaten
Titel
Formal Verification of the TTP Group Membership Algorithm
verfasst von
Holger Pfeifer
Copyright-Jahr
2000
Verlag
Springer US
DOI
https://doi.org/10.1007/978-0-387-35533-7_1