Skip to main content
SpringerLink
Log in

The Denotational Semantics of slotted-Circus

  • Conference paper
FM 2009: Formal Methods (FM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5850))

Included in the following conference series:

Abstract

This paper describes a complete denotational semantics, in the UTP framework, of slotted-Circus, a generic framework for reasoning about discrete timed/synchronously clocked systems. The key result presented here is a comprehensive semantics of the entire language that addresses various semantics issues that have been uncovered, whilst laying foundations for future extensions, particularly towards prioritized choice.

This research was supported by a grant from Science Foundation Ireland, as well as partial support from Lero, the Irish Software Engineering Research Centre.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Butterfield, A., Gancarski, P.: Slotted-Circus: A generic UTP framework for discretely-timed circus. Technical Report TCD-CS-09-32, School of Computer Science & Statistic Trinity College Dublin, Trinity College, Dublin 2, Ireland (July 2009), https://www.cs.tcd.ie/publications/tech-reports/reports.09/TCD-CS-2009-32.pdf

  2. Butterfield, A., Sherif, A., Woodcock, J.: Slotted-circus: A UTP-family of reactive theories. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75–97. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Butler, M.J.: csp2b: A practical approach to combining csp and b. Formal Aspects of Computing 12, 182–196 (2000)

    Article  MATH  Google Scholar 

  4. Butterfield, A., Woodcock, J.: Prialt in Handel-C: an operational semantics. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 248–267 (2005)

    Google Scholar 

  5. Celoxica Ltd. Handel-C Language Reference Manual, v3.0 (2002), http://www.celoxica.com

  6. Gancarski, P., Butterfield, A., Woodcock, J.: State visibility and communication in unifying theories of programming. In: Chin, W.-N., Qin, S. (eds.) 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 47–54. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  7. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall, Englewood Cliffs (1998), http://www.unifyingtheories.org

    Google Scholar 

  8. Hoare, C.A.R.: Communicating Sequential Processes. Intl. Series in Computer Science. Prentice Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  9. Hoare, C.A.R.: Programs are predicates. In: Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, pp. 141–155. Prentice-Hall, Inc., Englewood Cliffs (1985)

    Google Scholar 

  10. Mahony, B.P., Dong, J.S.: Timed communicating object Z. IEEE Trans. Software Eng. 26(2), 150–177 (2000)

    Article  Google Scholar 

  11. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Asp. Comput. 21(1-2), 3–32 (2009)

    Article  MATH  Google Scholar 

  12. Qin, S., Dong, J.S., Chin, W.-N.: A semantic foundation for TCOZ in unifying theories of programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 321–340. Springer, Heidelberg (2003)

    Google Scholar 

  13. Roggenbach, M.: CSP-CASL - A new integration of process algebra and algebraic specification. Theor. Comput. Sci. 354(1), 42–71 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  14. Roscoe, A.W.: The Theory and Practice of Concurrency. international series in computer science. Prentice Hall, Englewood Cliffs (1997)

    Google Scholar 

  15. Schneider, S.: Concurrent and Real-time Systems — The CSP Approach. Wiley, Chichester (2000)

    Google Scholar 

  16. Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems-an integration of object-Z and CSP. Formal Methods in System Design 18(3), 249–284 (2001)

    Article  MATH  Google Scholar 

  17. SGS-THOMSON Microelectronics Limited. occam 2.1 reference manual, May 12 (1995)

    Google Scholar 

  18. Sherif, A., He, J.: Towards a time model for circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613–624. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Sherif, A.: A Framework for Specification and Validation of Real Time Systems using Circus Action. Ph.d. thesis, Universidade Federale de Pernambuco, Recife, Brazil (January 2006)

    Google Scholar 

  20. Smith, G.: An integration of real-time object-Z and CSP for specifying concurrent real-time systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 267–285. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Woodcock, J., Cavalcanti, A.: Circus: a concurrent refinement language. Technical report, University of Kent at Canterbury (October 2001)

    Google Scholar 

  22. Woodcock, J., Hughes, A.P.: Unifying theories of parallel programming. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 24–37. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Trinity College Dublin,  

    Paweł Gancarski & Andrew Butterfield

Authors
  1. Paweł Gancarski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew Butterfield
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Heslington, University of York, Y010 5DD, York, UK

    Ana Cavalcanti

  2. Bell Laboratories, 600 Mountain Ave., 07974, Murray Hill, NY, USA

    Dennis R. Dams

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gancarski, P., Butterfield, A. (2009). The Denotational Semantics of slotted-Circus . In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-05089-3_29

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-05088-6

  • Online ISBN: 978-3-642-05089-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation