TY - GEN
T1 - UTP semantics for bigrtimo
AU - Xie, Wanling
AU - Zhu, Huibiao
AU - Qin, Shengchao
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85056871362
U2 - 10.1007/978-3-030-02450-5_20
DO - 10.1007/978-3-030-02450-5_20
M3 - 会议稿件
AN - SCOPUS:85056871362
SN - 9783030024499
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 337
EP - 353
BT - Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Proceedings
A2 - Sun, Jing
A2 - Sun, Meng
PB - Springer Verlag
T2 - 20th International Conference on Formal Engineering Methods, ICFEM 2018
Y2 - 12 November 2018 through 16 November 2018
ER -