{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:55:13Z","timestamp":1761929713161,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319076010"},{"type":"electronic","value":"9783319076027"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07602-7_21","type":"book-chapter","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T11:29:08Z","timestamp":1402572548000},"page":"348-368","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Define, Verify, Refine: Correct Composition and Transformation of Concurrent System Semantics"],"prefix":"10.1007","author":[{"given":"Anton","family":"Wijs","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"21_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447\u2013466 (2010)","journal-title":"STTT"},{"issue":"3","key":"21_CR3","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the Bip framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"21_CR4","unstructured":"Blech, J.O., Glesner, S., Leitner, J.: Formal verification of Java code generation from UML models. In: Fujaba Days 2005, pp. 49\u201356 (2005)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013)"},{"key":"21_CR6","unstructured":"Engelen, L.J.P., Wijs, A.J.: Checking property preservation of refining transformations for model-driven development. CS-Report 12\u201308, TU Eindhoven (2012)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/11603009_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"WJ Fokkink","year":"2005","unstructured":"Fokkink, W.J., Pang, J., Wijs, A.J.: Is timed branching bisimilarity an equivalence indeed? In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 258\u2013272. Springer, Heidelberg (2005)"},{"key":"21_CR8","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. 6605, pp. 372\u2013387. Springer, Heidelberg (2011)"},{"key":"21_CR9","unstructured":"Giese, H., Glesner, S., Leitner, J., Sch\u00e4fer, W., Wagner, R.: Towards verified model transformations. In: 3rd International Workshop on Model Development, Validation and Verification (MoDeVVa 2006), pp. 78\u201393. IEEE Press, New York (2006)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-33654-6_17","volume-title":"Graph Transformations","author":"H Giese","year":"2012","unstructured":"Giese, H., Lambers, L.: Towards automatic verification of behavior preservation for model transformation via invariant checking. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 249\u2013263. Springer, Heidelberg (2012)"},{"issue":"4","key":"21_CR11","doi-asserted-by":"crossref","first-page":"371","DOI":"10.3233\/FI-2009-109","volume":"93","author":"RJ van Glabbeek","year":"2009","unstructured":"van Glabbeek, R.J., Luttik, B., Tr\u010dka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371\u2013392 (2009)","journal-title":"Fundam. Inform."},{"issue":"3","key":"21_CR12","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"issue":"3\u20134","key":"21_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","volume":"26","author":"A Habel","year":"1996","unstructured":"Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform. 26(3\u20134), 287\u2013313 (1996)","journal-title":"Fundam. Inform."},{"key":"21_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/j.entcs.2005.12.018","volume":"148","author":"R Heckel","year":"2006","unstructured":"Heckel, R.: Graph transformation in a nutshell. Electron. Notes Theor. Comput. Sci. 148, 187\u2013198 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16265-7_14","volume-title":"Integrated Formal Methods","author":"M H\u00fclsbusch","year":"2010","unstructured":"H\u00fclsbusch, M., K\u00f6nig, B., Rensink, A., Semenyak, M., Soltenborn, Ch., Wehrheim, H.: Showing full semantics preservation in model transformation - a comparison of techniques. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 183\u2013198. Springer, Heidelberg (2010)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-642-03429-9_14","volume-title":"Recent Trends in Algebraic Development Techniques","author":"T Kahsai","year":"2009","unstructured":"Kahsai, T., Roggenbach, M.: Property preserving refinement for Csp-Casl. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 206\u2013220. Springer, Heidelberg (2009)"},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theoret. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Kundu, S., Lerner S., Gupta, R.: Automated refinement checking of concurrent systems. In: 26th International Conference on Computer-Aided Design (ICCAD 2007), pp. 318\u2013325. IEEE Press, New York (2007)","DOI":"10.1109\/ICCAD.2007.4397284"},{"key":"21_CR19","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2008.04.026","volume":"211","author":"L Lambers","year":"2008","unstructured":"Lambers, L., Ehrig, H.: Efficient conflict detection in graph transformation systems by essential critical pairs. Electron. Notes Theor. Comput. Sci. 211, 17\u201326 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/11589976_6","volume-title":"Integrated Formal Methods","author":"F Lang","year":"2005","unstructured":"Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification Methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70\u201388. Springer, Heidelberg (2005)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22306-8_2","volume-title":"Model Checking Software","author":"R Mateescu","year":"2011","unstructured":"Mateescu, R., Wijs, A.: Property-dependent reductions for the modal mu-calculus. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 2\u201319. Springer, Heidelberg (2011)"},{"key":"21_CR22","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.entcs.2008.04.041","volume":"211","author":"A Narayanan","year":"2008","unstructured":"Narayanan, A., Karsai, G.: Towards verifying model transformations. Electron. Notes Theor. Comput. Sci. 211, 191\u2013200 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-58179-0_67","volume-title":"Computer Aided Verification","author":"OV Sokolsky","year":"1994","unstructured":"Sokolsky, O.V., Smolka, S.A.: Incremental model checking in the modal mu-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 351\u2013363. Springer, Heidelberg (1994)"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Swamy, G.M.: Incremental methods for formal verification and logic synthesis. Ph.D. thesis, University of California (1996)","DOI":"10.2139\/ssrn.3702088"},{"key":"21_CR25","unstructured":"Varr\u00f3, D., Pataricza, A.: Automated formal verification of model transformations. In: Critical Systems Development with UML (CSDUML 2003), pp. 63\u201378 (2003)"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Wijs, A.J.: Achieving Discrete relative timing with untimed process algebra. In: 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), pp. 35\u201344. IEEE Press, New York (2007)","DOI":"10.1109\/ICECCS.2007.13"},{"key":"21_CR27","unstructured":"Wijs, A.J.: What to do next?: analysing and optimising system behaviour in time. Ph.D. thesis, VU University, Amsterdam (2007)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Wijs, A.J., Engelen, L.J.P.: Incremental formal verification for model refining. In: 9th International Workshop on Model Development, Validation and Verification (MoDeVVa 2012), pp. 29\u201334. ACM Press, New York (2012)","DOI":"10.1145\/2427376.2427382"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-642-36742-7_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2013","unstructured":"Wijs, A., Engelen, L.: Efficient property preservation checking of model refinements. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 565\u2013579. Springer, Heidelberg (2013)"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-540-74128-2_11","volume-title":"Model Checking and Artificial Intelligence","author":"AJ Wijs","year":"2007","unstructured":"Wijs, A.J., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 166\u2013184. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07602-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:44:05Z","timestamp":1746265445000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-07602-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319076010","9783319076027"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07602-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"13 June 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}