Relational Concurrent Refinement - Partial and Total Frameworks

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 below, 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.