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 small example. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Derrick, J., & Smith, G. (2000). Structural refinement in object-Z / CSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1945 LNCS, pp. 194–213). Springer Verlag. https://doi.org/10.1007/3-540-40911-4_12
Mendeley helps you to discover research relevant for your work.