© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Relational concurrent refinement with internal operations
J. Derrick and E.A. Boiten
Electronic Notes in Theoretical Computer Science, 187:182-196, July 2007 Proceedings of Refine 2007, the 11th BCS-FACS Refinement Workshop. Editors: B. Aichernig, E.A. Boiten, J. Derrick and L. Groves.Abstract
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.
Bibtex Record
@article{2580,
author = {J. Derrick and E.A. Boiten},
title = {Relational Concurrent Refinement with Internal Operations},
month = {July},
year = {2007},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Proceedings of Refine 2007, the 11th BCS-FACS Refinement Workshop. Editors: B. Aichernig, E.A. Boiten, J. Derrick and L. Groves.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2007/2580},
publication_type = {article},
submission_id = {3341_1184342652},
ISSN = {15710661},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {187},
}