{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,20]],"date-time":"2024-08-20T13:10:17Z","timestamp":1724159417945},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1-2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s11334-009-0116-1","type":"journal-article","created":{"date-parts":[[2010,2,6]],"date-time":"2010-02-06T03:52:28Z","timestamp":1265428348000},"page":"83-90","source":"Crossref","is-referenced-by-count":30,"title":["Towards model checking executable UML specifications in mCRL2"],"prefix":"10.1007","volume":"6","author":[{"given":"Helle Hvid","family":"Hansen","sequence":"first","affiliation":[]},{"given":"Jeroen","family":"Ketema","sequence":"additional","affiliation":[]},{"given":"Bas","family":"Luttik","sequence":"additional","affiliation":[]},{"given":"MohammadReza","family":"Mousavi","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,7]]},"reference":[{"issue":"3","key":"116_CR1","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R Alur","year":"2001","unstructured":"Alur R, Yannakakis M (2001) Model checking of hierarchical state machines. ACM Trans Program Lang Syst 23(3): 273\u2013303","journal-title":"ACM Trans Program Lang Syst"},{"key":"116_CR2","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press, New York"},{"issue":"1\u20133","key":"116_CR3","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra JA, Klop JW (1984) Process algebra for synchronous communicati. Inf Control 60(1\u20133): 109\u2013137","journal-title":"Inf Control"},{"key":"116_CR4","doi-asserted-by":"crossref","unstructured":"Blom S, van de Pol J (2008) Symbolic reachability for process algebras with recursive data types. In: Proceedings on theoretical aspects of computing (ICTAC 2008). Lecture Notes in Computer Science, vol 5160. Springer, Berlin, pp 81\u201395","DOI":"10.1007\/978-3-540-85762-4_6"},{"key":"116_CR5","unstructured":"Blom SCC, van de Pol JC, Weber M (2009) Bridging the gap between enumerative and symbolic model checkers. Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede"},{"issue":"4","key":"116_CR6","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A Cimatti","year":"1998","unstructured":"Cimatti A, Giunchiglia F, Mongardi G, Romano D, Torielli F, Traverso P (1998) Formal verification of a railway interlocking system using model checking. Formal Aspects Comput 10(4): 361\u2013380","journal-title":"Formal Aspects Comput"},{"key":"116_CR7","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/j.scico.2004.05.012","volume":"55","author":"W Damm","year":"2005","unstructured":"Damm W, Josko B, Pnueli A, Votintseva A (2005) A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci Comput Program 55: 81\u2013155","journal-title":"Sci Comput Program"},{"key":"116_CR8","doi-asserted-by":"crossref","unstructured":"Eriksson L-H (1996) Specifying railway interlocking requirements for practical use. In: Proceedings of the 15th international conference on computer safety, reliability and security (SAFECOMP\u201996). Springer, Berlin","DOI":"10.1007\/978-1-4471-0937-2_21"},{"key":"116_CR9","unstructured":"Xie F, Levin V, Browne J (2001) Model checking for an executable subset of UML. In: 16th IEEE international conference on automated software engineering (ASE 2001), pp 333\u2013336"},{"key":"116_CR10","unstructured":"Fokkink W (1996) Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In: 5th conference on computers in railways (COMPRAIL\u201996). Volume I: railway systems and management"},{"key":"116_CR11","doi-asserted-by":"crossref","unstructured":"Gnesi S, Latella D, Lenzini G, Abbaneo C, Amendola AM, Marmo P (2000) An automatic SPIN validation of a safety critical railway control system. In: Proceedings of the 2000 international conference on dependable systems and networks. IEEE Computer Society, Washington, DC, pp 119\u2013124","DOI":"10.1109\/ICDSN.2000.857524"},{"key":"116_CR12","unstructured":"Groote JF, Mathijssen A, Reniers MA, Usenko YS, van Weerdenburg M (2007) The formal specification language mCRL2. In: Proceedings of methods for modelling software systems, Dagstuhl seminar proceedings, vol 06351"},{"issue":"4","key":"116_CR13","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/s10515-006-0272-6","volume":"13","author":"Z Hu","year":"2006","unstructured":"Hu Z, Shatz SM (2006) Explicit modeling of semantics associated with composite states in UML statecharts. J Autom Softw Eng 13(4): 423\u2013467","journal-title":"J Autom Softw Eng"},{"key":"116_CR14","unstructured":"KnowGravity (2008) Cassandra\/xUML user\u2019s guide. http:\/\/www.knowgravity.com\/eng\/value\/cassandra.htm"},{"key":"116_CR15","volume-title":"Executable UML: a foundation for model-driven architecture","author":"SJ Mellor","year":"2002","unstructured":"Mellor SJ, Balcer M (2002) Executable UML: a foundation for model-driven architecture. Addison Wesley, Reading"},{"key":"116_CR16","unstructured":"Object Management Group (2008) Semantics of a foundational subset for executable UML models. http:\/\/www.omg.org\/spec\/FUML\/1.0\/Beta1\/PDF\/ . Accessed Nov 2008"},{"key":"116_CR17","unstructured":"Object Management Group (2009) OMG unified modeling language superstructure version 2.2. http:\/\/www.omg.org\/spec\/UML\/2.2\/Superstructure\/PDF\/ . Accessed Feb 2009"},{"key":"116_CR18","unstructured":"Purandar B, Ramesh S (2004) Model checking of statechart models: survey and research directions. http:\/\/arxiv.org\/abs\/cs.SE\/0407038 . Accessed July 2004"},{"key":"116_CR19","doi-asserted-by":"crossref","unstructured":"Turner E, Treharne H, Schneider S, Evans N (2008) Automatic generation of CSP || B skeletons from xUML models. In: Proc. of Theoretical Aspects of Computing (ICTAC 2008), pp. 364\u2013379","DOI":"10.1007\/978-3-540-85762-4_25"},{"key":"116_CR20","doi-asserted-by":"crossref","unstructured":"von der Beeck M (2001) Formalization of UML-statecharts. In: Proceedings UML 2001. Lecture Notes in Computer Science, vol 2185. Springer, Berlin, pp 406\u2013421","DOI":"10.1007\/3-540-45441-1_30"},{"key":"116_CR21","unstructured":"Winter K, Robinson NJ (2003) Modelling large railway interlockings and model checking small ones. In: ACSC \u201903: Proceedings of the 26th Australasian computer science conference, pp 309\u2013316. Australian Computer Society, Inc."},{"key":"116_CR22","doi-asserted-by":"crossref","unstructured":"Yeung WL, Leung KRPH, Wang J, Dong W (2005) Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific software engineering conference (APSEC 2005). IEEE Computer Society","DOI":"10.1109\/APSEC.2005.70"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0116-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T16:34:56Z","timestamp":1558802096000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0116-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,7]]},"references-count":22,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["116"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0116-1","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,7]]}}}