@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 Annual 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 = "Sorel Reisman and Ahamed, \{Sheikh Iqbal\} and Claudio Demartini and Thomas Conte and Ling Liu and William Claycomb and Motonori Nakamura and Edmundo Tovar and Stelvio Cimato and Chung-Horng Lung and Hiroki Takakura and Ji-Jiang Yang and Toyokazu Akiyama and Zhiyong Zhang and Kamrul Hasan",
booktitle = "Proceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018",
address = "美国",
}