Structural refinement in Object-Z / CSP

Derrick, J. and Smith, G. (2000) Structural refinement in Object-Z / CSP. In: Grieskamp, W. and Stanten, T. and Stoddart, B., eds. Proceedings of the Second International Conference on Integrated Formal Methods. Lecture Notes in Computer Science, 1945. Springer pp. 194-213. ISBN 3-540-41196-8 . (Full text available)

PDF
Download (179kB)
[img]
Preview
Postscript
Download (150kB)
[img]
Preview

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: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 13 Sep 2009 19:04
Last Modified: 12 Jun 2012 12:55
Resource URI: http://kar.kent.ac.uk/id/eprint/21935 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year