UTP Semantics for BigrTiMo

Wanling Xie, Huibiao Zhu, Shengchao Qin

Research output: Contribution to journalConference articlepeer-review

116 Downloads (Pure)


BigrTiMo [1], a process algebra that combines the rTiMo calculus [2] and the Bigraph model [3], is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with rTiMo, our BigrTiMo calculus can specify not only time, mobility and local communication, but also remote communication. In this paper, we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model for it based on Hoare and He’s Unifying Theories of Programming (UTP) [4]. Compared to the standard UTP model, in addition to the communication, the novelty of the proposed UTP model in this paper covers time, location and global shared variable. Moreover, we give an example to show the contribution of BigrTiMo and illustrate how to use our semantic model and the trace-merging definition proposed in our paper under this example. We also demonstrate the proofs of some algebraic laws proposed in [1] based on our denotational semantics.
Original languageEnglish
Pages (from-to)337-353
JournalFormal Methods and Software Engineering
Publication statusPublished - 11 Oct 2018
Event20th International Conference on Formal Engineering Methods - Gold Coast, Australia
Duration: 12 Nov 201816 Nov 2018


Dive into the research topics of 'UTP Semantics for BigrTiMo'. Together they form a unique fingerprint.

Cite this