Skip to main content
Kent Academic Repository

More relational refinement: traces and partial relations

Derrick, John, Boiten, Eerke Albert (2008) More relational refinement: traces and partial relations. Electronic Notes in Theoretical Computer Science, 214 . pp. 255-276. ISSN 1571-0661. (doi:10.1016/j.entcs.2008.06.012) (KAR id:23978)


Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements. On the other hand, refinement in a process algebra takes a number of different forms depending on the exact notion of observation chosen, which can include the events a system is prepared to accept or refuse. In this paper we continue our program of deriving relational simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension.

Item Type: Article
DOI/Identification number: 10.1016/j.entcs.2008.06.012
Additional information: Proceedings of REFINE 2008 (Turku, May 2008)
Uncontrolled keywords: Data refinement, Z, process algebra, simulations, relations
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: 29 Mar 2010 12:09 UTC
Last Modified: 16 Nov 2021 10:02 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:

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.