{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T10:57:36Z","timestamp":1772881056994,"version":"3.50.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,11,2]],"date-time":"2016-11-02T00:00:00Z","timestamp":1478044800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10009-016-0439-9","type":"journal-article","created":{"date-parts":[[2016,11,2]],"date-time":"2016-11-02T08:08:06Z","timestamp":1478074086000},"page":"395-408","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of critical systems described in real-time TiMo\u00a0"],"prefix":"10.1007","volume":"19","author":[{"given":"Bogdan","family":"Aman","sequence":"first","affiliation":[]},{"given":"Gabriel","family":"Ciobanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,2]]},"reference":[{"key":"439_CR1","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-642-40561-7_3","volume":"8137","author":"B Aman","year":"2013","unstructured":"Aman, B., Ciobanu, G.: Real-time migration properties of TiMo@ PAT verified in Uppaal. Lect. Notes Comput. Sci. 8137, 31\u201345 (2013)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR2","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-319-19458-5_10","volume":"9128","author":"B Aman","year":"2015","unstructured":"Aman, B., Ciobanu, G.: Timed mobility and timed communication for critical systems. Lect. Notes Comput. Sci. 9128, 146\u2013161 (2015)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR3","doi-asserted-by":"crossref","unstructured":"Aman, B., Ciobanu, G., Koutny, M.: Behavioural equivalences over migrating processes with timers. Lect. Notes Comput. Sci. 7273, 52\u201366 (2012)","DOI":"10.1007\/978-3-642-30793-5_4"},{"key":"439_CR4","doi-asserted-by":"crossref","unstructured":"Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Monographs in Theoretical Computer Science. Springer, Berlin (2002)","DOI":"10.1007\/978-3-662-04995-2"},{"key":"439_CR5","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-3-540-89437-7_13","volume":"5380","author":"G Ciobanu","year":"2008","unstructured":"Ciobanu, G.: Behaviour equivalences in timed distributed $$\\pi $$ \u03c0 -calculus. Lect. Notes Comput. Sci. 5380, 190\u2013208 (2008)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR6","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. Concurr. Comput. Pract. Exp. 24, 559\u2013571 (2012)","journal-title":"Concurr. Comput. Pract. Exp."},{"key":"439_CR7","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. Logic Algebr. Program. 80, 377\u2013391 (2011)","journal-title":"J. Logic Algebr. Program."},{"key":"439_CR8","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-642-21437-0_23","volume":"6664","author":"G Ciobanu","year":"2011","unstructured":"Ciobanu, G., Koutny, M.: Timed migration and interaction with access permissions. Lect. Notes Comput. Sci. 6664, 293\u2013307 (2011)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR9","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, 1041\u20131060 (2015)","journal-title":"Comput. J."},{"key":"439_CR10","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/j.entcs.2006.07.013","volume":"164","author":"G Ciobanu","year":"2006","unstructured":"Ciobanu, G., Prisacariu, C.: Timers for distributed systems. Electron. Notes Theor. Comput. Sci. 164, 81\u201399 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"439_CR11","doi-asserted-by":"crossref","unstructured":"Ciobanu, G., Zheng, M.: Automatic analysis of TiMo@PAT systems in PAT. In: Proceedings of 18th International Conference on Engineering of Complex Computer Systems. IEEE Computer Society, pp. 121\u2013124 (2013)","DOI":"10.1109\/ICECCS.2013.25"},{"key":"439_CR12","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/BFb0039069","volume":"458","author":"JF Groote","year":"1990","unstructured":"Groote, J.F.: Transition system specifications with negative premises. Lect. Notes Comput. Sci. 458, 332\u2013341 (1990)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR13","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/978-3-540-78929-1_18","volume":"4981","author":"T Han","year":"2008","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Compositional modeling and minimization of time-inhomogeneous Markov chains. Lect. Notes Comput. Sci. 4981, 244\u2013258 (2008)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR14","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Lynch, N.: The generalized railroad crossing: a case study in formal verification of real-time systems. In: Proceedings of IEEE Real-Time Systems Symposium, pp. 120\u2013131 (1994)","DOI":"10.1109\/REAL.1994.342724"},{"key":"439_CR15","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1016\/j.apal.2011.12.002","volume":"163","author":"N Kamide","year":"2012","unstructured":"Kamide, N.: Bounded linear-time temporal logic: a proof-theoretic investigation. Ann. Pure Appl. Logic 163, 439\u2013466 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"439_CR16","volume-title":"Communicating and Mobile Systems: The $$\\pi $$ \u03c0","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The $$\\pi $$ \u03c0 -Calculus. Cambridge University Press, New York (1999)"},{"key":"439_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume":"104","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. Lect. Notes Comput. Sci. 104, 167\u2013183 (1981)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)"},{"key":"439_CR19","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume":"5643","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. Lect. Notes Comput. Sci. 5643, 709\u2013714 (2009)","journal-title":"Lect. Notes Comput. Sci."},{"key":"439_CR20","doi-asserted-by":"crossref","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings of International Conference on Formal Description Techniques, pp. 223\u2013238 (1994)","DOI":"10.1007\/978-0-387-34878-0_18"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0439-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0439-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0439-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,20]],"date-time":"2023-08-20T18:27:11Z","timestamp":1692556031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0439-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,2]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["439"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0439-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,2]]}}}