We exemplify a method for the formal derivation of multiprograms, using the simple theory of Owicki and Gries as our main tool for coping with concurrency. In our first and simple example we derive a protocol for the problem of Concurrent Vector Writing, and in our second and more tricky example we design a distributed algorithm for the problem of Liberal Phase Synchronization.
|Title of host publication||Mathematical methods in program development|
|Editors||M. Broy, B. Schieder|
|Publication status||Published - 1997|
|Name||NATO ASI, Series F: Computer and System Sciences|