Go backward to References
Go up to Top
Go 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  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.