In this paper, we present a process calculus called BigrTiMo that combines the rTiMo calculus and the Bigraph model. BigrTiMo calculus 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.We then investigate the operational semantics of the BigrTiMo calculus and develop an executable formal specification of our BigrTiMo calculus in a declarative language called Maude. In addition, we verify safety properties and liveness properties of the mobile systems described by BigrTiMo using state exploration and LTL model checking in Maude. Based on Hoare and He’s Unifying Theories of Programming (UTP), we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model and a set of algebraic laws for it. The semantic model in this paper covers time, location, communication and global shared variable at the same time.We also demonstrate the proofs of some algebraic laws based on our denotational semantics. Moreover, we explore how the algebraic semantics relates with the operational semantics and denotational semantics,which is conducted by the study of deriving the operational semantics and denotational semantics from algebraic semantics. We prove the equivalence between the derived transition system (e.g., the operational semantics) and the derivation strategy, which indicates that the operational semantics is sound and complete.