5th Irish Workshop on Formal Methods (IWFM)
Irish Workshop on Formal Methods
16-17 July 2001
This paper introduces the theory of Owicki and Gries as a method for the design (as opposed to the verification) of multiprograms (concurrent programs).
The theory is applied to a problem of barrier synchronisation for two (and more) programs. The problem is well chosen because it is easy to state yet not easy to solve, and it therefore shows the difficulties of multiprogram design very well.
The effectiveness of the theory to manage multiprogram design, and in the control of complexity, emerges quite well from the exercise.