Skip to main content
Kent Academic Repository

Relational Concurrent Refinement - partial and total frameworks

Derrick, John and Boiten, Eerke Albert (2016) Relational Concurrent Refinement - partial and total frameworks. In: Petre, Luigia and Sekerinski, Emil, eds. From Action Systems to Distributed Systems: The Refinement Approach. Taylor and Francis, Florida, USA, pp. 143-154. ISBN 978-1-4987-0158-7. (doi:10.1201/b20053-15) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:51618)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:


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.

Item Type: Book section
DOI/Identification number: 10.1201/b20053-15
Uncontrolled keywords: refinement, process algebra, state-based systems, concurrency, simulation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
University-wide institutes > Institute of Cyber Security for Society
Depositing User: Eerke Boiten
Date Deposited: 10 Nov 2015 00:50 UTC
Last Modified: 09 Mar 2023 11:34 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Boiten, Eerke Albert.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.