Skip to main content
SpringerLink
Log in

A Semantic Foundation for TCOZ in Unifying Theories of Programming

  • Conference paper
  • First Online:
FME 2003: Formal Methods (FME 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2805))

Included in the following conference series:

Abstract

Unifying Theories of Programming (UTP) can provide a formal semantic foundation not only for programming languages but also for more expressive specification languages. We believe UTP is particularly well suited for presenting the formal semantics for integrated specification languages which often have rich language constructs for state encapsulation, event communication and real-time modeling. This paper uses UTP to formalise the semantics of Timed Communicating Object Z (TCOZ) and captures some TCOZ new features for the first time. In particular, a novel unified semantic model of the channel based synchronisation and sensor/actuator based asynchronisation in TCOZ is presented. This semantic model will be used as a reference document for developing tools support for TCOZ and as a semantic foundation for proving soundness of those tools.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

References

  1. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Wang, Y.: UPPAAL - a Tool Suite forAutomatic Verification of Real-Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  2. Davies, J., Schneider, S.: A brief history of Timed CSP. Theoret. Comput. Sci. 138, 243–271 (1995)

    Article  MathSciNet  Google Scholar 

  3. Duke, D., Duke, R.: Towards a semantics for Object-Z. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 242–262. Springer, Heidelberg (1990)

    Google Scholar 

  4. Duke, R., Rose, G.: Formal Object Oriented Specification Using Object-Z, March 2000. Cornerstones of Computing Series. Macmillan, Basingstoke (2000)

    Google Scholar 

  5. He, J., Liu, Z., Li, X.: A relational model for specification of object-oriented systems. Technical Report 262, UNU/IIST (October 2002)

    Google Scholar 

  6. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  7. Mahony, B., Dong, J.S.: Sensors and Actuators in TCOZ. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1166–1185. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2), 150–177 (2000)

    Article  Google Scholar 

  9. Mahony, B., Dong, J.S.: Overview of the semantics of TCOZ. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999: Integrated Formal Methods, pp. 66–85. Springer, Heidelberg (1999)

    Google Scholar 

  10. Mislove, M., Roscoe, A., Schneider, S.: Fixed Points Without Completeness. Theoret. Comput. Sci. 138, 273–314 (1995)

    Article  MathSciNet  Google Scholar 

  11. Reed, G., Roscoe, A.: A timed model for communicating sequential processes. Theoret. Comput. Sci. 58, 249–261 (1988)

    Article  MathSciNet  Google Scholar 

  12. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  13. Schneider, S., Davies, J., Jackson, D., Reed, G., Reed, J., Roscoe, A.: Timed CSP: Theory and practice. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 640–675. Springer, Heidelberg (1992)

    Google Scholar 

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

    Chapter  Google Scholar 

  15. Smith, G.: A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing 7(3), 289–313 (1995)

    Article  Google Scholar 

  16. Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)

    Book  Google Scholar 

  17. Woodcock, J., Cavalcanti, A.: Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Oxford OX1 3QD, UK (July 2001)

    Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Singapore-MIT Alliance, National University of Singapore, Singapore

    Shengchao Qin & Wei-Ngan Chin

  2. School of Computing, National University o Singapore, Singapore

    Jin Song Dong & Wei-Ngan Chin

Authors
  1. Shengchao Qin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jin Song Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wei-Ngan Chin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Qin, S., Dong, J.S., Chin, WN. (2003). A Semantic Foundation for TCOZ in Unifying Theories of Programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45236-2_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40828-4

  • Online ISBN: 978-3-540-45236-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation