Abstract
Over the years, the Circus family of notation has been used for specification, programming, and verification by refinement in many applications. Circus Time, a timed variant of Circus, plays a key role in dealing with timed behaviours. While most of the semantic developments of Circus Time have tended to focus on the denotational and operational sides, the work on its algebraic semantics is frustrated by the fact that the parallel operators are difficult to be reduced to other primitives in both discrete-time and continuous-time CSP models. In this paper, we present an algebraic operational semantics (AOS) of the discrete-time CSP in Circus Time. The related AOS form is identified in the timed context, and a complete set of algebraic laws are provided to transform any finite Circus Time programs into the AOS form. The AOS provides a solution to sequentialise the parallel operators and is also the major step towards a fully algebraic semantics.
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.
Similar content being viewed by others
References
Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: essays in Honour of C.A.R. Hoare, ch. 21. Prentice-Hall (1994)
Cavalcanti, A., Clayton, P., O’Halloran, C.: From control law diagrams to ada via circus. Formal Asp. Comput. 23(4), 465–512 (2011)
Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2–3), 146–181 (2003)
Cavalcanti, A., Zeyda, F., Wellings, A.J., Woodcock, J., Wei, K.: Safety-critical java programs from circus models. Real-Time Systems 49(5), 614–667 (2013)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Unifying Classes and Processes. Software and System Modelling 4(3), 277–296 (2005)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall International (1998)
Lowe, G., Ouaknine, J.: On timed models and full abstraction. Electron. Notes Theor. Comput. Sci. 155, 497–519 (2006)
Miyazawa, A., Cavalcanti, A.: Refinement-based verification of sequential implementations of stateflow charts. In: Refine, pp. 65–83 (2011)
Morgan, C.: Programming from specifications. Prentice-Hall Inc., Upper Saddle River (1990)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP Semantics for Circus. Formal Aspects of Computing 21(1), 3–32 (2007)
Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. PhD thesis, Oxford University, UK (2001)
Ouaknine, J., Schneider, S.: Timed csp: A retrospective. Electr. Notes Theor. Comput. Sci. 162, 273–276 (2006)
Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer-Verlag New York Inc., New York (2010)
Roscoe, A.W.:. The Theory and Practice of Concurrency. Prentice-Hall International (1998)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons (1999)
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)
Wei, K., Woodcock, J., Burns, A.: A timed model of Circus with the reactive design miracle. In: 8th International Conference on Software Engineering and Formal Methods (SEFM), pp. 315–319. IEEE Computer Society, Pisa (2010)
Wei, K., Woodcock, J., Burns, A.: Modelling temporal behaviour in complex systems with timebands. Formal Methods in System Design 43(3), 520–551 (2013)
Wei, K., Woodcock, J., Cavalcanti, A.: Circus Time with reactive designs. In: UTP, pp. 68–87 (2012)
Wei, K., Woodcock, J., Cavalcanti, A.: New Circus Time. Technical report, Computer Science, University of York, UK (2012). http://www.cs.york.ac.uk/circus/hijac/publication.html
Wei, K., Woodcock, J., Cavalcanti, A.: Operational Semantics for Circus Time. Technical report, Computer Science, University of York, UK (2013). http://www.cs.york.ac.uk/circus/hijac/publication.html
Woodcock, J., Cavalcanti, A., Fitzgerald, J.S., Larsen, P.G., Miyazawa, A., Perry, S.: Features of cml: A formal modelling language for systems of systems. In: SoSE, pp. 445–450. IEEE (2012)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall Inc., Upper Saddle River (1996)
Woodcock, J.C.P., Cavalcanti, A.L.C.: 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)
Woodcock, J., Cavalcanti, A.: The semantics of circus. In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 184. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Wei, K., Woodcock, J. (2015). Towards Algebraic Semantics of Circus Time . In: Naumann, D. (eds) Unifying Theories of Programming. UTP 2014. Lecture Notes in Computer Science(), vol 8963. Springer, Cham. https://doi.org/10.1007/978-3-319-14806-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-14806-9_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14805-2
Online ISBN: 978-3-319-14806-9
eBook Packages: Computer ScienceComputer Science (R0)