© University of Kent - Contact | Feedback | Legal
The University of Kent, Canterbury, Kent, CT2 7NZ, T +44 (0)1227 764000
Modelling divergence in relational concurrent refinement
E.A. Boiten and J. Derrick
In M. Leuschel and H. Wehrheim, editors, IFM 2009: Integrated Formal Methods, volume 5423 of LNCS, pages 183-199. Springer Verlag, February 2009 [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 investigate how divergence can be modelled relationally, and in particular show how differing process algebraic interpretations of divergence can be embedded in a relational framework. In doing so we derive relational simulation conditions for process algebraic refinement incorporating divergence.Bibtex Record
@inproceedings{2838,
author = {E.A. Boiten and J. Derrick},
title = {Modelling divergence in Relational Concurrent Refinement},
month = {February},
year = {2009},
pages = {183-199},
keywords = {Data refinement, simulations, internal operations, process algebraic refinement preorders, divergence},
note = {},
doi = {10.1007/978-3-642-00255-7_13},
url = {http://www.cs.kent.ac.uk/pubs/2009/2838},
publication_type = {inproceedings},
submission_id = {727_1225665750},
booktitle = {IFM 2009: Integrated Formal Methods},
editor = {M. Leuschel and H. Wehrheim},
series = {LNCS},
publisher = {Springer Verlag},
refereed = {yes},
volume = {5423},
}