Abstract
In this paper we define a combination of Object-Z and CSP called CSP-OZ. The basic idea is to define a CSP-semantics for every Object-Z class. Special care is taken to capture the characteristics of input and output parameters properly and to preserve the expected refinement rules.
CSP-OZ is well suited for the specification and development of communicating distributed systems. It provides powerful techniques to model data-and control-aspects in a common framework. The language is easy to use for Z and Object-Z users.
Chapter PDF
References
E. Barros and A. Sampaio. Towards provably correct hardware/software codesign using OCCAM. In Proceedings of the Third International Workshop on Codesign. IEEE Computer Society Press, 1994.
E. Boiten, H. Bowman, J. Derrick, and M. Steen. Viewpoint consistency in Z and LOTOS: A case study. submitted for publication, 1997.
T. Bolognesi, J. van de Lagemaat, and C. Vissers, editors. LOTOSphere: Software Development with LOTOS. Kluwer Academic, 1995.
M. J. Butler. A CSP Approach To Action Systems. PhD thesis, University of Oxford, 1992.
J. Derrick, E.A. Boiten, H. Bowman, and M.W.A. Steen. Supporting ODP — translating LOTOS to Z. In First IFIP International workshop on Formal Methods for Open Object-based Distributed Systems. Chapmann & Hall, 1996.
R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17: 511–533, 1995.
C. Fischer. Combining CSP and Z. submitted for publication, 1997.
C. Fischer. Combining Object-Z and CSP. Technical report, University of Oldenburg, April 1997.
Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR 2, Dec 1995. Preliminary Manual.
S. Hallerstede. Die semantische Fundierung von CSP-Z. Master’s thesis, University of Oldenburg, January 1997. in german.
J. He. Process simulation and refinement. Formal Aspects of Computing, 1 (3): 229–241, 1989.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
M.B. Josephs. A state-based approach to communicating processes. Distributed Computing, 3: 9–18, 1988.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, LNCS 1125, pages 283–298. Springer Verlag, 1996.
B. Krieg-Bruckner, J. Peleska, E.-R. Olderog, D. Balzer, and A. Baer. UniForM — Universal Formal Methods Workbench. In U. Grote and G. Wolf, editors, Statusseminar des BMBF Softwaretechnologie, pages 357–378. BMBF, Berlin, March 1996.
C. Morgan. Programming from Specifications. Prentice Hall, 1990.
A. W. Roscoe. An alternative order for the failures model. In Two papers on CSP, Technical Monograph PRG-67, pages 1–26. Oxford University, 1988.
A. W. Roscoe and G. Barrett. Unbounded nondeterminism in CSP. In Mathematical Foundations of Programming Semantics, volume 442 of LNCS, pages 160–193. Springer-Verlag, 1989.
A. W. Roscoe, J. C. P. Woodcock, and L. Wulf. Non-interference through determinism. In D. Gollmann, editor, ESORICS 9.4, volume 875 of LNCS, pages 33–54. Springer-Verlag, 1994.
G. Smith. An Object-Oriented Approach to Formal Specification. PhD thesis, Department of Computer Science, University of Queensland, St. Lucia 4072, Australia, October 1992.
G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. submitted for publication, 1997.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International Series in Computer Science, 2nd edition, 1992.
B. Strulo. How firing conditions help inheritance. In J. P. Bowen and M. G. Hinchey, editors, ZUM ’85: The Z Formal Specification Notation, volume 967 of LNCS, pages 264–275, 1995.
H. Tej and B. Wolff. A corrected failure-divergence-model for CSP in Isabelle/HOL. submitted for publication, 1997.
J. C. P. Woodcock and C. C. Morgan. Refinement of state-based concurrent systems. In Proceedings of VDM Symposium 1990, volume 428 of LNCS, pages 340–351. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Fischer, C. (1997). CSP-OZ: A Combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds) Formal Methods for Open Object-based Distributed Systems. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35261-9_29
Download citation
DOI: https://doi.org/10.1007/978-0-387-35261-9_29
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2952-7
Online ISBN: 978-0-387-35261-9
eBook Packages: Springer Book Archive