{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:49:44Z","timestamp":1764053384951,"version":"3.37.3"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,7,30]],"date-time":"2015-07-30T00:00:00Z","timestamp":1438214400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2017,5]]},"DOI":"10.1007\/s10270-015-0485-x","type":"journal-article","created":{"date-parts":[[2015,7,28]],"date-time":"2015-07-28T23:56:33Z","timestamp":1438127793000},"page":"357-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Formal validation of domain-specific languages with derived features and well-formedness constraints"],"prefix":"10.1007","volume":"16","author":[{"given":"Oszk\u00e1r","family":"Semer\u00e1th","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c1gnes","family":"Barta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c1kos","family":"Horv\u00e1th","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zolt\u00e1n","family":"Szatm\u00e1ri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8790-252X","authenticated-orcid":false,"given":"D\u00e1niel","family":"Varr\u00f3","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,30]]},"reference":[{"issue":"1","key":"485_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Softw. Syst. Model. 9(1), 69\u201386 (2010)","journal-title":"Softw. Syst. Model."},{"key":"485_CR2","doi-asserted-by":"publisher","unstructured":"Antkiewicz, M., Bak, K., Murashkin, A., Olaechea, R., Liang, J., Czarnecki, K.: Clafer tools for product line engineering. In: SPLC, Tokyo, Japan (2013)","DOI":"10.1145\/2499777.2499779"},{"key":"485_CR3","unstructured":"ARINC\u2014Aeronautical Radio, Incorporated: A653\u2014Avionics Application Software Standard Interface. http:\/\/www.aviation-ia.com\/standards"},{"key":"485_CR4","unstructured":"AUTOSAR Consortium: The AUTOSAR Standard (2013). http:\/\/www.autosar.org\/"},{"key":"485_CR5","doi-asserted-by":"publisher","unstructured":"Bak, K., Czarnecki, K., Wasowski, A.: Feature and meta-models in clafer: mixed, specialized, and coupled. In: 3rd International Conference on Software Language Engineering. Eindhoven, The Netherlands (2010). doi: 10.1007\/978-3-642-19440-5_7","DOI":"10.1007\/978-3-642-19440-5_7"},{"key":"485_CR6","unstructured":"Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: Proceedings of the VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark (2002)"},{"key":"485_CR7","doi-asserted-by":"publisher","unstructured":"Bergmann, G., Horv\u00e1th, \u00c1., R\u00e1th, I., Varr\u00f3, D., Balogh, A., Balogh, Z., \u00d6kr\u00f6s, A.: Incremental evaluation of model queries over EMF models. In: MODELS\u201910, LNCS, vol. 6395. Springer (2010)","DOI":"10.1007\/978-3-642-16145-2_6"},{"key":"485_CR8","doi-asserted-by":"publisher","unstructured":"Bergmann, G., Ujhelyi, Z., R\u00e1th, I., Varr\u00f3, D.: A graph query language for EMF models. In: Cabot, J., Visser, E. (eds.) Fourth International Conference on Theory and Practice of Model Transformations, LNCS, vol. 6707, pp. 167\u2013182. Springer (2011)","DOI":"10.1007\/978-3-642-21732-6_12"},{"key":"485_CR9","doi-asserted-by":"publisher","unstructured":"Bergmann, G.: Translating OCL to graph patterns. In: ACM\/IEEE 17th International Conference on Model Driven Engineering Languages and Systems, MODELS 2014. Springer, Valencia (2014)","DOI":"10.1007\/978-3-319-11653-2_41"},{"key":"485_CR10","unstructured":"Brucker, A.D., Wolff, B.: The HOL\u2013OCL tool (2007). http:\/\/www.brucker.ch\/"},{"key":"485_CR11","doi-asserted-by":"publisher","unstructured":"B\u00fcttner, F., Cabot, J.: Lightweight string reasoning for OCL. In: Vallecillo, A., Tolvanen, J.P., Kindler, E., St\u00f6rrle, H., Kolovos, D.S. (eds.) Modelling Foundations and Applications\u20148th European Conference, ECMFA 2012, Lyngby, Denmark, July 2\u20135, 2012. Proceedings, LNCS, vol. 7349, pp. 244\u2013258. Springer (2012)","DOI":"10.1007\/978-3-642-31491-9_19"},{"key":"485_CR12","doi-asserted-by":"publisher","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: 14th International Conference on Formal Engineering Methods, ICFEM\u201912, pp. 198\u2013213. LNCS 7635. Springer (2012)","DOI":"10.1007\/978-3-642-34281-3_16"},{"key":"485_CR13","doi-asserted-by":"publisher","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: Proceedings of the 15th International Conference on MODELS, LNCS, vol. 7590 (2012)","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"485_CR14","doi-asserted-by":"publisher","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML\/OCL models using constraint programming. In: Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201907), pp. 547\u2013548. ACM, New York (2007). doi: 10.1145\/1321631.1321737","DOI":"10.1145\/1321631.1321737"},{"key":"485_CR15","doi-asserted-by":"publisher","unstructured":"Cabot, J., Clariso, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: Software Testing Verification and Validation Workshop, 2008. ICSTW\u201908. IEEE International Conference on, pp. 73\u201380 (2008). doi: 10.1109\/ICSTW.2008.54","DOI":"10.1109\/ICSTW.2008.54"},{"issue":"3","key":"485_CR16","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10270-009-0129-0","volume":"9","author":"J Cabot","year":"2010","unstructured":"Cabot, J., Claris\u00f3, R., Guerra, E., de Lara, J.: A UML\/OCL framework for the analysis of graph transformation rules. Softw. Syst. Model. 9(3), 335\u2013357 (2010)","journal-title":"Softw. Syst. Model."},{"key":"485_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2014.03.023","volume":"93","author":"J Cabot","year":"2014","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: On the verification of UML\/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1\u201323 (2014)","journal-title":"J. Syst. Softw."},{"key":"485_CR18","unstructured":"Choco. http:\/\/www.emn.fr\/z-info\/choco-solverp"},{"key":"485_CR19","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24 (2009)"},{"key":"485_CR20","unstructured":"Clavel, M., Egea, M.: The ITP\/OCL tool (2008). http:\/\/maude.sip.ucm.es\/itp\/ocl\/"},{"key":"485_CR21","doi-asserted-by":"crossref","unstructured":"Cunha, A., Garis, A., Riesco, D.: Translating between alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 5\u201325 (2013)","DOI":"10.1007\/s10270-013-0353-5"},{"key":"485_CR22","unstructured":"Dania, C., Clavel, M.: OCL2FOL+: coping with undefinedness. In: Cabot, J., Gogolla, M., R\u00e1th, I., Willink, E.D. (eds.) OCL@MoDELS, CEUR Workshop Proceedings, vol. 1092, pp. 53\u201362. CEUR-WS.org (2013). http:\/\/dblp.uni-trier.de\/db\/conf\/models\/ocl2013.html#DaniaC13"},{"key":"485_CR23","doi-asserted-by":"publisher","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"485_CR24","doi-asserted-by":"publisher","unstructured":"Famelis, M., Salay, R., Chechik, M.: Partial models: towards modeling and reasoning with uncertainty. In: Proceedings of the 34th International Conference on Software Engineering, ICSE\u201912, pp. 573\u2013583. IEEE Press, Piscataway (2012). http:\/\/dl.acm.org\/citation.cfm?id=2337223.2337290","DOI":"10.1109\/ICSE.2012.6227159"},{"key":"485_CR25","doi-asserted-by":"publisher","unstructured":"Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, LNCS, vol. 5643, pp. 306\u2013320. Springer, Berlin (2009). doi: 10.1007\/978-3-642-02658-4_25","DOI":"10.1007\/978-3-642-02658-4_25"},{"issue":"4","key":"485_CR26","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s10270-005-0089-y","volume":"4","author":"M Gogolla","year":"2005","unstructured":"Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4(4), 386\u2013398 (2005)","journal-title":"Softw. Syst. Model."},{"key":"485_CR27","doi-asserted-by":"publisher","unstructured":"Gr\u00f6nniger, H., Ringert, J.O., Rumpe, B.: System model-based definition of modeling language semantics. In: Formal Techniques for Distributed Systems, LNCS, vol. 5522, pp. 152\u2013166. Springer (2009)","DOI":"10.1007\/978-3-642-02138-1_10"},{"key":"485_CR28","doi-asserted-by":"crossref","unstructured":"Horv\u00e1th, \u00c1., Heged\u00fcs, \u00c1., B\u00far, M., Varr\u00f3, D., Starr, R.R., Mirachi, S.: Hardware\u2013software allocation specification of ima systems for early simulation. In: Digital Avionics Systems Conference (DASC). IEEE, IEEE, Colorado Springs, Colorado, US (2014)","DOI":"10.1109\/DASC.2014.6979474"},{"key":"485_CR29","doi-asserted-by":"publisher","unstructured":"Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Proceedings of the 14th International Conference on MODELS, LNCS, vol. 6981, pp. 653\u2013667 (2011)","DOI":"10.1007\/978-3-642-24485-8_48"},{"key":"485_CR30","doi-asserted-by":"publisher","unstructured":"Jackson, E.K., Schulte, W., Bj\u00f8rner, N.: Detecting specification errors in declarative languages with constraints. In: Proceedings of the 15th International Conference on MODELS, LNCS, vol. 7590, pp. 399\u2013414 (2012)","DOI":"10.1007\/978-3-642-33666-9_26"},{"issue":"2","key":"485_CR31","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002). doi: 10.1145\/505145.505149","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"4","key":"485_CR32","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403\u2013434 (2004). doi: 10.1023\/B:AUSE.0000038938.10589.b9","journal-title":"Autom. Softw. Eng."},{"key":"485_CR33","doi-asserted-by":"publisher","unstructured":"Kuhlmann, M., Gogolla, M.: From UML and OCL to Relational Logic and Back. Lecture Notes in Computer Science, vol. 7590. Springer, Berlin (2012). doi: 10.1007\/978-3-642-33666-9_27","DOI":"10.1007\/978-3-642-33666-9_27"},{"key":"485_CR34","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Gogolla, M.: Strengthening SAT-based validation of UML\/OCL models by representing collections as relations. In: European Conference on Modelling Foundations and Applications, LNCS, vol. 7349, pp. 32\u201348 (2012)","DOI":"10.1007\/978-3-642-31491-9_5"},{"key":"485_CR35","doi-asserted-by":"publisher","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into use. In: TOOLS\u201911\u2014Objects, Models, Components and Patterns, LNCS, vol. 6705, pp. 290\u2013306 (2011)","DOI":"10.1007\/978-3-642-21952-8_21"},{"key":"485_CR36","unstructured":"Liang, J.: Solving Clafer Models with Choco (GSDLab-TR 2012-12-30) (2012)"},{"key":"485_CR37","doi-asserted-by":"publisher","unstructured":"Lucio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: Proceedings of the 13th International Conference on MODELS, LNCS, vol. 6394, pp. 136\u2013150 (2010)","DOI":"10.1007\/978-3-642-16145-2_10"},{"key":"485_CR38","unstructured":"Mathworks: Matlab Simulink\u2014Simulation and Model-Based Design. http:\/\/www.mathworks.com\/products\/simulink\/"},{"key":"485_CR39","unstructured":"Microsoft Research: Pex. http:\/\/research.microsoft.com\/projects\/pex\/"},{"key":"485_CR40","doi-asserted-by":"publisher","unstructured":"Micskei, Z., Szatm\u00e1ri, Z., Ol\u00e1h, J., Majzik, I.: A concept for testing robustness and safety of the context-aware behaviour of autonomous systems. In: Jezic, G., Kusek, M., Nguyen, N.T., Howlett, R., Jain, L. (eds.) Agent and Multi-Agent Systems. Technologies and Applications, LNCS, vol. 7327, pp. 504\u2013513. Springer, Berlin (2012). doi: 10.1007\/978-3-642-30947-2_55","DOI":"10.1007\/978-3-642-30947-2_55"},{"key":"485_CR41","doi-asserted-by":"crossref","unstructured":"Olaechea, R., Stewart, S., Czarnecki, K., Rayside, D.: Modeling and multi-objective optimization of quality attributes in variability-rich software. In: International Workshop on Non-functional System Properties in Domain Specific Modeling Languages. Innsbruck, Austria (2012)","DOI":"10.1145\/2420942.2420944"},{"key":"485_CR42","unstructured":"Oszk\u00e1r Semer\u00e1th: Validation of Domain Specific Languages. Technical Report (2013). https:\/\/incquery.net\/publications\/dslvalid"},{"key":"485_CR43","unstructured":"Piskac, R., de Moura, L., Bjorner, N.: Deciding effectively propositional logic with equality. Microsoft Research, MSR-TR-2008-181 Technical Report (2008)"},{"key":"485_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.datak.2011.09.004","volume":"73","author":"A Queralt","year":"2012","unstructured":"Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: finite reasoning on UML\/OCL conceptual schemas. Data Knowl. Eng. 73, 1\u201322 (2012)","journal-title":"Data Knowl. Eng."},{"key":"485_CR45","unstructured":"R3-cop (resilient reasoning robotic co-operative systems). ARTEMIS project no 100233. http:\/\/www.r3-cop.eu\/"},{"key":"485_CR46","doi-asserted-by":"publisher","unstructured":"R\u00e1th, I., Heged\u00fcs, A., Varr\u00f3, D.: Derived features for EMF by integrating advanced model queries. In: Vallecillo, A., Tolvanen, J.P., Kindler, E., St\u00f6rrle, H., Kolovos, D. (eds.) Modelling Foundations and Applications, LNCS, vol. 7349, pp. 102\u2013117. Springer, Berlin (2012). doi: 10.1007\/978-3-642-31491-9_10","DOI":"10.1007\/978-3-642-31491-9_10"},{"key":"485_CR47","unstructured":"RTCA, S.C.: DO-178C, Software Considerations in Airborne Systems and Equipment Certification (2011)"},{"key":"485_CR48","unstructured":"SAE\u2014Radio Technical Commission for Aeronautic: Architecture Analysis and Design Language (AADL) v2, AS-5506A, SAE International (2009)"},{"key":"485_CR49","doi-asserted-by":"publisher","unstructured":"Salay, R., Famelis, M., Chechik, M.: Language independent refinement using partial modeling. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 7212, pp. 224\u2013239. Springer, Berlin (2012). doi: 10.1007\/978-3-642-28872-2_16","DOI":"10.1007\/978-3-642-28872-2_16"},{"key":"485_CR50","unstructured":"Semer\u00e1th, O., Horv\u00e1th, \u00c1., Varr\u00f3, D.: Validation of derived features and well-formedness constraints in DSLs\u2014by mapping graph queries to an SMT-solver. In: MODELS\u2014Proceedings of 16th International Conference, MODELS 2013, Miami, FL, USA, September 29\u2013October 4, 2013, pp. 538\u2013554 (2013)"},{"key":"485_CR51","doi-asserted-by":"publisher","unstructured":"Sen, S., Mottu, J.M., Tisi, M., Cabot, J.: Using models of partial knowledge to test model transformations. In: 5th International Conference on Theory and Practice of Model Transformations, LNCS, vol. 7307, pp. 24\u201339 (2012)","DOI":"10.1007\/978-3-642-30476-7_2"},{"key":"485_CR52","doi-asserted-by":"publisher","unstructured":"Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and back again. In: MoDeVVa \u201909: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, pp. 1\u201310. ACM (2009)","DOI":"10.1145\/1656485.1656489"},{"key":"485_CR53","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\u201910), pp. 1341\u20131344. IEEE (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"485_CR54","unstructured":"The Eclipse Project: Eclipse Modeling Framework. http:\/\/www.eclipse.org\/emf"},{"key":"485_CR55","unstructured":"The Eclipse Project: Zest. http:\/\/www.eclipse.org\/gef\/zest\/"},{"key":"485_CR56","unstructured":"The Object Management Group: Object Constraint Language, v2.0 (2006). http:\/\/www.omg.org\/spec\/OCL\/2.0\/"},{"issue":"3","key":"485_CR57","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1016\/j.scico.2007.05.004","volume":"68","author":"D Varr\u00f3","year":"2007","unstructured":"Varr\u00f3, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68(3), 214\u2013234 (2007)","journal-title":"Sci. Comput. Program."},{"key":"485_CR58","doi-asserted-by":"publisher","unstructured":"Willink, E.D.: An extensible OCL virtual machine and code generator. In: Proceedings of the 12th Workshop on OCL and Textual Modelling, pp. 13\u201318. ACM (2012)","DOI":"10.1145\/2428516.2428519"},{"key":"485_CR59","doi-asserted-by":"publisher","unstructured":"Winkelmann, J., Taentzer, G., Ehrig, K., K\u00fcster, J.M.: Translation of restricted OCL constraints into graph constraints for generating meta model instances by graph grammars. ENTCS. In: Proceedings of the 5th International Workshop on Graph Transformation and Visual Modeling Techniques vol. 211, pp. 159\u2013170 (2008). doi: 10.1016\/j.entcs.2008.04.038","DOI":"10.1016\/j.entcs.2008.04.038"},{"key":"485_CR60","unstructured":"yEd Graph Editor: yED. http:\/\/www.yworks.com\/en\/products_yed_about.html"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0485-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-015-0485-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0485-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0485-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T16:57:12Z","timestamp":1567011432000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-015-0485-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,30]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["485"],"URL":"https:\/\/doi.org\/10.1007\/s10270-015-0485-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2015,7,30]]}}}