{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:54:40Z","timestamp":1773615280926,"version":"3.50.1"},"reference-count":15,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2014,12]]},"DOI":"10.3103\/s0146411614070232","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T19:16:45Z","timestamp":1422645405000},"page":"534-542","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["How to make a simple tool for verification of real-time systems"],"prefix":"10.3103","volume":"48","author":[{"given":"I. V.","family":"Konnov","sequence":"first","affiliation":[]},{"given":"V. V.","family":"Podymov","sequence":"additional","affiliation":[]},{"given":"D. Yu.","family":"Volkanov","sequence":"additional","affiliation":[]},{"given":"V. A.","family":"Zakharov","sequence":"additional","affiliation":[]},{"given":"D. A.","family":"Zorin","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2015,2,1]]},"reference":[{"key":"6355_CR1","volume-title":"From HUppaal to Uppaal: a translation from hierarchical timed automata to flat timed automata","author":"A David","year":"2001","unstructured":"David, A. and Moller, M.O., From HUppaal to Uppaal: a translation from hierarchical timed automata to flat timed automata, Research Series RS-01-11, BRICS, Department of Computer Science, University of Aarhus, 2001."},{"key":"6355_CR2","first-page":"187","volume":"1345","author":"ME Lakhnech","year":"1997","unstructured":"Lakhnech, M.E. and Siegal, M., Hierarchical automata as model for statechart, Lecture Notes Compt. Sci., 1997, vol. 1345, pp. 187\u2013196.","journal-title":"Lecture Notes Compt. Sci."},{"key":"6355_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF03160241","volume":"6","author":"H-y Chen","year":"2001","unstructured":"Chen Hai-yan, Dong Wei, and Wang Huo-wang, Verify UML statechart with SMV, Wuhan Univ. J. Natur. Sci., 2001, vol. 6, pp. 183\u2013190.","journal-title":"Wuhan Univ. J. Natur. Sci."},{"key":"6355_CR4","unstructured":"Jussila, J., Dubrovin, T., Junttila, T., and Latvala, I., Pores. Model checking dynamic and hierarchical UML state machines, Proc. 3rd Workshop on Model Design and Validation, 2006."},{"key":"6355_CR5","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11\u00e1","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., and Massink, M., Automatic verification of a behavioral subset of UML statechart diagrams using SPIN model-checker, Formal Aspects Compt., 1999, vol. 11\u00e1 pp. 637\u2013664.","journal-title":"Formal Aspects Compt."},{"key":"6355_CR6","volume-title":"vUML: A Tool for Verifying UML Models","author":"J Lilius","year":"1999","unstructured":"Lilius, J. and Paltor, I., vUML: A Tool for Verifying UML Models Technical Report TUCS-272. Turku Centre for Computer Science, 1999."},{"key":"6355_CR7","unstructured":"Ober, I., Graf, S., and Ober, I., Validating timed UML models by simulation and verification, Proc. Workshop on Specification and Validation of UML Models for Real Time and Embedded Systems, 2003."},{"key":"6355_CR8","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume":"3185","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., and Larsen, K.G., A tutorial on Uppaal, Lecture Notes in Compt. Sci., 2004, vol. 3185, pp. 200\u2013236.","journal-title":"Lecture Notes in Compt. Sci."},{"key":"6355_CR9","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume":"1066","author":"G Bengtsson","year":"1996","unstructured":"Bengtsson, G., Larsen, K.G., Larsson, F., Pettersson, P., and Yi, W., UPPAAL \u2014 a tool suite for automatic verification of real-time systems, Lecture Notes in Compt. Sci., 1996, vol. 1066, pp. 232\u2013243.","journal-title":"Lecture Notes in Compt. Sci."},{"key":"6355_CR10","volume-title":"Verification of UML Statechart with Real-Time Extensions","author":"A David","year":"2003","unstructured":"David, A., Moller, M.O., and Yi, W., Verification of UML Statechart with Real-Time Extensions IT Tech. Rep. 2003-009, Uppsala: Dep. of Information Technology, Uppsala University. 2003."},{"key":"6355_CR11","volume-title":"Innovation in Software and System Engineering","author":"ALN Muniz","year":"2009","unstructured":"Muniz, A.L.N., Andrade, A.M.S., and Lima, G., Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems, in Innovation in Software and System Engineering, 2009."},{"key":"6355_CR12","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume":"443","author":"R Alur","year":"1990","unstructured":"Alur, R. and Dill, D.L., Automata for modeling real-time systems, Lecture Notes in Compt. Sci., 1990, vol. 443, pp. 322\u2013335.","journal-title":"Lecture Notes in Compt. Sci."},{"key":"6355_CR13","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R. and Dill, D.L., A theory of timed automata. Theor. Compt. Sci., 1994, vol. 126, pp. 183\u2013235.","journal-title":"Theor. Compt. Sci."},{"key":"6355_CR14","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, M.C., and Grumberg, O., Characterizing finite Kripke structures in propositional temporal logics, Theor. Compt. Sci., 1988, vol. 59, pp. 115\u2013131.","journal-title":"Theor. Compt. Sci."},{"key":"6355_CR15","first-page":"316","volume-title":"Proc. Conf. UKRPROG-2000. Problems of Programming","author":"MV Chistolinov","year":"2000","unstructured":"Chistolinov, M.V., Epatko, I.V., Bahmurov, A.G., Smelyansky, R.L., Zakharov, V.A., Winter, K., and Usenko, Y., Towards a unified toolset for embedded systems development, Proc. Conf. UKRPROG-2000. Problems of Programming, 2000, nos.1\u20132, pp. 316\u2013322."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070232.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411614070232","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070232","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070232.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:49Z","timestamp":1773611869000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411614070232"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12]]},"references-count":15,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["6355"],"URL":"https:\/\/doi.org\/10.3103\/s0146411614070232","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12]]},"assertion":[{"value":"22 November 2006","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2015","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}