{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T10:34:47Z","timestamp":1725878087414},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522272"},{"type":"electronic","value":"9783319522289"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52228-9_9","type":"book-chapter","created":{"date-parts":[[2017,1,9]],"date-time":"2017-01-09T23:23:43Z","timestamp":1484004223000},"page":"176-196","source":"Crossref","is-referenced-by-count":3,"title":["UTP Semantics for rTiMo"],"prefix":"10.1007","author":[{"given":"Wanling","family":"Xie","sequence":"first","affiliation":[]},{"given":"Shuangqing","family":"Xiang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11562436_14","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"CA Lakos","year":"2005","unstructured":"Lakos, C.A.: A Petri net view of mobility. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 174\u2013188. Springer, Heidelberg (2005). doi: 10.1007\/11562436_14"},{"issue":"1","key":"9_CR2","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1109\/TSMCA.2007.909552","volume":"38","author":"L Ma","year":"2008","unstructured":"Ma, L., Tsai, J.J.P.: Formal modeling and analysis of a secure mobile-agent system. IEEE Trans. Syst. Man Cybern. Part A 38(1), 180\u2013196 (2008)","journal-title":"IEEE Trans. Syst. Man Cybern. Part A"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-04856-2_6","volume-title":"Transactions on Petri Nets and Other Models of Concurrency III","author":"C Lakos","year":"2009","unstructured":"Lakos, C.: Modelling mobile IP with mobile petri nets. In: Jensen, K., Billington, J., Koutny, M. (eds.) ToPNoC III. LNCS, vol. 5800, pp. 127\u2013158. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04856-2_6"},{"issue":"5","key":"9_CR4","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1007\/s00165-010-0159-y","volume":"23","author":"C Braghin","year":"2011","unstructured":"Braghin, C., Sharygina, N., Barone-Adesi, K.: A model checking-based approach for security policy verification of mobile systems. Formal Asp. Comput. 23(5), 627\u2013648 (2011)","journal-title":"Formal Asp. Comput."},{"issue":"7","key":"9_CR5","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1016\/j.jlap.2011.05.002","volume":"80","author":"G Ciobanu","year":"2011","unstructured":"Ciobanu, G., Koutny, M.: Timed mobility in process algebra and Petri nets. J. Log. Algebr. Program. 80(7), 377\u2013391 (2011)","journal-title":"J. Log. Algebr. Program."},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-40561-7_3","volume-title":"Software Engineering and Formal Methods","author":"B Aman","year":"2013","unstructured":"Aman, B., Ciobanu, G.: Real-time migration properties of rTiMo verified in uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 31\u201345. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40561-7_3"},{"issue":"3","key":"9_CR7","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s00165-014-0324-9","volume":"27","author":"G Ciobanu","year":"2015","unstructured":"Ciobanu, G., Koutny, M., Steggles, L.J.: Strategy based semantics for mobility with time and access permissions. Formal Asp. Comput. 27(3), 525\u2013549 (2015)","journal-title":"Formal Asp. Comput."},{"key":"9_CR8","unstructured":"Aman, B., Ciobanu, G.: 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\u201311, pp. 109\u2013120 (2015)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-21437-0_23","volume-title":"FM 2011: Formal Methods","author":"G Ciobanu","year":"2011","unstructured":"Ciobanu, G., Koutny, M.: Timed migration and interaction with access permissions. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 293\u2013307. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21437-0_23"},{"issue":"6","key":"9_CR10","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1002\/cpe.1854","volume":"24","author":"G Ciobanu","year":"2012","unstructured":"Ciobanu, G., Juravle, C.: Flexible software architecture and language for mobile agents. Concurrency Comput.: Pract. Experience 24(6), 559\u2013571 (2012)","journal-title":"Concurrency Comput.: Pract. Experience"},{"issue":"5","key":"9_CR11","doi-asserted-by":"crossref","first-page":"1041","DOI":"10.1093\/comjnl\/bxu006","volume":"58","author":"G Ciobanu","year":"2015","unstructured":"Ciobanu, G., Koutny, M.: Pertimo: a model of spatial migration with safe access permissions. Comput. J. 58(5), 1041\u20131060 (2015)","journal-title":"Comput. J."},{"key":"9_CR12","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algebr. Program."},{"issue":"8","key":"9_CR13","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C., Roscoe, A.W., Sanders, J.W., S\u00f8rensen, I.H., Spivey, J.M., Sufrin, B.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"9_CR14","series-title":"International Series in Computer Science","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in Computer Science. Prentice Hall, Upper Saddle River (1998)"},{"key":"9_CR15","series-title":"International Series in Software Engineering","volume-title":"Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers","author":"J He","year":"1994","unstructured":"He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. International Series in Software Engineering. The McGraw-Hill, New York City (1994)"},{"issue":"8","key":"9_CR16","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"CAR Hoare","year":"1993","unstructured":"Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta Inf. 30(8), 701\u2013739 (1993)","journal-title":"Acta Inf."},{"issue":"5","key":"9_CR17","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/s00165-009-0124-9","volume":"22","author":"A Duran","year":"2010","unstructured":"Duran, A., Cavalcanti, A., Sampaio, A.: An algebraic approach to the design of compilers for object-oriented languages. Formal Asp. Comput. 22(5), 489\u2013535 (2010)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"9_CR18","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s00165-014-0309-8","volume":"27","author":"H Zhu","year":"2015","unstructured":"Zhu, H., He, J., Qin, S., Brooke, P.J.: Denotational semantics and its algebraic derivation for an event-driven system-level language. Formal Asp. Comput. 27(1), 133\u2013166 (2015)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"9_CR19","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.jlap.2011.06.003","volume":"81","author":"H Zhu","year":"2012","unstructured":"Zhu, H., Yang, F., He, J., Bowen, J.P., Sanders, J.W., Qin, S.: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. J. Log. Algebr. Program. 81(1), 2\u201325 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"9_CR20","first-page":"209","volume":"7","author":"H Zhu","year":"2011","unstructured":"Zhu, H., He, J., Li, J., Bowen, J.P.: Algebraic approach to linking the semantics of web services. ISSE 7(3), 209\u2013224 (2011)","journal-title":"ISSE"},{"key":"9_CR21","series-title":"Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52228-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T03:45:58Z","timestamp":1498362358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52228-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522272","9783319522289"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52228-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}