Go backward to ReferencesGo up to TopGo forward to B Distributed Snapshots |

The assertion presented here can (and should!) be also formally verified. In this appendix, we sketch a strategy how to prove properties of algorithms implemented with the facility of the DAJ toolkit. This strategy is based on the concept of Temporal Logic [7] but we deliberately avoid its formalism and sketch the ideas in natural language instead.

We focus on the proof of safety properties (properties that must
*always* hold); at the end of this section we will shortly discuss
liveness properties (properties that must *eventually*
hold). Here
we describe the design and verification of a more interesting distributed
algorithm.

Maintainer: Wolfgang Schreiner

Last Modification: October 1, 1998