A formal transformation and refinement method for concurrent programs

We describe a formal approach to the modelling of existing concurrent software systems, together with a theory of program equivalence and refinement. From this basis, we show how correctness-preserving transformations and refinements may be developed and proved, allowing us to change the structure of concurrent programs whilst preserving their functional behaviour. We then demonstrate the application of transformations to a simple concurrent program implementing a mutual exclusion algorithm, to illustrate its restructuring into a simpler form, and outline how the formal modelling of the program allows us to derive safety and liveness properties