{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:28:46Z","timestamp":1742912926019,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319614816"},{"type":"electronic","value":"9783319614823"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-61482-3_14","type":"book-chapter","created":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T07:38:38Z","timestamp":1497857918000},"page":"232-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formulating Model Verification Tasks Prover-Independently as UML Diagrams"],"prefix":"10.1007","author":[{"given":"Martin","family":"Gogolla","sequence":"first","affiliation":[]},{"given":"Frank","family":"Hilken","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"Niemann","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Wille","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,20]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Model Driven Engineering Languages and Systems","author":"K Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436\u2013450. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-75209-7_30"},{"key":"14_CR2","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-319-29510-7_16","volume-title":"Formal Techniques for Safety-Critical Systems","author":"F Arshad","year":"2016","unstructured":"Arshad, F., Mehmood, H., Raza, F., Hasan, O.: g-HOL: a graphical user interface for the HOL proof assistant. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 265\u2013269. Springer, Cham (2016). doi:\n                      10.1007\/978-3-319-29510-7_16"},{"issue":"9","key":"14_CR3","doi-asserted-by":"publisher","first-page":"867","DOI":"10.1016\/j.compind.2012.06.002","volume":"63","author":"A Awad","year":"2012","unstructured":"Awad, A., Sakr, S.: On efficient processing of BPMN-Q queries. Comput. Ind. 63(9), 867\u2013881 (2012)","journal-title":"Comput. Ind."},{"issue":"4","key":"14_CR4","doi-asserted-by":"publisher","first-page":"1527","DOI":"10.1007\/s10270-013-0390-0","volume":"14","author":"M Balaban","year":"2015","unstructured":"Balaban, M., Maraee, A., Sturm, A., Jelnov, P.: A pattern-based approach for improving model quality. Softw. Syst. Model. 14(4), 1527\u20131555 (2015)","journal-title":"Softw. Syst. Model."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Ballis, D., Baruzzo, A., Comini, M.: A minimalist visual notation for design patterns and antipatterns. In: 5th International Conference on Information Technology: New Generations (ITNG 2008), pp. 51\u201356 (2008)","DOI":"10.1109\/ITNG.2008.227"},{"key":"14_CR6","unstructured":"Beckert, B., Grebing, S.: Evaluating the usability of interactive verification systems. In: Proceedings of 1st International Workshop Comparative Empirical Evaluation of Reasoning Systems, pp. 3\u201317 (2012)"},{"issue":"8","key":"14_CR7","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/j.infsof.2010.03.005","volume":"52","author":"P Bottoni","year":"2010","unstructured":"Bottoni, P., Guerra, E., de Lara, J.: A language-independent and formal approach to pattern-based modelling with support for composition and analysis. Inf. Softw. Technol. 52(8), 821\u2013844 (2010)","journal-title":"Inf. Softw. Technol."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-78743-3_8","volume-title":"Fundamental Approaches to Software Engineering","author":"AD Brucker","year":"2008","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: a formal proof environment for UML\/OCL. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97\u2013100. Springer, Heidelberg (2008). doi:\n                      10.1007\/978-3-540-78743-3_8"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: First International Conference on Software Testing Verification and Validation, ICST 2008, pp. 73\u201380. IEEE Computer Society (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1921532.1921561","volume":"36","author":"C Choppy","year":"2011","unstructured":"Choppy, C., Klai, K., Zidani, H.: Formal verification of UML state diagrams: a petri net based approach. Softw. Eng. Notes 36(1), 1\u20138 (2011)","journal-title":"Softw. Eng. Notes"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M Gogolla","year":"2007","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69, 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"key":"14_CR12","unstructured":"Gogolla, M., Hilken, F.: Model validation and verification options in a contemporary UML and OCL analysis tool. In: Oberweis, A., Reussner, R. (eds.) Proceedings of Modellierung (MODELLIERUNG 2016). LNI, GI, vol. 254, pp. 203\u2013218 (2016)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-02949-3_8","volume-title":"Tests and Proofs","author":"M Gogolla","year":"2009","unstructured":"Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL models. In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 90\u2013104. Springer, Heidelberg (2009). doi:\n                      10.1007\/978-3-642-02949-3_8"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-08789-4_13","volume-title":"Theory and Practice of Model Transformations","author":"F Hilken","year":"2014","unstructured":"Hilken, F., Hamann, L., Gogolla, M.: Transformation of UML and OCL models into filmstrip models. In: Ruscio, D., Varr\u00f3, D. (eds.) ICMT 2014. LNCS, vol. 8568, pp. 170\u2013185. Springer, Cham (2014). doi:\n                      10.1007\/978-3-319-08789-4_13"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-09099-3_8","volume-title":"Tests and Proofs","author":"F Hilken","year":"2014","unstructured":"Hilken, F., Niemann, P., Gogolla, M., Wille, R.: Filmstripping and unrolling: a comparison of verification approaches for UML and OCL behavioral models. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 99\u2013116. Springer, Cham (2014). doi:\n                      10.1007\/978-3-319-09099-3_8"},{"key":"14_CR16","unstructured":"Hilken, F., Niemann, P., Gogolla, M., Wille, R.: Towards a catalog of structural and behavioral verification tasks for UML\/OCL models. In: Oberweis, A., Reussner, R. (eds.) Proceedings of Modellierung (MODELLIERUNG 2016). LNI, GI, vol. 254, pp. 115\u2013122 (2016)"},{"key":"14_CR17","unstructured":"Homik, M., Meier, A.: Designing a GUI for proofs - evaluation of an HCI experiment. CoRR abs\/0903.3926 (2009)"},{"issue":"1","key":"14_CR18","first-page":"43","volume":"14","author":"VSW Lam","year":"2007","unstructured":"Lam, V.S.W.: A formalism for reasoning about UML activity diagrams. Nordic J. Comp. 14(1), 43\u201364 (2007)","journal-title":"Nordic J. Comp."},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2012.06.004","volume":"285","author":"A Lapets","year":"2012","unstructured":"Lapets, A., Kfoury, A.J.: A user-friendly interface for a lightweight verification system. Electr. Notes Theor. Comput. Sci. 285, 29\u201341 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"14_CR20","unstructured":"L\u00fcth, C.: User interfaces for theorem provers: necessary nuisance or unexplored potential? ECEASST 23 (2009). \n                      http:\/\/dblp.uni-trier.de\/db\/journals\/eceasst\/eceasst23.html"},{"key":"14_CR21","unstructured":"Moisuc, D., Revol, S., Snook, C.F.: UML user interface to a proof-based hardware design flow. In: Forum on Specification and Design Languages, FDL 2006, pp. 337\u2013344. ECSI (2006)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Pescador, A., Garmendia, A., Guerra, E., Cuadrado, J.S., de Lara, J.: Pattern-based development of domain-specific modelling languages. In: 18th ACM\/IEEE MoDELS 2015, pp. 166\u2013175 (2015)","DOI":"10.1109\/MODELS.2015.7338247"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-662-43613-4_2","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D Remenska","year":"2014","unstructured":"Remenska, D., Willemse, T.A.C., Templon, J., Verstoep, K., Bal, H.: Property specification made easy: harnessing the power of model checking in UML designs. In: \u00c1brah\u00e1m, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 17\u201332. Springer, Heidelberg (2014). doi:\n                      10.1007\/978-3-662-43613-4_2"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-662-46675-9_9","volume-title":"Fundamental Approaches to Software Engineering","author":"R Salay","year":"2015","unstructured":"Salay, R., Chechik, M.: A generalized formal framework for partial modeling. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 133\u2013148. Springer, Heidelberg (2015). doi:\n                      10.1007\/978-3-662-46675-9_9"},{"issue":"3","key":"14_CR25","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.5381\/jot.2015.14.3.a3","volume":"14","author":"R Salay","year":"2015","unstructured":"Salay, R., Chechik, M., Famelis, M., Gorzny, J.: A methodology for verifying refinements of partial models. J. Object Technol. 14(3), 3:1\u20133:31 (2015)","journal-title":"J. Object Technol."},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: Design, Automation and Test in Europe, DATE 2011, pp. 1077\u20131082. IEEE (2011)","DOI":"10.1109\/DATE.2011.5763177"},{"key":"14_CR27","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, DATE 2010, pp. 1341\u20131344. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-21470-7_6","volume-title":"Modelling Foundations and Applications","author":"R Straeten","year":"2011","unstructured":"Straeten, R., Pinna Puissant, J., Mens, T.: Assessing the Kodkod model finder for resolving model inconsistencies. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 69\u201384. Springer, Heidelberg (2011). doi:\n                      10.1007\/978-3-642-21470-7_6"},{"key":"14_CR29","unstructured":"Wang, X., Rutle, A., Lamo, Y.: Towards user-friendly and efficient analysis with alloy. In: Model-Driven Engineering, Verification and Validation, MoDeVVa@MoDELS 2015, pp. 28\u201337 (2015)"},{"issue":"5","key":"14_CR30","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/C-M.1981.220446","volume":"14","author":"MM Zloof","year":"1981","unstructured":"Zloof, M.M.: QBE\/OBE: a language for office and business automation. IEEE Comput. 14(5), 13\u201322 (1981)","journal-title":"IEEE Comput."}],"container-title":["Lecture Notes in Computer Science","Modelling Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-61482-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:30:48Z","timestamp":1558319448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-61482-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319614816","9783319614823"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-61482-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"20 June 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ECMFA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Conference on Modelling Foundations and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ecmdafa2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ecmfaconference.wixsite.com\/ecmfa2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}