{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T22:59:19Z","timestamp":1783465159993,"version":"3.55.0"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,3,1]],"date-time":"2021-03-01T00:00:00Z","timestamp":1614556800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,3,1]],"date-time":"2021-03-01T00:00:00Z","timestamp":1614556800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-021-00530-x","type":"journal-article","created":{"date-parts":[[2021,3,6]],"date-time":"2021-03-06T08:02:31Z","timestamp":1615017751000},"page":"207-249","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A process calculus BigrTiMo of mobile systemsand its formal semantics"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4044-7320","authenticated-orcid":false,"given":"Wanling","family":"Xie","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qiwen","family":"Xu","sequence":"additional","affiliation":[{"name":"Faculty of Science and Technology, University of Macau, Macau, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Aman B Ciobanu G (2007) Mobile ambients with timers and types. In: Theoretical aspects of computing\u2014ICTAC 2007 4th International colloquium volume 4711 of lecture notes in computer science pp 50\u201363 Macau China September 26\u201328. Springer","DOI":"10.1007\/978-3-540-75292-9_4"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.010"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aman B Ciobanu G (2013) Real-time migration properties of rtimo verified in uppaal. In: Software engineering and formal methods\u201411th international conference SEFM 2013 volume 8137 of lecture notes in computer science pp 31\u201345 Madrid Spain September 25\u201327. Springer","DOI":"10.1007\/978-3-642-40561-7_3"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Guldstrand LK (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems international school on formal methods for the design of computer communication and software systems SFM-RT 2004 Bertinoro Italy September 13\u201318 2004 Revised Lectures pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Berger M (2004) Basic theory of reduction congruence fortwo timed asynchronous pi-calculi. In: CONCUR 2004\u2014concurrency theory 15th international conference volume 3170 of lecture notes in computer science pp 115\u2013130 London UK August 31\u2013September 3. Springer","DOI":"10.1007\/978-3-540-28644-8_8"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Clavel M. Dur\u00e1n F. Eker S. Lincoln P. Mart\u00ed -Oliet N Meseguer J Quesada JF : Maude: specification and programming in rewriting logic. Theor Comput Sci 285 (2) 187\u2013243 (2002)","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_2_11_2","unstructured":"Clavel M Dur\u00e1n F Eker S Lincoln P Mart\u00ed -Oliet N Meseguer J Talcott CL (eds) (2007) All about Maude\u2014a high-performance logical framework how to specify program and verify systems in rewriting logic volume 4350 of lecture notes in computer science. Springer"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80699-1"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.05.002"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0124-9"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82534-4"},{"key":"e_1_2_1_2_17_2","volume-title":"Software engineering and formal methods\u201317th international conference, SEFM 2019, Oslo, Norway, September 18\u201320, 2019, Proceedings","author":"Gleirscher M","year":"2019"},{"key":"e_1_2_1_2_18_2","unstructured":"Hennessy M.: Algebraic theory of processes. MIT Press series in the foundations of computing MIT Press Cambridge (1988)"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/95363"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90219-Y"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR He J (1998) Unifying theories of programming. Prentice Hall international series in computer science","DOI":"10.1007\/BFb0002714"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_2_1_2_24_2","unstructured":"G\u00e9rard H Gilles K Christine P-M (2004) The coq proof assistant a tutorial. Rapport Tech 178"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.009"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/357980.358001"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (2013) Unifying semantics for concurrent programming. In: Computation logic games and quantum foundations. The many facets of Samson Abramsky\u2014essays dedicated to Samson Abramsky on the occasion of his 60th birthday volume 7860 of lecture notes in computer science pp 139\u2013149. Springer","DOI":"10.1007\/978-3-642-38164-5_10"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-09526-8_8","volume-title":"Mathematical foundations of computer science 1979, proceedings, 8th symposium","author":"Hennessy M","year":"1979"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0249-0"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.09.012"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-007-0002-7"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Lakos C (2005) A petri net view of mobility. In: Formal techniques for networked and distributed systems\u2014FORTE 2005 25th IFIP WG 6.1 international conference Taipei Taiwan October 2\u20135 2005 Proceedings pp 174\u2013188","DOI":"10.1007\/11562436_14"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-04856-2_6","article-title":"Modelling mobile IP with mobile petri nets","volume":"3","author":"Lakos C","year":"2009","journal-title":"Trans Petri Nets Other Models Concurr"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"M\u00e4kel\u00e4 M (2002) Maria: Modular reachability analyser for algebraic system nets. In: Applications and theory of Petri nets 2002 23rd international conference ICATPN 2002 Adelaide Australia June 24\u201330 2002 Proceedings pp 434\u2013444","DOI":"10.1007\/3-540-48068-4_25"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Milner R.: A calculus of communicating systems. lecture notes in computer science vol. 92. Springer Berlin (1980)","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_39_2","volume-title":"Communicating and mobile systems\u2013the pi-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/1540607"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/304399.304400"},{"key":"e_1_2_1_2_44_2","volume-title":"Semantics with applications\u2013a formal introduction","author":"Nielson HR","year":"1992"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L.C. Wenzel M.: Isabelle\/HOL\u2013a proof assistant for higher-order logic. lecture notes in computer science vol. 2283. Springer Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"O'Hearn P.W.: Resources concurrency and local reasoning. Theor Comput Sci 375 (1\u20133) 271\u2013307 (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211473"},{"key":"e_1_2_1_2_48_2","unstructured":"Paulson LC (1994) Isabelle\u2014a generic theorem prover (with a contribution by T. Nipkow) volume 828 of lecture notes in computer science. Springer Berlin"},{"key":"e_1_2_1_2_49_2","first-page":"1","article-title":"IP mobility support for ipv4, revised","volume":"5944","author":"Perkins CE","year":"2010","journal-title":"RFC"},{"key":"e_1_2_1_2_50_2","unstructured":"Pereira E (2015) Mobile reactive systems over bigraphical machines\u2014a programming model and its implementation. PhD thesis University of California Berkeley USA"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Pita I Riesco A (2015) Specifying and analyzing the kademlia protocol in maude. In: Theoretical aspects of computing\u2014ICTAC 2015 volume 9399 of lecture notes in computer science pp 524\u2013541 Colombia October 29\u201331. Springer","DOI":"10.1007\/978-3-319-25150-9_30"},{"key":"e_1_2_1_2_53_2","volume-title":"Distributed computing by mobile entities, current research in moving and computing","author":"Potop-Butucaru M","year":"2019"},{"key":"e_1_2_1_2_54_2","volume-title":"Tools and algorithms for construction and analysis of systems, 4th international conference, TACAS '98, Held as Part of the European joint conferences on the theory and practice of software, ETAPS'98, Lisbon, Portugal, March 28-April 4, 1998, proceedings","author":"Regensburger F","year":"1998"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0398-7"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Reisig W. Rozenberg G. (eds.): Lectures on Petri nets I: basic models. lecture notes in computer science vol. 1491. Springer Berlin (1998)","DOI":"10.1007\/3-540-65306-6"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Reisig W. Rozenberg G. (eds.): Lectures on Petri nets II: applications. lecture notes in computer science vol. 1492. Springer Berlin (1998)","DOI":"10.1007\/3-540-65307-4"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/TASE.2009.32","volume-title":"TASE 2009, third IEEE international symposium on theoretical aspects of software engineering, 29\u201331 July 2009","author":"Sun J","year":"2009"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS Pang J (2009) Pat: Towards flexible verification under fairness volume 5643 of lecture notes in computer science pp 709\u2013714. Springer Berlin","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Stoy JE (1979) Foundations of denotational semantics. In: Abstract software specifications 1979 Copenhagen Winter School volume 86 of lecture notes in computer science pp 43\u201399. Springer","DOI":"10.1007\/3-540-10007-5_35"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0453-7"},{"key":"e_1_2_1_2_63_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Padberg U. Schulz A. (2016) Model checking reconfigurable petri nets with maude. In: Graph transformation\u20139th international conference ICGT : in memory of Hartmut Ehrig held as part of STAF 2016. lecture notes in computer science pp 54\u201370 Vienna vol. 9761. Springer Austria (2016)","DOI":"10.1007\/978-3-319-40530-8_4"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","unstructured":"Verdejo A. Mart\u00ed -Oliet N : Executable structural operational semantics in maude. J Log Algebr Program 67 (1\u20132) 226\u2013293 (2006)","DOI":"10.1016\/j.jlap.2005.09.008"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/120468"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0467-1"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Xie W Zhu H Qin S (2018) UTP semantics for bigrtimo. In: Formal methods and software engineering\u201420th international conference on formal engineering methods ICFEM 2018 volume 11232 of lecture notes in computer science pp 337\u2013353 Gold Coast QLD Australia November 12\u201316. Springer","DOI":"10.1007\/978-3-030-02450-5_20"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"crossref","unstructured":"Xie W Zhu H Xu Q (2017) Bigrtimo-a process algebra for structure-aware mobile systems. In: 22nd International conference on engineering of complex computer systems ICECCS 2017 pp 50\u201359 Fukuoka Japan November 5\u20138. IEEE Computer Society","DOI":"10.1109\/ICECCS.2017.13"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","unstructured":"Xie W Zhu H Zhang M Lu G Fang Y (2018) Formalization and verification of mobile systems calculus using the rewriting engine maude. In: 2018 IEEE 42nd annual computer software and applications conference COMPSAC 2018 pp 213\u2013218 Tokyo Japan 23-27. IEEE Computer Society","DOI":"10.1109\/COMPSAC.2018.00034"},{"issue":"3","key":"e_1_2_1_2_71_2","first-page":"209","article-title":"Algebraic approach to linking the semantics of web services","volume":"7","author":"Zhu H","year":"2011","journal-title":"ISSE"},{"issue":"4","key":"e_1_2_1_2_72_2","first-page":"271","article-title":"PTSC: probability, time and shared-variable concurrency","volume":"5","author":"Zhu H","year":"2009","journal-title":"ISSE"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Zhu H Sanders JW He J Qin S (2012) Denotational semantics for a probabilistic timed shared-variable language. In: Unifying theories of programming 4th international symposium UTP 2012 volume 7681 of lecture notes in computer science pp 224\u2013247 Paris France August 27\u201328","DOI":"10.1007\/978-3-642-35705-3_11"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.06.003"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00530-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00530-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00530-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00530-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,25]],"date-time":"2024-08-25T14:15:19Z","timestamp":1724595319000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00530-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3]]},"references-count":74,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["10.1007\/s00165-021-00530-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00530-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3]]},"assertion":[{"value":"22 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 December 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 March 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}