Formalization and Verification of Mobile Systems Calculus Using the Rewriting Engine Maude

摘要

BigTiMo calculus is for structure-aware mobile systems and it combines the TiMo calculus and the Bigraph model. Compared with TiMo, BigTiMo can model not only the locations of the components but also the connectivity of the components. Thus, our BigTiMo process can communicate not only locally with other process, but also remotely with other process. In this paper, we introduce the syntax and the operational semantics of the BigTiMo calculus. We also develop an executable formal specification of our Big-TiMo calculus in a declarative language called Maude. In addition, we verify safety properties of the mobile systems described by BigTiMo using state exploration and LTL model checking in Maude.