Abstract
This paper presents a method of formally specifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to be used directly within the CSP part of the specification.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Benjamin. A message passing system. An example of combining CSP and Z. In J.E. Nicholls, editor, 4th Z Users Workshop, Workshops in Computing, pages 221–228. Springer-Verlag, 1989.
T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25–59, 1988.
S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984.
S.D. Brookes and A.W. Roscoe. An improved failures model for communicating processes. In Pittsburgh Symposium on Concurrency, volume 197 of Lecture Notes in Computer Science, pages 281–305. Springer-Verlag, 1985.
M.J. Butler and C.C. Morgan. Action systems, unbounded nondeterminism, and infinite traces. Formal Aspects of Computing, 7(1):37–53, 1995.
J. Derrick, H. Bowman, and M. Steen. Viewpoints and objects. In J. Bowen and M. Hinchey, editors, 9th International Conference of Z Users (ZUM'95), volume 967 of Lecture Notes in Computer Science, pages 449–468. Springer-Verlag, 1995.
J. Dong, R. Duke, and G. Rose. An object-oriented approach to the semantics of programming languages. In G. Gupta, editor, 17th Annual Computer Science Conference (ACSC'17), pages 767–775, 1994.
D. Duke and R. Duke. Towards a semantics for Object-Z. In D. Bjørner, C.A.R. Hoare, and H. Langmaack, editors, VDM'90: VDM and Z., volume 428 of Lecture Notes in Computer Science, pages 242–262. Springer-Verlag, 1990.
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.
H. Ehrich, J. Goguen, and A. Sernadas. A categorical theory of objects as observed processes. In J.W. Bakker, W.P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, volume 489 of Lecture Notes in Computer Science, pages 203–228. Springer-Verlag, 1991.
M. Nielsen et al. The RAISE language, methods and tools. Formal Aspects of Computing, 1:85–114, 1989.
J. He. Process refinement. In J. McDermid, editor, The Theory and Practice of Refinement. Butterworths, 1989.
M. Heisel and C. Sühl. Formal specification of safety-critical software with Z and real-time CSP. In E. Schoitsch, editor, Proceedings 15th International Conference on Computer Safety, Reliability and Security, pages 31–45. Springer, 1996.
C.A.R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, 1985.
ITU Recommendation X.901-904. Open Distributed Processing-Reference Model — Parts 1–4, July 1995.
C.B. Jones. Systematic Software Development using VDM. Series in Computer Science. Prentice-Hall International, 1986.
M.B. Josephs. A state-based approach to communicating processes. Distributed Computing, 3:9–18, 1988.
R. Milner. Communication and Concurrency. Series in Computer Science. Prentice-Hall International, 1989.
A.W. Roscoe. An alternative order for the failures model. Journal of Logic and Computation, 3(2), 1993.
A.W. Roscoe. Unbounded nondeterminism in CSP. Journal of Logic and Computation, 3(2), 1993.
M. Shaw and D. Garlan. Formulations and formalisms in software architecture. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 307–323. Springer-Verlag, 1996.
G. Smith. Extending W for Object-Z. In J. Bowen and M. Hinchey, editors, 9th International Conference of Z Users, volume 967 of Lecture Notes in Computer Science, pages 276–295. Springer-Verlag, 1995.
G. Smith. A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3):289–313, 1995.
G. Smith and J. Derrick. Refinement and verification of concurrent systems specified in Object-Z and CSP. Submitted for publication, 1997.
J.M. Spivey. The Z Notation: A Reference Manual (2nd Ed.). Series in Computer Science. Prentice-Hall International, 1992.
F.W. Vaandrager. Process algebra semantics for POOL. Technical Report CSR8629, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, 1991.
J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In D. Bjørner, C.A.R. Hoare, and H. Langmaack, editors, VDM'90: VDM and Z!, volume 428 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
A. Yonezawa and M. Tokoro, editors. Object-Oriented Concurrent Programming. MIT Press, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smith, G. (1997). A semantic integration of object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_4
Download citation
DOI: https://doi.org/10.1007/3-540-63533-5_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63533-8
Online ISBN: 978-3-540-69593-6
eBook Packages: Springer Book Archive