In this paper, we present a process calculus called BigrTiMo thatcombines the rTiMo calculus and the Bigraph model. BigrTiMo calculusis capable of specifying a rich variety of properties forstructure-aware mobile systems. Compared with rTiMo, our BigrTiMocalculus can specify not only time, mobility and localcommunication, but also remote communication. We then investigatethe operational semantics of the BigrTiMo calculus and develop anexecutable formal specification of our BigrTiMo calculus in adeclarative language called Maude. In addition, we verify safetyproperties and liveness properties of the mobile systems describedby BigrTiMo using state exploration and LTL model checking in Maude.Based on Hoare and He's Unifying Theories of Programming (UTP), westudy the semantic foundation of this highly expressive modellinglanguage and propose a denotational semantic model and a set ofalgebraic laws for it. The semantic model in this paper coverstime, location, communication and global shared variable at the sametime. We also demonstrate the proofs of some algebraic laws based onour denotational semantics. Moreover, we explore how the algebraicsemantics relates with the operational semantics and denotationalsemantics, which is conducted by the study of deriving theoperational semantics and denotational semantics from algebraicsemantics. We prove the equivalence between the derived transitionsystem (e.g., the operational semantics) and the derivationstrategy, which indicates that the operational semantics is soundand complete.