A Semantic Foundation for TCOZ in Unifying Theories of Programming

Shengchao Qin, Jin Song Dong, Wei-Ngan Chin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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.
    Original languageEnglish
    Title of host publicationFME 2003: Formal Methods
    PublisherSpringer Berlin
    ISBN (Electronic)9783540452362
    ISBN (Print)9783540408284
    Publication statusPublished - 2003
    EventFME 2003: Formal Methods: International Symposium of Formal Methods Europe - Piza, Italy
    Duration: 8 Sept 200314 Sept 2003

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer, Berlin


    ConferenceFME 2003: Formal Methods


    Dive into the research topics of 'A Semantic Foundation for TCOZ in Unifying Theories of Programming'. Together they form a unique fingerprint.

    Cite this