{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T03:54:51Z","timestamp":1763178891084},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,7,22]],"date-time":"2015-07-22T00:00:00Z","timestamp":1437523200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2017,5]]},"DOI":"10.1007\/s10270-015-0484-y","type":"journal-article","created":{"date-parts":[[2015,7,21]],"date-time":"2015-07-21T02:25:06Z","timestamp":1437445506000},"page":"393-415","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Language-specific model checking of UML-RT models"],"prefix":"10.1007","volume":"16","author":[{"given":"Karolina","family":"Zurowska","sequence":"first","affiliation":[]},{"given":"Juergen","family":"Dingel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,22]]},"reference":[{"key":"484_CR1","doi-asserted-by":"publisher","unstructured":"Balasubramanian, D., P\u0103s\u0103reanu, C.S., Karsai, G., Lowry, M.R.: Polyglot: systematic analysis for multiple statechart formalisms. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 523\u2013529. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_36"},{"key":"484_CR2","doi-asserted-by":"publisher","unstructured":"Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL. In: Symposium on Logic in Computer Science, pp. 388\u2013397. IEEE, New York (1995)","DOI":"10.1109\/LICS.1995.523273"},{"key":"484_CR3","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"484_CR4","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Logic in Computer Science LICS, pp. 353\u2013362 (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"484_CR5","unstructured":"Concrete syntax for a UML action language: Action Language for Foundational UML (ALF). http:\/\/www.omg.org\/spec\/ALF\/ . Last accessed 21 June 2014"},{"key":"484_CR6","unstructured":"Compton, K., Gurevich, Y., Huggins, J., Shen, W.: An automatic verification tool for UML. Technical report, University of Michigan (2000)"},{"key":"484_CR7","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Kurshan, R. (ed.) Computer-Aided Verification, pp. 129\u2013142. Springer, Berlin (1993)","DOI":"10.1007\/3-540-56922-7"},{"key":"484_CR8","doi-asserted-by":"publisher","unstructured":"Giese, H., Tichy, M., Burmester, S., Sch\u00e4fer, W., Flake, S.: Towards the compositional verification of real-time UML designs. In: Proceedings of the ESEC\/FSE, pp. 38\u201347 (2003)","DOI":"10.1145\/940071.940078"},{"key":"484_CR9","doi-asserted-by":"publisher","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification, pp. 186\u2013196. Springer, Berlin (1991)","DOI":"10.1007\/BFb0023732"},{"key":"484_CR10","doi-asserted-by":"publisher","unstructured":"Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 191\u2013205. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_13"},{"key":"484_CR11","unstructured":"IBM. IBM Rational Rhapsody. http:\/\/www.ibm.com\/developerworks\/rational\/products\/rhapsody\/"},{"key":"484_CR12","unstructured":"IBM rational software architect, realtime edition, version 8.0.2. http:\/\/publib.boulder.ibm.com\/infocenter\/ . Last accessed 21 June 2014"},{"key":"484_CR13","doi-asserted-by":"publisher","unstructured":"Jensen, H.E., Larsen, G.K., Skou, A.: Scaling up uppaal. In: Joseph, M. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 641\u2013678. Springer, Berlin (2000)","DOI":"10.1007\/3-540-45352-0_4"},{"key":"484_CR14","unstructured":"Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proceedings of the 3rd Workshop on Model Design and Validation MoDeVa, pp. 94\u2013110 (2006)"},{"issue":"6","key":"484_CR15","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Form. Asp. Comput. 11(6), 637\u2013664 (1999)","journal-title":"Form. Asp. Comput."},{"key":"484_CR16","doi-asserted-by":"crossref","unstructured":"Leue, S., Stefanescu, A., Wei, W.: An AsmL semantics for dynamic structures and run time schedulability in UML-RT. Technical report, University of Konstanz, Konstanz (2008)","DOI":"10.1007\/978-3-540-69824-1_14"},{"issue":"1","key":"484_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1008736219484","volume":"18","author":"J Lind-Nielsen","year":"2001","unstructured":"Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K., Larsen, K.G.: Verification of large state\/event systems using compositionality and dependency analysis. Form. Methods Syst. Des. 18(1), 5\u201323 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"484_CR18","doi-asserted-by":"publisher","unstructured":"Mehlitz, P.C.: Trust your model\u2013verifying aerospace system models with Java pathfinder. In: IEEE Aerospace Conference (2008)","DOI":"10.1109\/AERO.2008.4526573"},{"key":"484_CR19","doi-asserted-by":"crossref","unstructured":"Posse, E., Dingel, J.: An executable formal semantics for UML-RT. Softw. Syst. Model. 1\u201339 (2014)","DOI":"10.1007\/s10270-014-0399-z"},{"key":"484_CR20","unstructured":"Saaltink, M., Meisels, I.: Using SPIN to analyse RoseRT models. Technical report, ORA Canada (1999)"},{"issue":"3","key":"484_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T Sch\u00e4fer","year":"2001","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. Electron. Notes Theor. Comput. Sci. 55(3), 1\u201313 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"484_CR22","volume-title":"Real-Tme Object Oriented Modeling and Design","author":"B Selic","year":"1994","unstructured":"Selic, B., Gullekson, G., Ward, P.T.: Real-Tme Object Oriented Modeling and Design. Wiley, London (1994)"},{"key":"484_CR23","unstructured":"Shen, W., Compton, K., Huggins, J.: A UML validation toolset based on abstract state machines. In: International Conference on Automated Software Engineering, pp. 315\u2013318 (2001)"},{"key":"484_CR24","unstructured":"Unified Modeling Language (UML 2.0) superstructure. http:\/\/www.uml.org\/ . Last accessed 21 June 2014"},{"key":"484_CR25","doi-asserted-by":"publisher","unstructured":"Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: CONCUR, pp. 447\u2013461. Springer, Berlin (1993)","DOI":"10.1007\/3-540-57208-2_31"},{"issue":"4","key":"484_CR26","first-page":"541","volume":"11","author":"W Visser","year":"2012","unstructured":"Visser, W., Dwyer, M.B., Whalen, M.: The hidden models of model checking. Softw. Syst. Model. 11(4), 541\u2013555 (2012)","journal-title":"Softw. Syst. Model."},{"key":"484_CR27","doi-asserted-by":"publisher","unstructured":"Zheng, H.: Compositional reachability analysis for efficient modular verification of asynchronous designs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(3), 329\u2013340 (2010)","DOI":"10.1109\/TCAD.2009.2035544"},{"key":"484_CR28","unstructured":"Zurowska, K.: Language specific analysis of state machine models of reactive systems. Ph.D. thesis, Queen\u2019s Univerity, Canada (2014)"},{"key":"484_CR29","doi-asserted-by":"publisher","unstructured":"Zurowska, K., Dingel, J.: Symbolic execution of communicating and hierarchically composed UML-RT state machines. In: Goodloe, A.E., Person, S. (eds.) NASA Formal Methods, pp. 39\u201353. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28891-3_6"},{"key":"484_CR30","doi-asserted-by":"publisher","unstructured":"Zurowska, K., Dingel, J.: Model checking of UML-RT models using lazy composition. In: MoDELS, pp. 304\u2013319 (2013)","DOI":"10.1007\/978-3-642-41533-3_19"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0484-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-015-0484-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0484-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0484-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T09:58:56Z","timestamp":1566986336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-015-0484-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,22]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["484"],"URL":"https:\/\/doi.org\/10.1007\/s10270-015-0484-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,22]]}}}