{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:27:19Z","timestamp":1749421639962,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642252709"},{"type":"electronic","value":"9783642252716"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25271-6_12","type":"book-chapter","created":{"date-parts":[[2011,12,14]],"date-time":"2011-12-14T20:56:11Z","timestamp":1323896171000},"page":"225-250","source":"Crossref","is-referenced-by-count":15,"title":["Automated Verification of Executable UML Models"],"prefix":"10.1007","author":[{"given":"Helle","family":"Hvid 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":[]},{"given":"Osmar Marchi","family":"dos Santos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R. Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Transactions on Programming Languages and Systems\u00a023(3), 273\u2013303 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"M.H. Beek ter","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Science of Computer Programming\u00a076(2), 119\u2013135 (2011)","journal-title":"Science of Computer Programming"},{"issue":"2","key":"12_CR4","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1016095519611","volume":"21","author":"G. Behrmann","year":"2002","unstructured":"Behrmann, G., Larsen, K.G., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J.: Verification of hierarchical state\/event systems using reusability and compositionality. Formal Methods in System Design\u00a021(2), 225\u2013244 (2002)","journal-title":"Formal Methods in System Design"},{"issue":"1-3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control\u00a060(1-3), 109\u2013137 (1984)","journal-title":"Information and Control"},{"key":"12_CR6","first-page":"118","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-31848-4_9","volume-title":"Formal Approaches to Software Testing","author":"J. Blom","year":"2005","unstructured":"Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol.\u00a03395, pp. 125\u2013139. Springer, Heidelberg (2005)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"issue":"1","key":"12_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10703-006-0033-y","volume":"31","author":"G. Ciardo","year":"2007","unstructured":"Ciardo, G., L\u00fcttgen, G., Miner, A.S.: Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design\u00a031(1), 63\u2013100 (2007)","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"12_CR10","doi-asserted-by":"publisher","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.: Formal verification of a railway interlocking system using model checking. Formal Aspects of Computing\u00a010(4), 361\u2013380 (1998)","journal-title":"Formal Aspects of Computing"},{"issue":"5","key":"12_CR11","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM"},{"key":"12_CR12","doi-asserted-by":"publisher","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.: A discrete-time UML semantics for concurrency and communication in safety-critical applications. Science of Computer Programming\u00a055, 81\u2013155 (2005)","journal-title":"Science of Computer Programming"},{"key":"12_CR13","volume-title":"Proceedings of the 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1996)","author":"L.-H. Eriksson","year":"1996","unstructured":"Eriksson, L.-H.: Specifying railway interlocking requirements for practical use. In: Proceedings of the 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1996). Springer, Heidelberg (1996)"},{"key":"12_CR14","unstructured":"Fokkink, W.: Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In: Computers in Railways V (COMPRAIL 1996). Railway Systems and Management, vol.\u00a0I (1996)"},{"key":"12_CR15","unstructured":"Formal Systems (Europe) Ltd. Failures-divergence refinement: FDR2 User Manual (2010)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-19835-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"2011","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 372\u2013387. Springer, Heidelberg (2011)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. Electr. Notes in Theor. Comp. Sci.\u00a055(2) (2001)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"issue":"2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s10626-009-0060-0","volume":"19","author":"M. Ghazel","year":"2009","unstructured":"Ghazel, M., Toguy\u00e9ni, A., Yim, P.: State observer for DES under partial observation with timed petri nets. Discrete Event Dynamic Systems\u00a019(2), 137\u2013165 (2009)","journal-title":"Discrete Event Dynamic Systems"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1109\/ICDSN.2000.857524","volume-title":"Proceedings of the 2000 Int. Conf. on Dependable Systems and Networks","author":"S. Gnesi","year":"2000","unstructured":"Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A.M., Marmo, P.: An automatic SPIN validation of a safety critical railway control system. In: Proceedings of the 2000 Int. Conf. on Dependable Systems and Networks, pp. 119\u2013124. IEEE Computer Society, Washington, DC, USA (2000)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Graw, G., Herrmann, P.: Transformation and verification of Executable UML models. In: Proceedings of the Workshop on the Compositional Verification of UML Models. Electr. Notes in Theor. Comp. Sci, vol.\u00a0101, pp. 3\u201324 (2004)","DOI":"10.1016\/j.entcs.2004.09.006"},{"key":"12_CR21","unstructured":"Groote, J.F., Mathijssen, A., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.: The formal specification language mCRL2. In: Methods for Modelling Software Systems. Dagstuhl Seminar Proceedings, vol.\u00a006351 (2007)"},{"issue":"1-2","key":"12_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"H.H. Hansen","year":"2010","unstructured":"Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J.: Towards model checking Executable UML specifications in mCRL2. Innovations in Systems and Software Engineering\u00a06(1-2), 83\u201390 (2010)","journal-title":"Innovations in Systems and Software Engineering"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-02674-4_9","volume-title":"Model Driven Architecture - Foundations and Applications","author":"F. Heidenreich","year":"2009","unstructured":"Heidenreich, F., Johannes, J., Karol, S., Seifert, M., Wende, C.: Derivation and refinement of textual syntax for models. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol.\u00a05562, pp. 114\u2013129. Springer, Heidelberg (2009), http:\/\/www.emftext.org (last visit: July 4, 2011)"},{"key":"12_CR24","volume-title":"Communicating Sequential Processes","author":"T. Hoare","year":"1985","unstructured":"Hoare, T.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"12_CR25","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"12_CR26","unstructured":"ISO\/IEC. Enhancements to Lotos (E-Lotos), International Standard 15437:2001 (2001)"},{"key":"12_CR27","unstructured":"ISO\/IEEE. ISO\/IEEE 11073-20601: Health infomatics \u2014 personal health device communication \u2014 Part 20601: Application profile \u2014 optimized exchange protocol (April 2010)"},{"key":"12_CR28","unstructured":"Keiren, J.: Modelling session setup of IEEE Std 11073-20601 (2011), Personal communication"},{"key":"12_CR29","unstructured":"KnowGravity. Cassandra\/xUML User\u2019s Guide (2008)"},{"key":"12_CR30","unstructured":"Kolovos, D.: An Extensible Platform for Specification of Integrated Languages for Model Management. PhD thesis, University of York, United Kingdom (2009), http:\/\/www.eclipse.org\/gmt\/epsilon\/ (last visit: July 4, 2011)"},{"key":"12_CR31","unstructured":"Kolovos, D., Rose, L., Paige, R.: The Epsilon Book, http:\/\/www.eclipse.org\/gmt\/epsilon\/doc\/book\/ (last visit: July 4, (2011)"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Lafortune, S., Teneketzis, D., Sampath, M., Sengupta, R., Sinnamohideen, K.: Failure diagnosis of dynamic systems: an approach based on discrete event systems. In: Proceedings of the American Control Conference, vol.\u00a03, pp. 2058\u20132071 (2001)","DOI":"10.1109\/ACC.2001.946047"},{"issue":"1","key":"12_CR33","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.J., Larsen, K.G.: Verification of large state\/event systems using compositionality and dependency analysis. Formal Methods in System Design\u00a018(1), 5\u201323 (2001)","journal-title":"Formal Methods in System Design"},{"key":"12_CR34","unstructured":"Mekki, A., Ghazel, M., Toguyeni, A.: Time-constrained systems validation using MDA model transformation. A railway case study. In: Proceedings of the 8th International Conference of Modeling and Simulation, MOSIM 2010 (2010)"},{"key":"12_CR35","volume-title":"Executable UML: A foundation for model-driven architecture","author":"S.J. Mellor","year":"2002","unstructured":"Mellor, S.J., Balcer, M.: Executable UML: A foundation for model-driven architecture. Addison-Wesley, Reading (2002)"},{"key":"12_CR36","unstructured":"Object Management Group. OMG Unified Modeling Language Superstructure Version 2.2 (February 2009)"},{"key":"12_CR37","unstructured":"Papyrus Developers. Papyrus: Open source tool for graphical UML2 modelling, http:\/\/www.papyrusuml.org (last visit: July 4, 2011)"},{"issue":"1","key":"12_CR38","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and Systems Security\u00a03(1), 30\u201350 (2000)","journal-title":"ACM Transactions on Information and Systems Security"},{"key":"12_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"12_CR40","unstructured":"Sighireanu, M.: LOTOS NT user\u2019s manual. Technical report, INRIA Rh\u00f4ne-Alpes\/VASY (2008)"},{"key":"12_CR41","volume-title":"EMF: Eclipse Modeling Framework","author":"D. Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework. Addison-Wesley Professional, Boston (2008), http:\/\/www.eclipse.org\/modeling\/emf\/ (last visit: July 4, 2011)"},{"key":"12_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-540-85762-4_25","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"E. Turner","year":"2008","unstructured":"Turner, E., Treharne, H., Schneider, S., Evans, N.: Automatic generation of CSP || B skeletons from xUML models. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 364\u2013379. Springer, Heidelberg (2008)"},{"key":"12_CR43","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: ACSC 2003: Proceedings of the 26th Australasian Comp. Sci. Conference, pp. 309\u2013316. Australian Computer Society, Inc. (2003)"},{"key":"12_CR44","volume-title":"Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005)","author":"W.L. Yeung","year":"2005","unstructured":"Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005). IEEE Computer Society, Los Alamitos (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25271-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,20]],"date-time":"2019-06-20T19:29:03Z","timestamp":1561058943000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25271-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642252709","9783642252716"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25271-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}