TY - GEN
T1 - An Axiomatic Approach to BigrTiMo
AU - Xie, Wanling
AU - Zhu, Huibiao
AU - Qin, Shengchao
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/12
Y1 - 2020/12
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 the rTiMo model, our BigrTiMo calculus can specify not only time, mobility and the local communication (the two communication components should be at the same location), but also the remote communication (the two communication components can be at the different locations). In this paper, we present an axiomatic approach to BigrTiMo program language verification based on Hoare-style [4] proof rules. In order to describe the timing of observable actions and the state of the bigraph, we extend the assertion language with primitives. Moreover, we prove the soundness of our proof rules and show the application of the proof rules via an example.
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 the rTiMo model, our BigrTiMo calculus can specify not only time, mobility and the local communication (the two communication components should be at the same location), but also the remote communication (the two communication components can be at the different locations). In this paper, we present an axiomatic approach to BigrTiMo program language verification based on Hoare-style [4] proof rules. In order to describe the timing of observable actions and the state of the bigraph, we extend the assertion language with primitives. Moreover, we prove the soundness of our proof rules and show the application of the proof rules via an example.
KW - n/a
UR - https://www.scopus.com/pages/publications/85105395352
U2 - 10.1109/TASE49443.2020.00015
DO - 10.1109/TASE49443.2020.00015
M3 - 会议稿件
AN - SCOPUS:85105395352
T3 - Proceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
SP - 41
EP - 48
BT - Proceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
A2 - Aoki, Toshiaki
A2 - Li, Qin
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 14th International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
Y2 - 11 December 2020 through 13 December 2020
ER -