Go backward to References Go up to Top Go forward to B Distributed Snapshots

A Proving Assertions

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.