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 …