previous up next
Go backward to References
Go up to Top
Go forward to B Distributed Snapshots
RISC-Linz logo

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.

  • A.1 State Transitions
  • A.2 The Invariant
  • A.3 The Proof
  • A.4 Termination

  • Maintainer: Wolfgang Schreiner
    Last Modification: October 1, 1998

    previous up next