{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T03:34:25Z","timestamp":1775014465844,"version":"3.50.1"},"reference-count":22,"publisher":"Pleiades Publishing Ltd","issue":"6","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"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":["Program Comput Soft"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1134\/s0361768815060080","type":"journal-article","created":{"date-parts":[[2015,11,13]],"date-time":"2015-11-13T22:51:27Z","timestamp":1447455087000},"page":"325-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A combined toolset for the verification of real-time distributed systems"],"prefix":"10.1134","volume":"41","author":[{"given":"D. Yu.","family":"Volkanov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. A.","family":"Zakharov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D. A.","family":"Zorin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V. V.","family":"Podymov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I. V.","family":"Konnov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"key":"6278_CR1","first-page":"16","volume-title":"Trudy 3 Vserossiiskoi nauchnoi konferentsii","author":"V.V. Balashov","year":"2009","unstructured":"Balashov, V.V., Bakhmurov, A.G., Volkanov, D.Yu, Smeliansky, R.L., Chistolinov, M.V., and Yushchenko, N.V., A test facility for semirealistic simulation and development of embedded computer system, Trudy 3 Vserossiiskoi nauchnoi konferentsii (Proc. of the Third All-Russia Scientific Conference), Moscow: Mosk. Gos. Univ., 2009, pp. 16\u201325."},{"issue":"3","key":"6278_CR2","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D., Statecharts: A visual formalism for complex systems, in Sci. Comput. Program., 1987, vol. 8, no. 3, pp. 231\u2013274.","journal-title":"Sci. Comput. Program."},{"key":"6278_CR3","volume-title":"Designing Concurrent, Distributed,and Real-Time Applications with UML","author":"H. Gomaa","year":"2000","unstructured":"Gomaa, H., Designing Concurrent, Distributed,and Real-Time Applications with UML, Reading, Mass.: Addison-Wesley, 2000."},{"issue":"1","key":"6278_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., and Dill, D.L., Modelchecking in dense real-time, in Inf. Comput., 1993, vol. 104, no. 1, pp. 2\u201334.","journal-title":"Inf. Comput."},{"key":"6278_CR5","first-page":"55","volume-title":"Formal Methods for Real-Time Computing. Trends in Software","author":"R. Alur","year":"1996","unstructured":"Alur, R. and Dill, D.L., Automata-theoretic verification of real-time systems, in Formal Methods for Real-Time Computing. Trends in Software, Chichester: Wiley, 1996, pp. 55\u201382."},{"key":"6278_CR6","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume":"1066","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., and Yi, W., UPPAAL\u2014A tool suite for automatic verification of real-time systems, Lect. Notes Comput. Sci., 1996, vol. 1066, pp. 232\u2013243.","journal-title":"Lect. Notes Comput. Sci."},{"issue":"1","key":"6278_CR7","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., and Wong Hoi, H., HyTech: A model checker for hybrid systems, Int. J. Software Tools Technol. Transfer, 1997, vol. 1, no. 1, pp. 110\u2013122.","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"6278_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S., KRONOS: A verification tool for real-time systems, Int. J. Software Tools Technol. Transfer, 1997, vol. 1, nos. 1\u20132.","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"6278_CR9","volume-title":"Comparing verification with HyTech, Kronos and UPPAAL on the railroad crossing example","author":"D. Berard","year":"2000","unstructured":"Berard, D. and Sierra, L., Comparing verification with HyTech, Kronos and UPPAAL on the railroad crossing example, Research Report, 2000."},{"issue":"2","key":"6278_CR10","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s10009-005-0213-x","volume":"8","author":"S. Graf","year":"2002","unstructured":"Graf, S., Ober, I., and Ober, I., A real time profile for UML, Int. J. Software Tools Technol. Transfer, 2002, vol. 8, no. 2, pp. 113\u2013127.","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"6278_CR11","volume-title":"Univ. of Aarhus, Department of Computer Science","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, Univ. of Aarhus, Department of Computer Science, 2001, no. RS-01-11, BRICS."},{"key":"6278_CR12","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D. Latella","year":"1999","unstructured":"Latella, D., Majzik, I., and Massink, M., Automatic verification of a behavioural subset of UML statechart diagrams using SPIN model-checker, Formal Aspects Comput., 1999, vol. 11, pp. 637\u2013664.","journal-title":"Formal Aspects Comput."},{"issue":"1\u20132","key":"6278_CR13","first-page":"183","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. Natural Sci., 2001, vol. 6, no. 1\u20132, pp. 183\u2013190.","journal-title":"Wuhan Univ. J. Natural Sci."},{"key":"6278_CR14","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s11334-009-0103-6","volume":"6","author":"A.L.N. Muniz","year":"2010","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, Innovation Software Syst. Eng., 2010, vol. 6, pp. 29\u201337.","journal-title":"Innovation Software Syst. Eng."},{"key":"6278_CR15","volume-title":"IT Tech. Rep. of Uppsala University","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. of Uppsala University, Uppsala: Dep. of Information Technology, 2003, no. 2003-009."},{"key":"6278_CR16","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, Lect. Notes Comput. Sci., 2004, vol. 3185, pp. 200\u2013236.","journal-title":"Lect. Notes Comput. Sci."},{"key":"6278_CR17","volume-title":"Model Checking","author":"E.M. J.r. Clarke","year":"1999","unstructured":"Clarke, E.M., Jr., Grumberg, O., and Peled, D., Model Checking (Cambridge, Mass.: MIT Press, 1999; Moscow: Mosc. Tsentr Nepreryvnogo Matematicheskogo Obrazovaniya, 2002)."},{"key":"6278_CR18","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. Comput. Sci., 1994, vol. 126, pp. 183\u2013235.","journal-title":"Theor. Comput. Sci."},{"key":"6278_CR19","first-page":"1","volume-title":"Theories and Experiences for Real-Time System Development, AMAST Series in Computing","author":"R. Alur","year":"1994","unstructured":"Alur, R. and Henzinger, T.A., Real-time system = discrete system + clock variables, in Theories and Experiences for Real-Time System Development, AMAST Series in Computing, 1994, pp. 1\u201330."},{"key":"6278_CR20","volume-title":"Mat. Anal., Inf. Sist.","author":"D.Yu. Volkanov","year":"2012","unstructured":"Volkanov, D.Yu., Zakharov, V.A., Zorin, D.A., Konnov, I.V., and Podymov, V.V., How to develop a simple tool for the verification of real-time systems, Mat. Anal., Inf. Sist., 2012, no. 4."},{"key":"6278_CR21","first-page":"601","volume-title":"Proc. of the Int. Multiconference on Computer Science and Information Technology","author":"A. Furfaro","year":"2008","unstructured":"Furfaro, A. and Nigro, L., Embedded control systems design based on RT-DEVS and temporal analysis using UPPAAL, in Proc. of the Int. Multiconference on Computer Science and Information Technology, 2008, pp. 601\u2013608."},{"key":"6278_CR22","first-page":"316","volume":"1\u20132","author":"M.V. 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, in Proc. of the Conference UKRPROG-2000 Problems of Programming, 2000, nos. 1\u20132, pp. 316\u2013322.","journal-title":"Proc. of the Conference UKRPROG-2000 Problems of Programming"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815060080.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768815060080","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815060080","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815060080.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:18:47Z","timestamp":1775009927000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768815060080"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["6278"],"URL":"https:\/\/doi.org\/10.1134\/s0361768815060080","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]},"assertion":[{"value":"17 November 2012","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 November 2015","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}