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

    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.
    Original languageEnglish
    Title of host publicationFME 2003: Formal Methods
    PublisherSpringer Berlin
    Pages321-340
    ISBN (Electronic)9783540452362
    ISBN (Print)9783540408284
    DOIs
    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
    Volume2805

    Conference

    ConferenceFME 2003: Formal Methods
    Country/TerritoryItaly
    CityPiza
    Period8/09/0314/09/03

    Fingerprint

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

    Cite this