Circus Time with Reactive Designs
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.
KeywordsCircus Time UTP reactive designs
Unable to display preview. Download preview PDF.
- 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), http://www.lri.fr/Rapports-internes
- 5.Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)Google Scholar
- 6.Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall International (1998)Google Scholar
- 7.Locke, D., et al.: Safety Critical Java Specification. First Release 0.76, The Open Group, UK (2010)Google Scholar
- 10.Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International (1998)Google Scholar
- 11.Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons (1999)Google Scholar
- 13.Wei, K., Woodcock, J., Cavalcanti, A.: New Circus Time. Technical report, Department of Computer Science, University of York, UK (March 2012), http://www.cs.york.ac.uk/circus/hijac/publication.html
- 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