Abstract
Circus is a combination of Z, CSP, and Morgan’s refinement calculus; it has an associated refinement strategy that supports the development of reactive programs. In this work, we present rules to translate Circus programs to Java programs that use JCSP, a library that implements CSP constructs. These rules can be used as a complement to the Circus algebraic refinement technique, or as a guideline for implementation. They are a link between the results on refinement in the context of Circus and a practical programming language in current use. The rules can also be used as the basis for a tool that mechanises the translation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cavalcanti, A.L.C., Sampaio, A.C.A.: From CSP-OZ to Java with Processes (Extended Version). Technical report, Centro de Informática/UFPE (2000); Available at, http://www.cin.ufpe.br/~lmf
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2-3), 146–181 (2003)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)
Fischer, C.: Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, Fachbereich Informatik, Universität Oldenburg, Oldenburg - Germany (2000)
Galloway, A.J.: Integrated Formal Methods with Richer Methodological Profiles for the Development of Multi-perspective Systems. PhD thesis, University of Teeside, School of Computing and Mathematics (1996)
Hilderink, G., Broenink, J., Vervoort, W., Bakkers, A.: Communicating Java Threads. In: Parallel Programming and Java Conference (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
McEwan, A.A.: Concurrent Program Development. PhD thesis, Oxford University Computing Laboratory, Oxford - UK (to appear, 2000)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)
Oliveira, M.V.M.: A Refinement Calculus for Circus - Mini-thesis. Mini-thesis 8-04, University of Kent, Canterbury, CT2 7NF, UK (April 2004)
Oliveira, M.V.M.: From Circus to JCSP - Summation Example Source Code (2004); At, http://www.cs.kent.ac.uk/~mvmo2/circus/summation.pdf
Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Refining Industrial Scale Systems in Circus. In: East, I., Martin, J., Welch, P., Duce, D., Green, M. (eds.) Communicating Process Architectures. IOS Press, Amsterdam (to appear, 2004)
Welch, P.H., Stiles, G.S., Hilderink, G.H., Bakkers, A.P.: CSP for Java: Multithreading for All. In: Cook, B.M. (ed.) Architectures, Languages and Techniques for Concurrent Systems, Amsterdam, the Netherlands, April 1999. Concurrent Systems Engineering Series, vol. 57. IOS Press, Amsterdam (1999)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)
Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through Determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 33–54. Springer, Heidelberg (1994)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)
Taguchi, K., Araki, K.: The State-based CCS Semantics for Concurrent Z Specification. In: Hinchey, M., Liu, S. (eds.) International Conference on Formal Engineering Methods, pp. 283–292. IEEE, Los Alamitos (1997)
Woodcock, J.C.P.: Using Circus for Safety-Critical Applications. In: VI Brazilian Workshop on Formal Methods, Campina Grande, Brazil, October 12th–14st, pp. 1–15 (2003)
Woodcock, J.C.P., Cavancanti, A.L.C.: Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD UK (July 2001)
Woodcock, J.C.P., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Oliveira, M., Cavalcanti, A. (2004). From Circus to JCSP. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive