Abstract
Refinement is one of the most important techniques in formal system design, supporting stepwise development of systems from abstract specifications into more concrete implementations. Non-atomic refinement is employed when the level of granularity changes during a refinement step, i.e., whenever an abstract operation is refined into a sequence of concrete operations, as opposed to a single concrete operation. There has been some limited work on non-atomic refinement in Z, and the purpose of this paper is to extend this existing theory. In particular, we strengthen the proposed definition to exclude certain behaviours which only occur in the concrete specification but have no counterpart on the abstract level. To do this we use coupled simulations: the standard simulation relation is complemented by a second relation which guarantees the exclusion of undesired behaviour of the concrete system. These two relations have to agree at specific points (coupling condition), thus ensuring the desired close correspondence between abstract and concrete specification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial. The B-Book: Assigning Programs to Meanings. CUP, 1996.
L. Aceto. Action Refinement in Process Algebras. CUP, London, 1992.
L. Aceto and M. Hennessy. Towards action-refinement in process algebras. Information and Computation, 103:204–269, 1993.
E. A. Boiten and J. Derrick. IO-refinement in Z. In A. Evans, D. J. Duke, and T. Clark, editors, 3rd BCS-FACS Northern Formal Methods Workshop. Springer-Verlag, September 1998. http://www.ewic.org.uk/.
W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. CUP, 1998.
J. Derrick and E. Boiten. Non-atomic refinement in Z. In J. Woodcock and J. Wing, editors, FM’99, World Congress on Formal Methods, number 1709 in LNCS, pages 1477–1496. Springer, 1999.
J. Derrick and E. A. Boiten. Refinement in Z and Object-Z. Springer-Verlag, 2001.
C. Fischer. CSP-OZ — a combination of CSP and Object-Z. In H. Bowman and J. Derrick, editors, Second IFIP International conference on Formal Methods for Open Object-based Distributed Systems, pages 423–438. Chapman & Hall, July 1997.
C. Fischer. How to combine Z with a process algebra. In ZUM’98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 5–23. Springer-Verlag, September 1998.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
C. B. Jones. Systematic Software Development using VDM. Prentice Hall, 1989.
J. Parrow and P. Sjödin. Multiway Synchronisation Verified with Coupled Simulation. In R. Cleaveland, editor, CONCUR’ 92, Concurrency Theory, number 630 in LNCS, pages 518–533. Springer, 1992.
A. Rensink. Action Contraction. In C. Palamidessi, editor, CONCUR 2000 — Concurrency Theory, number 1877 in LNCS, pages 290–304. Springer, 2000.
A. Rensink and R. Gorrieri. Action refinement as an implementation relation. In M. Bidoit and M. Dauchet, editors, TAPSOFT’ 97: Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 772–786, 1997.
G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97 Industrial Application and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science, pages 62–81. Springer-Verlag, September 1997.
G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems — an integration of Object-Z and CSP. Formal Methods in Systems Design, 18:249–284, May 2001.
J. M. Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice Hall, 2nd edition, 1992.
S. Stepney, D. Cooper, and J. C. P. Woodcock. More powerful data refinement in Z. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 284–307. Springer-Verlag, September 1998.
H. Treharne and S. Schneider. Using a process algebra to control B operations. In K. Araki, A. Galloway, and K. Taguchi, editors, International Conference on Integrated Formal Methods 1999 (IFM’99), pages 437–456, York, July 1999. Springer.
R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, volume 379 of LNCS, pages 237–248. Springer, 1989.
Walter Vogler. Failure semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139–162, 1991.
J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Wehrheim, H. (2003). Using Coupled Simulations in Non-atomic Refinement. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds) ZB 2003: Formal Specification and Development in Z and B. ZB 2003. Lecture Notes in Computer Science, vol 2651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44880-2_10
Download citation
DOI: https://doi.org/10.1007/3-540-44880-2_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40253-4
Online ISBN: 978-3-540-44880-8
eBook Packages: Springer Book Archive