Design, verification and documentation of concurrent systems

Abstract

The concept of invariant is the basis of most formal methods for the design and verification of concurrent systems. It can be noticed that invariants can also be used to give clear and concise descriptions of correct programs. As invariants are concerned only with the safety properties of systems, other formal objects have to be used to deal with liveness properties. Unfortunately, the formal objects generally used for liveness properties are somewhat inadequate, especially from the documentation point of view, A new family of formal objects, called proof graphs, is introduced. These graphs can be designed together with the corresponding program by stepwise refinement. They turn to be useful for specification, verification and documentation, but only the last point is emphasized in this paper and illustrated by an elementary example.