Verification and refinement of distributed programs in a fair framework

In this paper, we present a technique to prove progress properties of non-terminating concurrent programs and to refine them in such a way that these properties are preserved. We rely on strong fairness assumptions about the language implementation.We define a simple language based on Hoare-78 CSP. A program denotes a set of finite and infinite traces corresponding to all its possible computations. The semantics of a program is defined as the set of its fair traces. We also give a liveness-preserving implementation notion. Proof rules concerning progress properties and correction of refinements are given. We show that these proof rules are consistent with the given fair semantics. Finally, we verify and refine a non-trivial case study.