{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:14:39Z","timestamp":1725804879391},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319112442"},{"type":"electronic","value":"9783319112459"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11245-9_13","type":"book-chapter","created":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T04:35:11Z","timestamp":1409978111000},"page":"221-240","source":"Crossref","is-referenced-by-count":9,"title":["Model Checking of CTL-Extended OCL Specifications"],"prefix":"10.1007","author":[{"given":"Robert","family":"Bill","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"Gabmeyer","sequence":"additional","affiliation":[]},{"given":"Petra","family":"Kaufmann","sequence":"additional","affiliation":[]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-16145-2_9","volume-title":"Model Driven Engineering Languages and Systems","author":"T. Arendt","year":"2010","unstructured":"Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: Advanced Concepts and Tools for In-Place EMF Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, \u00d8. (eds.) MODELS 2010, Part I. LNCS, vol.\u00a06394, pp. 121\u2013135. Springer, Heidelberg (2010)"},{"key":"13_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"13_CR3","unstructured":"Bill, R., Gabmeyer, S., Kaufmann, P., Seidl, M.: OCL meets CTL: Towards CTL-Extended OCL Model Checking. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol.\u00a01092, pp. 13\u201322. Springer, Heidelberg (1996)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bill, R., Gabmeyer, S., Kaufmann, P., Seidl, M.: Model Checking of CTL-Extended OCL Specifications. Tech. Rep. BIG-TR-2014-2, E188 - Institut f\u00fcr Softwaretechnik und Interaktive Systeme; Technische Universit\u00e4t Wien (2014)","DOI":"10.1007\/978-3-319-11245-9_13"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-45923-5_14","volume-title":"Fundamental Approaches to Software Engineering","author":"J.C. Bradfield","year":"2002","unstructured":"Bradfield, J.C., K\u00fcster Filipe, J., Stevens, P.: Enriching OCL Using Observational Mu-Calculus. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, pp. 203\u2013217. Springer, Heidelberg (2002)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"13_CR7","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (1999)"},{"key":"13_CR8","series-title":"IFIP AICT","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-0-387-35520-7_16","volume-title":"Formal Methods for Open Object-Based Distributed Systems IV","author":"D. Distefano","year":"2000","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: On a Temporal Logic for Object-Based Systems. In: Formal Methods for Open Object-Based Distributed Systems IV. IFIP AICT, vol.\u00a049, pp. 305\u2013325. Springer, Heidelberg (2000)"},{"issue":"7","key":"13_CR9","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"13_CR11","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)"},{"issue":"3","key":"13_CR12","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10270-003-0026-x","volume":"2","author":"S. Flake","year":"2003","unstructured":"Flake, S., M\u00fcller, W.: Formal semantics of static and temporal state-oriented OCL constraints. Software and System Modeling\u00a02(3), 164\u2013186 (2003)","journal-title":"Software and System Modeling"},{"key":"13_CR13","unstructured":"Gabmeyer, S., Kaufmann, P., Seidl, M.: A feature-based classification of formal verification techniques for software models. Tech. Rep. BIG-TR-2014-1, Institut f\u00fcr Softwaretechnik und Interaktive Systeme; Technische Universit\u00e4t Wien (2014)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv.\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"13_CR15","unstructured":"Jussila, T., Dubrovin, J., Junttila, T., Latvala, T.L., Porres, I.: Model Checking Dynamic and Hierarchical UML State Machines. In: Models in Software Engineering. LNCS, vol.\u00a04364, p. 15. Springer (2006)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-36089-3_6","volume-title":"Software Language Engineering","author":"B. Kanso","year":"2013","unstructured":"Kanso, B., Taha, S.: Temporal Constraint Support for OCL. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol.\u00a07745, pp. 83\u2013103. Springer, Heidelberg (2013)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/11691617_19","volume-title":"Model Checking Software","author":"H. Kastenberg","year":"2006","unstructured":"Kastenberg, H., Rensink, A.: Model Checking Dynamic States in GROOVE. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 299\u2013305. Springer, Heidelberg (2006)"},{"issue":"2","key":"13_CR18","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C. Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal Verification in Hardware Design: A Survey. ACM Transactions on Design Automation of Electronic Systems (TODAES)\u00a04(2), 123\u2013193 (1999)","journal-title":"ACM Transactions on Design Automation of Electronic Systems (TODAES)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-69489-2_6","volume-title":"Models in Software Engineering","author":"A. Knapp","year":"2007","unstructured":"Knapp, A., Wuttke, J.: Model Checking of UML 2.0 Interactions. In: K\u00fchne, T. (ed.) MoDELS 2006. LNCS, vol.\u00a04364, pp. 42\u201351. Springer, Heidelberg (2007)"},{"key":"13_CR20","unstructured":"Lail, M.A., Abdunabi, R., France, R., Ray, I.: An Approach to Analyzing Temporal Properties in UML Class Models. In: Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa 2013). CEUR Workshop Proceedings, vol.\u00a01069, pp. 77\u201386. CEUR-WS.org (2013)"},{"issue":"9","key":"13_CR21","doi-asserted-by":"publisher","first-page":"1307","DOI":"10.1109\/TSE.2013.14","volume":"39","author":"Y. Moffett","year":"2013","unstructured":"Moffett, Y., Dingel, J., Beaulieu, A.: Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems. IEEE Software Engineering\u00a039(9), 1307\u201313256 (2013)","journal-title":"IEEE Software Engineering"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-540-72952-5_4","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Mullins","year":"2007","unstructured":"Mullins, J., Oarga, R.: Model Checking of Extended OCL Constraints on UML Models in SOCLe. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 59\u201375. Springer, Heidelberg (2007)"},{"key":"13_CR23","unstructured":"Rensink, A., Zambon, E.: Neighbourhood Abstraction in GROOVE. ECEASST\u00a032, 44\u201356"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-45669-4_4","volume-title":"Object Modeling with the OCL","author":"M. Richters","year":"2002","unstructured":"Richters, M., Gogolla, M.: OCL: Syntax, Semantics, and Tools. In: Clark, A., Warmer, J. (eds.) Object Modeling with the OCL. LNCS, vol.\u00a02263, pp. 42\u201368. Springer, Heidelberg (2002)"},{"key":"13_CR25","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10270-012-0261-0","volume":"11","author":"B. Selic","year":"2012","unstructured":"Selic, B.: What will it take? A view on adoption of model-based methods in practice. Software and Systems Modeling\u00a011, 513\u2013526 (2012)","journal-title":"Software and Systems Modeling"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-02674-4_14","volume-title":"Model Driven Architecture - Foundations and Applications","author":"M. Soden","year":"2009","unstructured":"Soden, M., Eichler, H.: Temporal Extensions of OCL Revisited. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol.\u00a05562, pp. 190\u2013205. Springer, Heidelberg (2009)"},{"key":"13_CR27","first-page":"1","volume-title":"Proceedings of the 1st Workshop on Behaviour Modelling in Model-Driven Architecture, Enschede, the Netherlands","author":"M. Soden","year":"2009","unstructured":"Soden, M., Eichler, H.: Towards a model execution framework for Eclipse. In: Proceedings of the 1st Workshop on Behaviour Modelling in Model-Driven Architecture, Enschede, the Netherlands, pp. 1\u20134. ACM Press, New York (2009)"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using Boolean satisfiability. In: Design, Automation and Test in Europe, pp. 1341\u20131344. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-39866-0_35","volume-title":"Perspectives of System Informatics","author":"P. Ziemann","year":"2004","unstructured":"Ziemann, P., Gogolla, M.: OCL Extended with Temporal Logic. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 351\u2013357. Springer, Heidelberg (2004)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-41533-3_19","volume-title":"Model-Driven Engineering Languages and Systems","author":"K. Zurowska","year":"2013","unstructured":"Zurowska, K., Dingel, J.: Model Checking of UML-RT Models Using Lazy Composition. In: Moreira, A., Sch\u00e4tz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol.\u00a08107, pp. 304\u2013319. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Software Language Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11245-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T16:12:15Z","timestamp":1558973535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11245-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319112442","9783319112459"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11245-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}