Circus Time with Reactive Designs

  • Kun Wei
  • Jim Woodcock
  • Ana Cavalcanti
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


The UTP theories for CSP and Circus can be built by the combination of the theories of designs and reactive processes. Defining the CSP operators using reactive design provides a more concise, readable and uniform UTP semantics, and, more importantly, exposes the pre-postcondition semantics of the operators. For Circus Time, a few operators have been defined as reactive designs, but some important operators are still be considered. In this paper, we develop the reactive design semantics of sequential composition, hiding and recursion within Circus Time, and show how to prove some subtle laws using the new semantics.


Circus Time UTP reactive designs 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cavalcanti, A., Wellings, A., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in Circus. In: Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES 2011, pp. 20–29. ACM, New York (2011)CrossRefGoogle Scholar
  2. 2.
    Cavalcanti, A., Woodcock, J.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2-3), 146–181 (2003)zbMATHCrossRefGoogle Scholar
  4. 4.
    Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle/Circus: a Process Specification and Verification Environment. Technical Report 1547, LRI, Université Paris-Sud XI (November 2011),
  5. 5.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)Google Scholar
  6. 6.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall International (1998)Google Scholar
  7. 7.
    Locke, D., et al.: Safety Critical Java Specification. First Release 0.76, The Open Group, UK (2010)Google Scholar
  8. 8.
    Morgan, C.: Programming from specifications. Prentice-Hall, Inc., Upper Saddle River (1990)zbMATHGoogle Scholar
  9. 9.
    Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP Semantics for Circus. Formal Aspects of Computing 21(1), 3–32 (2007)CrossRefGoogle Scholar
  10. 10.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International (1998)Google Scholar
  11. 11.
    Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons (1999)Google Scholar
  12. 12.
    Sherif, A., Cavalcanti, A.L.C., Jifeng, H., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing 22(2), 153–191 (2010)zbMATHCrossRefGoogle Scholar
  13. 13.
    Wei, K., Woodcock, J., Cavalcanti, A.: New Circus Time. Technical report, Department of Computer Science, University of York, UK (March 2012),
  14. 14.
    Woodcock, J.: The Miracle of Reactive Programming. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 202–217. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River (1996)zbMATHGoogle Scholar
  16. 16.
    Woodcock, J., Cavalcanti, A.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Woodcock, J., Cavalcanti, A.: A concurrent language for refinement. In: Butterfield, A., Pahl, C. (eds.) IWFM 2001: 5th Irish Workshop in Formal Methods, BCS Electronic Workshops in Computing, Dublin, Ireland (July 2001)Google Scholar
  18. 18.
    Woodcock, J., Cavalcanti, A.: The Semantics of $ Circus$. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Kun Wei
    • 1
  • Jim Woodcock
    • 1
  • Ana Cavalcanti
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations