@inproceedings{071726ab33054f6c8394c590a3bee740,
title = "Formalization and Verification of Mobile Systems Calculus Using the Rewriting Engine Maude",
abstract = "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.",
keywords = "BigTiMo calculus, Formalization, Maude, Mobile systems, Verification",
author = "Wanling Xie and Huibiao Zhu and Min Zhang and Gang Lu and Yucheng Fang",
note = "Publisher Copyright: {\textcopyright} 2018 IEEE.; 42nd IEEE Computer Software and Applications Conference, COMPSAC 2018 ; Conference date: 23-07-2018 Through 27-07-2018",
year = "2018",
month = jun,
day = "8",
doi = "10.1109/COMPSAC.2018.00034",
language = "英语",
series = "Proceedings - International Computer Software and Applications Conference",
publisher = "IEEE Computer Society",
pages = "213--218",
editor = "Chung-Horng Lung and Thomas Conte and Ling Liu and Toyokazu Akiyama and Kamrul Hasan and Edmundo Tovar and Hiroki Takakura and William Claycomb and Stelvio Cimato and Ji-Jiang Yang and Zhiyong Zhang and Ahamed, \{Sheikh Iqbal\} and Sorel Reisman and Claudio Demartini and Motonori Nakamura",
booktitle = "Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018",
address = "美国",
}