Design, verification and documentation of concurrent systems
(1991) 4th Refinement Workshop. Proceedings of the 4th Refinement Workshop — Location: Cambridge, UK (9.January.1991)
Files
No attached file found for this publication.
Details
- Authors
- 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 and illustrated by an elementary example.
- Affiliations
Citations
Gribomont, E. P. (1991). Design, verification and documentation of concurrent systems. In Morris, J.M.; Shaw, R.C.; (ed.), 4th Refinement Workshop. Proceedings of the 4th Refinement Workshop (p. p. 360-377). Springer-verlag. https://hdl.handle.net/2078.5/230468