# Structural refinement in Object-Z / CSP

Derrick, John and Smith, Graeme (2000) Structural refinement in Object-Z / CSP. In: Grieskamp, Wolfgang and Stanten, Thomas and Stoddart, Bill, eds. Integrated Formal Methods Second International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 194-213. ISBN 978-3-540-41196-3. E-ISBN 978-3-540-40911-3. (doi:10.1007/3-540-40911-4_12)

PDF
 Preview
Postscript
 Preview
Official URL
http://dx.doi.org/10.1007/3-540-40911-4_12

## Abstract

State-based refinement relations have been developed for use on the Object-Z components in an integrated Object-Z / CSP specification. However this refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would allow concurrency to be introduced during the development life-cycle. In this paper we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow a single Object-Z component to be refined to a number of communicating or interleaved classes. We prove soundness of these rules and illustrate them with a number of small examples.

Item Type: Book section 10.1007/3-540-40911-4_12 Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Faculties > Sciences > School of Computing > Theoretical Computing Group Mark Wheadon 13 Sep 2009 19:04 UTC 05 Sep 2019 11:14 UTC https://kar.kent.ac.uk/id/eprint/21935 (The current URI for this page, for reference purposes)