Verification techniques for distributed algorithms
Date
2006Author
Philippou, AnnaMichael, G.
ISSN
0302-9743Source
10th International Conference on Principles of Distributed Systems, OPODIS 2006Volume
4305 LNCSPages
172-186Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
A value-passing, asynchronous process calculus and its associated theory of confluence are considered as a basis for establishing the correctness of distributed algorithms. In particular, we present an asynchronous version of value-passing CCS and we develop its theory of confluence. We show techniques for demonstrating confluence of complex processes in a compositional manner and we study properties of confluent systems that can prove useful for their verification. These results give rise to a methodology for system verification which we illustrate by proving the correctness of two distributed leader-election algorithms. © Springer-Verlag Berlin Heidelberg 2006.