Skip to main content

Relational Concurrent Refinement with Internal Operations

Derrick, John, Boiten, Eerke Albert (2007) Relational Concurrent Refinement with Internal Operations. Electronic Notes in Theoretical Computer Science, 187 . pp. 35-53. ISSN 1571-0661. (doi:10.1016/j.entcs.2006.08.043) (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:14564)

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 in a state-based language such as Z is defined using a relational model in terms of the input-output behaviour of abstract programs. Downward and upward simulations form a sound and jointly complete methodology for verifying relational data refinements. Refinement in a concurrent context, for example, as found in a process semantics, takes a number of different forms. Typically this is based on a notion of observation, for example, which events a system is prepared to accept or refuse. Concurrent refinement relations include trace refinement, failures-divergences refinement, readiness refinement and bisimulation. In this paper we survey recent results linking the relational model of refinement to the process algebraic models. Specifically, we detail how variations in the relational framework lead to relational data refinement being in correspondence with traces-divergences, singleton failures and failures-divergences refinement in a process semantics. We then extend these results by showing how the effect of internal operations can be incorporated into the relational model. As a consequence simulation rules for failures-divergences refinement can be derived.

Item Type: Article
DOI/Identification number: 10.1016/j.entcs.2006.08.043
Additional information: Proceedings of Refine 2007, the 11th BCS-FACS Refinement Workshop. Editors: B. Aichernig, E.A. Boiten, J. Derrick and L. Groves.
Uncontrolled keywords: Z, CSP, refinement, internal operations, concurrency, divergence
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 24 Nov 2008 18:04 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: (The current URI for this page, for reference purposes)
Boiten, Eerke Albert:
  • Depositors only (login required):

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