Applying Refinement Calculi to Software Process Modelling

A refinement calculus provides a number of advantages to program development, besides correctness, like clarification of the goals of the program and effective documentation of the design choices. In this paper, we provide evidence that the same advantages can be obtained also in the case of those special programs that are known as enactable process models. The evidence is put forward by means of an example, a small Concurrent Engineering problem inspired to the IWSP7 problem. We assume that the enactment is done by rules in tuple spaces, and use a refinement calculus based on a temporal logic that builds on that of Unity. Finally, we show how the approach leads to seamless integration with existing process engines (the Oikos one in our case).