© University of Kent - Contact | Feedback | Legal | FOI | Cookies
More relational refinement: traces and partial relations
J. Derrick and E.A. Boiten
Electronic Notes in Theoretical Computer Science, 214:182-196, May 2008 Proceedings of REFINE 2008 (Turku, May 2008) [doi].Abstract
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.
Bibtex Record
@article{2722,
author = {J. Derrick and E.A. Boiten},
title = {More relational refinement: traces and partial relations},
month = {May},
year = {2008},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Proceedings of REFINE 2008 (Turku, May 2008)},
doi = {10.1016/j.entcs.2008.06.012},
url = {http://www.cs.kent.ac.uk/pubs/2008/2722},
publication_type = {article},
submission_id = {25060_1209075284},
ISSN = {1571-0661},
volume = {214},
journal = {Electronic Notes in Theoretical Computer Science},
}