Relational Concurrent Refinement - partial and total frameworks

Data refinement as found in a state-based language such as Z or B, and refinement as defined in a process algebra may appear as very different notions. Data refinement is defined using a relational model in terms of the behaviour of abstract programs, whereas in models of concurrency, refinement is often defined in terms of sets of observations. The methodologies used to verify them are also different: downward and upward simulations for data-refinement, whereas calculation of traces, refusals etc from the semantics is prevalent in a process algebra.

In this chapter we discuss work undertaken to reconcile the two approaches. Specifically, we show how one can embed concurrent semantics into a relational framework. This not only articulates the relationship between the two, but allows event-wise verification methods for concurrent refinement

relations to be derived. We discuss how this can be achieved, with particular emphasis on the type of relational model used - specifically whether one uses a model containing total relations, or one in which relations may be partial. Both are shown to have limits in expressiveness, and because of this we introduce a more general framework for simulations, called process data types.