Cookies on this website

We use cookies to ensure that we give you the best experience on our website. If you click 'Accept all cookies' we'll assume that you are happy to receive all cookies and you won't see this message again. If you click 'Reject all non-essential cookies' only necessary cookies providing core functionality such as security, network management, and accessibility will be enabled. Click 'Find out more' for information on how to change your cookie settings.

In this paper we compare the refinement orderings, and their associated simulation rules, of state-based specification languages such as Z and Object-Z with the refinement orderings of event-based specification languages such as CSP. We prove with a simple counter-example that data refinement, established using the standard simulation rules for Z, does not imply failures refinement in CSP. This contradicts accepted results. Having explored the differences between the simulation rules for establishing data refinement and those for establishing the refinement of action systems and state-transition systems - models in which refinement is equivalent to failures refinement within CSP - we present a new set of simulation rules for data types. These alternative rules are both sound and jointly complete with respect to the stable failures refinement ordering. Furthermore we present an alternative refinement ordering for CSP, one in which refinement is equivalent to data, refinement in Z. © 2002 Published by Elsevier Science B. V.

Original publication

DOI

10.1016/S1571-0661(05)82563-0

Type

Journal article

Journal

Electronic Notes in Theoretical Computer Science

Publication Date

01/01/2002

Volume

70

Pages

297 - 310