{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T22:59:18Z","timestamp":1783465158983,"version":"3.55.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"Natural Science Foundation of China","doi-asserted-by":"crossref","award":["Grant No. 61361136002"],"award-info":[{"award-number":["Grant No. 61361136002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>rTiMo is a real-time version of\u00a0 TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable<jats:italic>tr<\/jats:italic>is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of<jats:italic>guarded<\/jats:italic><jats:italic>choice<\/jats:italic>. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.<\/jats:p>","DOI":"10.1007\/s00165-018-0467-1","type":"journal-article","created":{"date-parts":[[2018,8,10]],"date-time":"2018-08-10T08:19:28Z","timestamp":1533889168000},"page":"713-738","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A UTP approach for rTiMo"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4044-7320","authenticated-orcid":false,"given":"Wanling","family":"Xie","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Laboratory of Trustworthy Software, International Research Center of Trustworthy Software, East China Normal University, 200062, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shuangqing","family":"Xiang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Laboratory of Trustworthy Software, International Research Center of Trustworthy Software, East China Normal University, 200062, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Laboratory of Trustworthy Software, International Research Center of Trustworthy Software, East China Normal University, 200062, Shanghai, China"},{"name":"School of Computer Science and Software Engineering, Shenzhen University, Shenzhen, 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 (2013) Real-time migration properties of rtimo verified in Uppaal. In: 11th international conference SEFM 2013 software engineering and formal methods Madrid Spain September 25\u201327 2013 proceedings pp. 31\u201345","DOI":"10.1007\/978-3-642-40561-7_3"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-319-19458-5_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"Aman Bogdan","year":"2015"},{"key":"e_1_2_1_2_3_2","unstructured":"Aman B Ciobanu G(2015) Verification of bounded real-time distributed systems with mobility. In: Proceedings of the 9th workshop on verification and evaluation of computer and communication systems VECoS 2015 Bucharest Romania September 10-11 2015 pp 109\u2013120"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0180-9"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barthe G Gaboardi M Arias EJG Hsu J Kunz C Strub PY (2014) Proving differential privacy in Hoare logic. In:IEEE 27th computer security foundations symposium CSF 2014 Vienna Austria 19\u201322 July 2014 pp. 411\u2013424","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0159-y"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.1854"},{"key":"e_1_2_1_2_10_2","first-page":"293","volume-title":"Lecture Notes in Computer Science","author":"Ciobanu Gabriel","year":"2011"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.05.002"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxu006"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0324-9"},{"key":"e_1_2_1_2_14_2","first-page":"201","volume-title":"Lecture Notes in Computer Science","author":"Christensen S\u00f8ren","year":"1995"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/43.3.224"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"issue":"1","key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(00)00304-2","article-title":"A Hoare logic for dynamic networks of asynchronously communicating deterministic processes","volume":"274","author":"de Boer Frank S","year":"2002","journal-title":"Theor Comput Sci"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0124-9"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0307-4"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/547872"},{"key":"e_1_2_1_2_22_2","unstructured":"Gordon Michael JC (1995) The semantic challenge of Verilog HDL. In: Proceedings 10th annual IEEE symposium on logic in computer science San Diego California USA June 26-29 1995 pp. 136\u2013145"},{"key":"e_1_2_1_2_23_2","unstructured":"He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill international series in software engineering"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"He J (2016) A new roadmap for linking theories of programming. In: Unifying theories of programming-6th international symposium UTP 2016 Reykjavik Iceland June 4\u20135 2016 Revised Selected Papers pp 26\u201343","DOI":"10.1007\/978-3-319-52228-9_2"},{"key":"e_1_2_1_2_25_2","volume-title":"Algebraic theory of processes","author":"Hennessy M","year":"1988"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90219-Y"},{"key":"e_1_2_1_2_27_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_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-015-3251-x"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-3-642-38164-5_10","volume-title":"Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky","author":"Hoare Tony","year":"2013"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/BFb0031996","volume-title":"Real-Time: Theory in Practice","author":"Hooman Jozef","year":"1992"},{"issue":"6","key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1007\/BF01213604","article-title":"Extending Hoare Logic to real-time","volume":"6","author":"Hooman J","year":"1994","journal-title":"Formal Asp Comput"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0249-0"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.09.012"},{"issue":"5","key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","first-page":"870","DOI":"10.1007\/s11704-016-5158-6","article-title":"Reasoning about actions with loops via Hoare logic","volume":"10","author":"He J","year":"2016","journal-title":"Front Comput Sci"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/11562436_14","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"Lakos Charles A.","year":"2005"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Lakos C (2009) Modelling mobile IP with mobile Petri nets.Transactions on petri nets and other models of concurrency III. Lecture notes in computer science 5800 Springer 2009 ISBN 978-3-642-04854-8 3:127\u2013158","DOI":"10.1007\/978-3-642-04856-2_6"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-008-0039-2"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/3-540-48068-4_25","volume-title":"Application and Theory of Petri Nets 2002","author":"M\u00e4kel\u00e4 Marko","year":"2002"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Milner R (1980) A calculus of communicating systems\u00a0 (Lecture notes in computer science) vol\u00a092. Springer","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/151233.151240"},{"key":"e_1_2_1_2_46_2","volume-title":"Communicating and mobile systems-the Pi-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059824"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2007.909552"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Paulson LC (1994) Isabelle-A Generic theorem prover (with a contribution by T. Nipkow) volume 828 of Lecture notes in computer science. Springer","DOI":"10.1007\/BFb0030541"},{"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","unstructured":"Vaughan RP (1990) Action logic and pure induction. In: Logics in AI European workshop JELIA '90 Amsterdam The Netherlands September 10\u201314 1990 proceedings pp 97\u2013120"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.004"},{"key":"e_1_2_1_2_54_2","unstructured":"Shi L (2009) Comparative studies formal semantics and PVS encoding of CSP#. PhD thesis East China Normal University China"},{"key":"e_1_2_1_2_55_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_56_2","first-page":"43","volume-title":"Lecture Notes in Computer Science","author":"Stoy Joseph E.","year":"1980"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Shi L Zhao Y Liu Y Sun J Dong JS Qin S (2018) A UTP semantics for communicating processes with shared variables and its formal encoding in PVS.Formal Asp Comput","DOI":"10.1007\/s00165-018-0453-7"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_59_2","first-page":"1","volume-title":"Application and Theory of Petri Nets 1998","author":"Valk R\u00fcdiger","year":"1998"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.598"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/120468"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Xie W Xiang S (2016) UTP semantics for rTiMo. In Unifying theories of programming-6th international symposium UTP 2016 Reykjavik Iceland June 4\u20135 2016 Revised Selected Papers pp. 176\u2013196","DOI":"10.1007\/978-3-319-52228-9_9"},{"issue":"4","key":"e_1_2_1_2_63_2","first-page":"341","article-title":"From algebraic semantics to denotational semantics for Verilog","volume":"4","author":"Zhu H","year":"2008","journal-title":"ISSE"},{"issue":"3","key":"e_1_2_1_2_64_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"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0309-8"},{"key":"e_1_2_1_2_66_2","unstructured":"Zhu H (2005)Linking the semantics of a multithreaded discrete event simulation language. PhD thesis London South Bank University UK"},{"key":"e_1_2_1_2_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.06.003"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Zou L Zhan N Wang S Fr\u00e4nzle M Qin S (2013) Verifying Simulink diagrams via a hybrid hoare logic prover. In: Proceedings of the international conference on embedded software EMSOFT 2013 Montreal QC Canada September 29\u2013Oct. 4 2013 pp 9:1\u20139:10","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0467-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0467-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0467-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0467-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T08:34:29Z","timestamp":1751790869000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0467-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":68,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["10.1007\/s00165-018-0467-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0467-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]},"assertion":[{"value":"25 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 July 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 August 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}