An Axiomatic Approach to BigrTiMo

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.