School of Computing

Structural refinement in Object-Z / CSP

John Derrick and Graeme Smith

In W. Grieskamp, T. Stanten, and B. Stoddart, editors, Integrated Formal Methods (IFM 2000), volume 1945 of Lecture Notes in Computer Science, pages 182-196. Springer, November 2000.

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.

Download publication 146 kbytes (PostScript)

Bibtex Record

@inproceedings{1133,
author = {John Derrick and Graeme Smith},
title = {{Structural refinement in Object-Z / CSP}},
month = {November},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1133},
    booktitle = {Integrated Formal Methods (IFM 2000)},
    editor = {W. Grieskamp and T. Stanten and B. Stoddart},
    publication_type = {inproceedings},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    submission_id = {25297_974465128},
    volume = {1945},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014