var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Foszkarsemerath.github.io%2Fpublications.bib&jsonp=1&theme=side&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Foszkarsemerath.github.io%2Fpublications.bib&jsonp=1&theme=side\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Foszkarsemerath.github.io%2Fpublications.bib&jsonp=1&theme=side\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2024\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Requirement-Driven Generation of Distributed Ledger Architectures.\n \n \n \n \n\n\n \n Al-Gburi, N.; Földvári, A.; Marussy, K.; Semeráth, O.; and Kocsis, I.\n\n\n \n\n\n\n In MODELS '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, pages 268-279, 2024. \n \n\n\n\n
\n\n\n\n \n \n \"Requirement-DrivenPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:35437803,\n\ttitle = {Requirement-Driven Generation of Distributed Ledger Architectures},\n\turl = {https://m2.mtmt.hu/api/publication/35437803},\n\tauthor = {Al-Gburi, Noor and Földvári, András and Marussy, Kristóf and Semeráth, Oszkár and Kocsis, Imre},\n\tbooktitle = {MODELS '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems},\n\tdoi = {10.1145/3640310.3674097},\n\tunique-id = {35437803},\n\tyear = {2024},\n\tpages = {268-279},\n\torcid-numbers = {Al-Gburi, Noor/0000-0002-6542-5291; Földvári, András/0000-0002-4559-6990; Marussy, Kristóf/0000-0002-9135-8256}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search.\n \n \n \n \n\n\n \n Babikian, A. A.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 50: 48-68. 2024.\n \n\n\n\n
\n\n\n\n \n \n \"ConcretizationPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n 
@article{MTMT:34375495,\n\ttitle = {Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search},\n\turl = {https://m2.mtmt.hu/api/publication/34375495},\n\tauthor = {Babikian, Aren A. and Semeráth, Oszkár and Varró, Dániel},\n\tdoi = {10.1109/TSE.2023.3331254},\n\tjournal-iso = {IEEE T SOFTWARE ENG},\n\tjournal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING},\n\tvolume = {50},\n\tunique-id = {34375495},\n\tissn = {0098-5589},\n\tabstract = {Existing safety assurance approaches for autonomous vehicles (AVs) perform system-level safety evaluation by placing the AV-under-test in challenging traffic scenarios captured by abstract scenario specifications and investigated in realistic traffic simulators. As a first step towards scenario-based testing of AVs, the initial scene of a traffic scenario must be concretized. In this context, the scene concretization challenge takes as input a high-level specification of abstract traffic scenes and aims to map them to concrete scenes where exact numeric initial values are defined for each attribute of a vehicle (e.g. position or velocity). In this paper, we propose a traffic scene concretization approach that places vehicles on realistic road maps such that they satisfy an extensible set of abstract constraints defined by an expressive scene specification language which also supports static detection of inconsistencies. Then, abstract constraints are mapped to corresponding numeric constraints, which are solved by metaheuristic search with customizable objective functions and constraint aggregation strategies. We conduct a series of experiments over three realistic road maps to compare eight configurations of our approach with three variations of the state-of-the-art Scenic tool, and to evaluate its scalability.},\n\tkeywords = {Multiobjective optimization; evolutionary algorithm; Computer Science, Software Engineering; Scenario Description Language; Assurance for autonomous vehicles; traffic scene concretization},\n\tyear = {2024},\n\teissn = {1939-3520},\n\tpages = {48-68},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Existing safety assurance approaches for autonomous vehicles (AVs) perform system-level safety evaluation by placing the AV-under-test in challenging traffic scenarios captured by abstract scenario specifications and investigated in realistic traffic simulators. As a first step towards scenario-based testing of AVs, the initial scene of a traffic scenario must be concretized. In this context, the scene concretization challenge takes as input a high-level specification of abstract traffic scenes and aims to map them to concrete scenes where exact numeric initial values are defined for each attribute of a vehicle (e.g. position or velocity). In this paper, we propose a traffic scene concretization approach that places vehicles on realistic road maps such that they satisfy an extensible set of abstract constraints defined by an expressive scene specification language which also supports static detection of inconsistencies. Then, abstract constraints are mapped to corresponding numeric constraints, which are solved by metaheuristic search with customizable objective functions and constraint aggregation strategies. We conduct a series of experiments over three realistic road maps to compare eight configurations of our approach with three variations of the state-of-the-art Scenic tool, and to evaluate its scalability.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Refinery: Graph Solver as a Service: Refinement-based Generation and Analysis of Consistent Models.\n \n \n \n \n\n\n \n Marussy, K.; Ficsor, A.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n In ICSE-Companion '24: Proceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings, pages 64-68, 2024. \n \n\n\n\n
\n\n\n\n \n \n \"Refinery:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:34872599,\n\ttitle = {Refinery: Graph Solver as a Service: Refinement-based Generation and Analysis of Consistent Models},\n\turl = {https://m2.mtmt.hu/api/publication/34872599},\n\tauthor = {Marussy, Kristóf and Ficsor, Attila and Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {ICSE-Companion '24: Proceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings},\n\tdoi = {10.1145/3639478.3640045},\n\tunique-id = {34872599},\n\tabstract = {Various software and systems engineering scenarios rely on the systematic construction of consistent graph models. However, automatically generating a diverse set of consistent graph models for complex domain specifications is challenging. First, the graph generation problem must be specified with mathematical precision. Moreover, graph generation is a computationally complex task, which necessitates specialized logic solvers. Refinery is a novel open-source software framework to automatically synthesize a diverse set of consistent domain-specific graph models. The framework offers an expressive high-level specification language using partial models to succinctly formulate a wide range of graph generation challenges. Moreover, it provides a modern cloud-based architecture for a scalable graph solver as a service, which uses logic reasoning rules to efficiently synthesize a diverse set of solutions to graph generation problems by partial model refinement. Applications include system-level architecture synthesis, test generation for modeling tools or traffic scenario synthesis for autonomous vehicles. Video demonstration: https://youtu.be/Qy-3udNsWsM. Continuously deployed at: https://refinery.services/. © 2024 IEEE Computer Society. All rights reserved.},\n\tyear = {2024},\n\tpages = {64-68},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Ficsor, Attila/0000-0002-0541-4590; Semeráth, Oszkár/0000-0002-3592-5105; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Various software and systems engineering scenarios rely on the systematic construction of consistent graph models. However, automatically generating a diverse set of consistent graph models for complex domain specifications is challenging. First, the graph generation problem must be specified with mathematical precision. Moreover, graph generation is a computationally complex task, which necessitates specialized logic solvers. Refinery is a novel open-source software framework to automatically synthesize a diverse set of consistent domain-specific graph models. The framework offers an expressive high-level specification language using partial models to succinctly formulate a wide range of graph generation challenges. Moreover, it provides a modern cloud-based architecture for a scalable graph solver as a service, which uses logic reasoning rules to efficiently synthesize a diverse set of solutions to graph generation problems by partial model refinement. Applications include system-level architecture synthesis, test generation for modeling tools or traffic scenario synthesis for autonomous vehicles. Video demonstration: https://youtu.be/Qy-3udNsWsM. Continuously deployed at: https://refinery.services/. © 2024 IEEE Computer Society. All rights reserved.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Automated generation of consistent models using qualitative abstractions and exploration strategies.\n \n \n \n \n\n\n \n Babikian, A. A.; Semeráth, O.; Li, A.; Marussy, K.; and Varró, D.\n\n\n \n\n\n\n SOFTWARE AND SYSTEMS MODELING, 21: 1763-1787. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@article{MTMT:32394785,\n\ttitle = {Automated generation of consistent models using qualitative abstractions and exploration strategies},\n\turl = {https://m2.mtmt.hu/api/publication/32394785},\n\tauthor = {Babikian, Aren A. and Semeráth, Oszkár and Li, Anqi and Marussy, Kristóf and Varró, Dániel},\n\tdoi = {10.1007/s10270-021-00918-6},\n\tjournal-iso = {SOFTW SYST MODEL},\n\tjournal = {SOFTWARE AND SYSTEMS MODELING},\n\tvolume = {21},\n\tunique-id = {32394785},\n\tissn = {1619-1366},\n\tabstract = {Automatically synthesizing consistent models is a key prerequisite for many testing scenarios in autonomous driving to ensure a designated coverage of critical corner cases. An inconsistent model is irrelevant as a test case (e.g., false positive); thus, each synthetic model needs to simultaneously satisfy various structural and attribute constraints, which includes complex geometric constraints for traffic scenarios. While different logic solvers or dedicated graph solvers have recently been developed, they fail to handle either structural or attribute constraints in a scalable way. In the current paper, we combine a structural graph solver that uses partial models with an SMT-solver and a quadratic solver to automatically derive models which simultaneously fulfill structural and numeric constraints, while key theoretical properties of model generation like completeness or diversity are still ensured. This necessitates a sophisticated bidirectional interaction between different solvers which carry out consistency checks, decision, unit propagation, concretization steps. Additionally, we introduce custom exploration strategies to speed up model generation. We evaluate the scalability and diversity of our approach, as well as the influence of customizations, in the context of four complex case studies.},\n\tkeywords = {Model generation; Exploration strategy; Partial model; Graph solver; SMT-solver; Numeric solver; Test scenario synthesis},\n\tyear = {2022},\n\teissn = {1619-1374},\n\tpages = {1763-1787},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Automatically synthesizing consistent models is a key prerequisite for many testing scenarios in autonomous driving to ensure a designated coverage of critical corner cases. An inconsistent model is irrelevant as a test case (e.g., false positive); thus, each synthetic model needs to simultaneously satisfy various structural and attribute constraints, which includes complex geometric constraints for traffic scenarios. While different logic solvers or dedicated graph solvers have recently been developed, they fail to handle either structural or attribute constraints in a scalable way. In the current paper, we combine a structural graph solver that uses partial models with an SMT-solver and a quadratic solver to automatically derive models which simultaneously fulfill structural and numeric constraints, while key theoretical properties of model generation like completeness or diversity are still ensured. This necessitates a sophisticated bidirectional interaction between different solvers which carry out consistency checks, decision, unit propagation, concretization steps. Additionally, we introduce custom exploration strategies to speed up model generation. We evaluate the scalability and diversity of our approach, as well as the influence of customizations, in the context of four complex case studies.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Consistent Scene Graph Generation by Constraint Optimization.\n \n \n \n \n\n\n \n Chen, B.; Marussy, K.; Pilarski, S.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n In ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, pages 1-13, 2022. \n \n\n\n\n
\n\n\n\n \n \n \"ConsistentPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:33648748,\n\ttitle = {Consistent Scene Graph Generation by Constraint Optimization},\n\turl = {https://m2.mtmt.hu/api/publication/33648748},\n\tauthor = {Chen, Boqi and Marussy, Kristóf and Pilarski, Sebastian and Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering},\n\tdoi = {10.1145/3551349.3560433},\n\tunique-id = {33648748},\n\tyear = {2022},\n\tpages = {1-13},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Initial Performance Analysis of Graph Predicate Evaluation over Partial Models.\n \n \n \n \n\n\n \n Ficsor, A.; and Semeráth, O.\n\n\n \n\n\n\n In Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics, pages 1-4, 2022. \n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:33283704,\n\ttitle = {An Initial Performance Analysis of Graph Predicate Evaluation over Partial Models},\n\turl = {https://m2.mtmt.hu/api/publication/33283704},\n\tisbn = {9789634218722},\n\tauthor = {Ficsor, Attila and Semeráth, Oszkár},\n\tbooktitle = {Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics},\n\tdoi = {10.3311/MINISY2022-001},\n\tunique-id = {33283704},\n\tyear = {2022},\n\tpages = {1-4},\n\torcid-numbers = {Ficsor, Attila/0000-0002-0541-4590}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated Generation of Consistent Graph Models with Multiplicity Reasoning.\n \n \n \n \n\n\n \n Marussy, K.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 48: 1610-1629. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:31360895,\n\ttitle = {Automated Generation of Consistent Graph Models with Multiplicity Reasoning},\n\turl = {https://m2.mtmt.hu/api/publication/31360895},\n\tauthor = {Marussy, Kristóf and Semeráth, Oszkár and Varró, Dániel},\n\tdoi = {10.1109/TSE.2020.3025732},\n\tjournal-iso = {IEEE T SOFTWARE ENG},\n\tjournal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING},\n\tvolume = {48},\n\tunique-id = {31360895},\n\tissn = {0098-5589},\n\tabstract = {Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph models is necessitated which is often carried out by solver-based model generation techniques. In many model generation scenarios, one needs more refined control over the generated unit tests to focus on the more relevant models. Type scopes allow to precisely define the required number of newly generated elements, thus one can avoid the generation of unrealistic and highly symmetric models having only a single type of elements. In this paper, we propose a 3-valued scoped partial modeling formalism, which innovatively extends partial graph models with predicate abstraction and counter abstraction. As a result, well-formedness constraints and multiplicity requirements can be evaluated in an approximated way on incomplete (unfinished) models by using advanced graph query engines with numerical solvers (e.g., IP or LP solvers). Based on the refinement of 3-valued scoped partial models, we propose an efficient model generation algorithm that generates models that are both well-formed and satisfy the scope requirements. We show that the proposed approach scales significantly better than existing SAT-solver techniques or the original graph solver without multiplicity reasoning. We illustrate our approach in a complex design-space exploration case study of collaborating satellites introduced by researchers at NASA JPL.},\n\tyear = {2022},\n\teissn = {1939-3520},\n\tpages = {1610-1629},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph models is necessitated which is often carried out by solver-based model generation techniques. In many model generation scenarios, one needs more refined control over the generated unit tests to focus on the more relevant models. Type scopes allow to precisely define the required number of newly generated elements, thus one can avoid the generation of unrealistic and highly symmetric models having only a single type of elements. In this paper, we propose a 3-valued scoped partial modeling formalism, which innovatively extends partial graph models with predicate abstraction and counter abstraction. As a result, well-formedness constraints and multiplicity requirements can be evaluated in an approximated way on incomplete (unfinished) models by using advanced graph query engines with numerical solvers (e.g., IP or LP solvers). Based on the refinement of 3-valued scoped partial models, we propose an efficient model generation algorithm that generates models that are both well-formed and satisfy the scope requirements. We show that the proposed approach scales significantly better than existing SAT-solver techniques or the original graph solver without multiplicity reasoning. We illustrate our approach in a complex design-space exploration case study of collaborating satellites introduced by researchers at NASA JPL.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Towards the Formal Semantics of Scenario Tests for Autonomous Vehicles.\n \n \n \n \n\n\n \n Kovacs, L.; and Semeráth, O.\n\n\n \n\n\n\n In 2021 10th Latin-American Symposium on Dependable Computing (LADC), pages 01-04, 2021. \n \n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:32605462,\n\ttitle = {Towards the Formal Semantics of Scenario Tests for Autonomous Vehicles},\n\turl = {https://m2.mtmt.hu/api/publication/32605462},\n\tauthor = {Kovacs, Laszlo and Semeráth, Oszkár},\n\tbooktitle = {2021 10th Latin-American Symposium on Dependable Computing (LADC)},\n\tdoi = {10.1109/LADC53747.2021.9672554},\n\tunique-id = {32605462},\n\tyear = {2021},\n\tpages = {01-04}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models.\n \n \n \n \n\n\n \n Semeráth, O.; Aren, A. B.; Boqi, C.; Chuning, L.; Marussy, K.; Szárnyas, G.; and Varró, D.\n\n\n \n\n\n\n SOFTWARE AND SYSTEMS MODELING, 20: 1713-1734. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:32028274,\n\ttitle = {Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models},\n\turl = {https://m2.mtmt.hu/api/publication/32028274},\n\tauthor = {Semeráth, Oszkár and Aren, A. Babikian and Boqi, Chen and Chuning, Li and Marussy, Kristóf and Szárnyas, Gábor and Varró, Dániel},\n\tdoi = {10.1007/s10270-021-00884-z},\n\tjournal-iso = {SOFTW SYST MODEL},\n\tjournal = {SOFTWARE AND SYSTEMS MODELING},\n\tvolume = {20},\n\tunique-id = {32028274},\n\tissn = {1619-1366},\n\tabstract = {In this paper, we present a novel technique to automatically synthesize consistent, diverse and structurally realistic domain-specific graph models. A graph model is (1) consistent if it is metamodel-compliant and it satisfies the well-formedness constraints of the domain; (2) it is diverse if local neighborhoods of nodes are highly different; and (1) it is structurally realistic if a synthetic graph is at a close distance to a representative real model according to various graph metrics used in network science, databases or software engineering. Our approach grows models by model extension operators using a hill-climbing strategy in a way that (A) ensures that there are no constraint violation in the models (for consistency reasons), while (B) more realistic candidates are selected to minimize a target metric value (wrt. the representative real model). We evaluate the effectiveness of the approach for generating realistic models using multiple metrics for guidance heuristics and compared to other model generators in the context of three case studies with a large set of real human models. We also highlight that our technique is able to generate a diverse set of models, which is a requirement in many testing scenarios.},\n\tyear = {2021},\n\teissn = {1619-1374},\n\tpages = {1713-1734},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n In this paper, we present a novel technique to automatically synthesize consistent, diverse and structurally realistic domain-specific graph models. A graph model is (1) consistent if it is metamodel-compliant and it satisfies the well-formedness constraints of the domain; (2) it is diverse if local neighborhoods of nodes are highly different; and (1) it is structurally realistic if a synthetic graph is at a close distance to a representative real model according to various graph metrics used in network science, databases or software engineering. Our approach grows models by model extension operators using a hill-climbing strategy in a way that (A) ensures that there are no constraint violation in the models (for consistency reasons), while (B) more realistic candidates are selected to minimize a target metric value (wrt. the representative real model). We evaluate the effectiveness of the approach for generating realistic models using multiple metrics for guidance heuristics and compared to other model generators in the context of three case studies with a large set of real human models. We also highlight that our technique is able to generate a diverse set of models, which is a requirement in many testing scenarios.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers.\n \n \n \n \n\n\n \n Aren, B.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n In Fundamental Approaches to Software Engineering, pages 441-461, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:31160534,\n\ttitle = {Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers},\n\turl = {https://m2.mtmt.hu/api/publication/31160534},\n\tauthor = {Aren, Babikian and Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {Fundamental Approaches to Software Engineering},\n\tdoi = {10.1007/978-3-030-45234-6_22},\n\tunique-id = {31160534},\n\tyear = {2020},\n\tpages = {441-461},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated video game world map synthesis by model-based techniques.\n \n \n \n \n\n\n \n Chen, B.; Havelock, D.; Plante, C.; Sukkarieh, M.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n In MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:31872191,\n\ttitle = {Automated video game world map synthesis by model-based techniques},\n\turl = {https://m2.mtmt.hu/api/publication/31872191},\n\tauthor = {Chen, Boqi and Havelock, Dylan and Plante, Connor and Sukkarieh, Michael and Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings},\n\tdoi = {10.1145/3417990.3422001},\n\tunique-id = {31872191},\n\tyear = {2020},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A specification language for consistent model generation based on partial models.\n \n \n \n \n\n\n \n Marussy, K.; Semeráth, O.; Aren, A. B.; and Varró, D.\n\n\n \n\n\n\n JOURNAL OF OBJECT TECHNOLOGY, 19. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:31361799,\n\ttitle = {A specification language for consistent model generation based on partial models},\n\turl = {https://m2.mtmt.hu/api/publication/31361799},\n\tauthor = {Marussy, Kristóf and Semeráth, Oszkár and Aren, A. Babikian and Varró, Dániel},\n\tdoi = {10.5381/jot.2020.19.3.a12},\n\tjournal-iso = {J OBJECT TECHNOL},\n\tjournal = {JOURNAL OF OBJECT TECHNOLOGY},\n\tvolume = {19},\n\tunique-id = {31361799},\n\tissn = {1660-1769},\n\tyear = {2020},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Diversity of Graph Models and Graph Generators in Mutation Testing.\n \n \n \n \n\n\n \n Semeráth, O.; Farkas, R.; Bergmann, G.; and Varró, D.\n\n\n \n\n\n\n INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 22: 57-78. 2020.\n \n\n\n\n
\n\n\n\n \n \n \"DiversityPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:30748493,\n\ttitle = {Diversity of Graph Models and Graph Generators in Mutation Testing},\n\turl = {https://m2.mtmt.hu/api/publication/30748493},\n\tauthor = {Semeráth, Oszkár and Farkas, Rebeka and Bergmann, Gábor and Varró, Dániel},\n\tdoi = {10.1007/s10009-019-00530-6},\n\tjournal-iso = {INT J SOFTW TOOLS TECHNOL TRANSF},\n\tjournal = {INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER},\n\tvolume = {22},\n\tunique-id = {30748493},\n\tissn = {1433-2779},\n\tyear = {2020},\n\teissn = {1433-2787},\n\tpages = {57-78},\n\torcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated generation of consistent models with structural and attribute constraints.\n \n \n \n \n\n\n \n Semeráth, O.; Babikian, A. A.; Li, A.; Marussy, K.; and Varró, D.\n\n\n \n\n\n\n In MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pages 187-199, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:31872205,\n\ttitle = {Automated generation of consistent models with structural and attribute constraints},\n\turl = {https://m2.mtmt.hu/api/publication/31872205},\n\tauthor = {Semeráth, Oszkár and Babikian, Aren A. and Li, Anqi and Marussy, Kristóf and Varró, Dániel},\n\tbooktitle = {MODELS '20: Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems},\n\tdoi = {10.1145/3365438.3410962},\n\tunique-id = {31872205},\n\tyear = {2020},\n\tpages = {187-199},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Towards System-Level Testing with Coverage Guarantees for Autonomous Vehicles.\n \n \n \n \n\n\n \n Majzik, I.; Semeráth, O.; Hajdu, C.; Marussy, K.; Szatmári, Z.; Micskei, Z. I.; Vörös, A.; Aren, A. B.; and Varró, D.\n\n\n \n\n\n\n In 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems (MODELS), pages 89-94, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:30748490,\n\ttitle = {Towards System-Level Testing with Coverage Guarantees for Autonomous Vehicles},\n\turl = {https://m2.mtmt.hu/api/publication/30748490},\n\tauthor = {Majzik, István and Semeráth, Oszkár and Hajdu, Csaba and Marussy, Kristóf and Szatmári, Zoltán and Micskei, Zoltán Imre and Vörös, András and Aren, A. Babikian and Varró, Dániel},\n\tbooktitle = {2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems (MODELS)},\n\tdoi = {10.1109/MODELS.2019.00-12},\n\tunique-id = {30748490},\n\tyear = {2019},\n\tpages = {89-94},\n\torcid-numbers = {Hajdu, Csaba/0000-0002-1058-7525; Marussy, Kristóf/0000-0002-9135-8256; Micskei, Zoltán Imre/0000-0003-1846-261X; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal validation and model generation for domain-specific languages by logic solvers.\n \n \n \n \n\n\n \n Semeráth, O.\n\n\n \n\n\n\n Master's thesis, 2019.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@mastersthesis{MTMT:31347768,\n\ttitle = {Formal validation and model generation for domain-specific languages by logic solvers},\n\turl = {https://m2.mtmt.hu/api/publication/31347768},\n\tauthor = {Semeráth, Oszkár},\n\tpublisher = {Budapest University of Technology and Economics},\n\tunique-id = {31347768},\n\tyear = {2019}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Viatra Solver: A Framework for the Automated Generation of Consistent Domain-Specific Models.\n \n \n \n \n\n\n \n Semeráth, O.; A Babikian, A.; Pilarski, S.; and Varró, D.\n\n\n \n\n\n\n In 2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pages 43-46, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"ViatraPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:30748475,\n\ttitle = {Viatra Solver: A Framework for the Automated Generation of Consistent Domain-Specific Models},\n\turl = {https://m2.mtmt.hu/api/publication/30748475},\n\tauthor = {Semeráth, Oszkár and A Babikian, Aren and Pilarski, Sebastian and Varró, Dániel},\n\tbooktitle = {2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)},\n\tdoi = {10.1109/ICSE-Companion.2019.00034},\n\tunique-id = {30748475},\n\tabstract = {VIATRA Solver [1] is a novel open source software tool to automatically synthesize consistent and diverse domain-specific graph models to be used as a test suite for the systematic testing of CPS modelling tools. Taking a metamodel, and a set of well-formedness constraints of a domain as input, the solver derives a diverse set of consistent graph models where each graph is compliant with the metamodel, satisfies consistency constraints, and structurally different from each other. The tool is integrated into the Eclipse IDE or it is executable from the command line.},\n\tyear = {2019},\n\tpages = {43-46},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n VIATRA Solver [1] is a novel open source software tool to automatically synthesize consistent and diverse domain-specific graph models to be used as a test suite for the systematic testing of CPS modelling tools. Taking a metamodel, and a set of well-formedness constraints of a domain as input, the solver derives a diverse set of consistent graph models where each graph is compliant with the metamodel, satisfies consistency constraints, and structurally different from each other. The tool is integrated into the Eclipse IDE or it is executable from the command line.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Towards the Automated Generation of Consistent, Diverse, Scalable and Realistic Graph Models.\n \n \n \n \n\n\n \n Varró, D.; Semeráth, O.; Szárnyas, G.; and Horváth, Á.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 10800: 285-312. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"TowardsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3327320,\n\ttitle = {Towards the Automated Generation of Consistent, Diverse, Scalable and Realistic Graph Models},\n\turl = {https://m2.mtmt.hu/api/publication/3327320},\n\tauthor = {Varró, Dániel and Semeráth, Oszkár and Szárnyas, Gábor and Horváth, Ákos},\n\tdoi = {10.1007/978-3-319-75396-6_16},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {10800},\n\tunique-id = {3327320},\n\tissn = {0302-9743},\n\tyear = {2018},\n\teissn = {1611-3349},\n\tpages = {285-312},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Incremental View Model Synchronization Using Partial Models.\n \n \n \n \n\n\n \n Marussy, K.; Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n In MODELS '18: Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pages 323-333, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"IncrementalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:3398313,\n\ttitle = {Incremental View Model Synchronization Using Partial Models},\n\turl = {https://m2.mtmt.hu/api/publication/3398313},\n\tauthor = {Marussy, Kristóf and Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {MODELS '18: Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems},\n\tdoi = {10.1145/3239372.3239412},\n\tunique-id = {3398313},\n\tyear = {2018},\n\tpages = {323-333},\n\torcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Iterative Generation of Diverse Models for Testing Specifications of DSL Tools.\n \n \n \n \n\n\n \n Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 10802: 227-245. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"IterativePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3335171,\n\ttitle = {Iterative Generation of Diverse Models for Testing Specifications of DSL Tools},\n\turl = {https://m2.mtmt.hu/api/publication/3335171},\n\tauthor = {Semeráth, Oszkár and Varró, Dániel},\n\tdoi = {10.1007/978-3-319-89363-1_13},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {10802},\n\tunique-id = {3335171},\n\tissn = {0302-9743},\n\tyear = {2018},\n\teissn = {1611-3349},\n\tpages = {227-245},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Graph Solver for the Automated Generation of Consistent Domain-Specific Models.\n \n \n \n \n\n\n \n Semeráth, O.; Nagy, A. S.; and Varró, D.\n\n\n \n\n\n\n In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE '18), pages 969-980, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:3335161,\n\ttitle = {A Graph Solver for the Automated Generation of Consistent Domain-Specific Models},\n\turl = {https://m2.mtmt.hu/api/publication/3335161},\n\tauthor = {Semeráth, Oszkár and Nagy, András Szabolcs and Varró, Dániel},\n\tbooktitle = {2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE '18)},\n\tdoi = {10.1145/3180155.3180186},\n\tunique-id = {3335161},\n\tyear = {2018},\n\tpages = {969-980},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Evaluating Well-Formedness Constraints on Incomplete Models.\n \n \n \n \n\n\n \n Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n ACTA CYBERNETICA, 23: 687-713. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"EvaluatingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3229152,\n\ttitle = {Evaluating Well-Formedness Constraints on Incomplete Models},\n\turl = {https://m2.mtmt.hu/api/publication/3229152},\n\tauthor = {Semeráth, Oszkár and Varró, Dániel},\n\tdoi = {10.14232/actacyb.23.2.2017.15},\n\tjournal-iso = {ACTA CYBERN-SZEGED},\n\tjournal = {ACTA CYBERNETICA},\n\tvolume = {23},\n\tunique-id = {3229152},\n\tissn = {0324-721X},\n\tabstract = {In modern modeling tools used for model-driven development, the valida- tion of several well-formedness constraints is continuously been carried out by exploiting advanced graph query engines to highlight conceptual design aws. However, while models are still under development, they are frequently par- tial and incomplete. Validating constraints on incomplete, partial models may identify a large number of irrelevant problems. By switching o the val- idation of these constraints, one may fail to reveal problematic cases which are dicult to correct when the model becomes suciently detailed. Here, we propose a novel validation technique for evaluating well-formed- ness constraints on incomplete, partial models with may and must semantics, e.g. a constraint without a valid match is satisable if there is a completion of the partial model that may satisfy it. To this end, we map the problem of constraint evaluation over partial models into regular graph pattern matching over complete models by semantically equivalent rewrites of graph queries.},\n\tyear = {2017},\n\teissn = {2676-993X},\n\tpages = {687-713},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n In modern modeling tools used for model-driven development, the valida- tion of several well-formedness constraints is continuously been carried out by exploiting advanced graph query engines to highlight conceptual design aws. However, while models are still under development, they are frequently par- tial and incomplete. Validating constraints on incomplete, partial models may identify a large number of irrelevant problems. By switching o the val- idation of these constraints, one may fail to reveal problematic cases which are dicult to correct when the model becomes suciently detailed. Here, we propose a novel validation technique for evaluating well-formed- ness constraints on incomplete, partial models with may and must semantics, e.g. a constraint without a valid match is satisable if there is a completion of the partial model that may satisfy it. To this end, we map the problem of constraint evaluation over partial models into regular graph pattern matching over complete models by semantically equivalent rewrites of graph queries.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal validation of domain-specific languages with derived features and well-formedness constraints.\n \n \n \n \n\n\n \n Semeráth, O.; Ágnes, B.; Horváth, Á.; Szatmári, Z.; and Varró, D.\n\n\n \n\n\n\n SOFTWARE AND SYSTEMS MODELING, 16: 357-392. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3018014,\n\ttitle = {Formal validation of domain-specific languages with derived features and well-formedness constraints},\n\turl = {https://m2.mtmt.hu/api/publication/3018014},\n\tauthor = {Semeráth, Oszkár and Ágnes, Barta and Horváth, Ákos and Szatmári, Zoltán and Varró, Dániel},\n\tdoi = {10.1007/s10270-015-0485-x},\n\tjournal-iso = {SOFTW SYST MODEL},\n\tjournal = {SOFTWARE AND SYSTEMS MODELING},\n\tvolume = {16},\n\tunique-id = {3018014},\n\tissn = {1619-1366},\n\tabstract = {Despite the wide range of existing tool support, constructing \n\t\ta design environment for a complex domain-specific language \n\t\t(DSL) is still a tedious task as the large number of derived \n\t\tfeatures and well-formedness constraints complementing the \n\t\tdomain metamodel necessitate special handling. Such derived \n\t\tfeatures and constraints are frequently defined by \n\t\tdeclarative techniques (such graph patterns or OCL \n\t\tinvariants). However, for complex domains, derived features \n\t\tand constraints can easily be formalized incorrectly \n\t\tresulting in inconsistent, incomplete or ambiguous DSL \n\t\tspecifications. To detect such issues, we propose an \n\t\tautomated mapping of EMF metamodels enriched with derived \n\t\tfeatures and well-formedness constraints captured as graph \n\t\tqueries in EMF-IncQuery or (a subset of) OCL invariants into \n\t\tan effectively propositional fragment of first-order logic \n\t\twhich can be efficiently analyzed by back-end reasoners. On \n\t\tthe conceptual level, the main added value of our encoding is \n\t\t(1) to transform graph patterns of the EMF-IncQuery framework \n\t\tinto FOL and (2) to introduce approximations for complex \n\t\tlanguage features (e.g., transitive closure or \n\t\tmultiplicities) which are not expressible in FOL. On the \n\t\tpractical level, we identify and address relevant challenges \n\t\tand scenarios for systematically validating DSL \n\t\tspecifications. Our approach is supported by a tool, and it \n\t\twill be illustrated on analyzing a DSL in the avionics \n\t\tdomain. We also present initial performance experiments for \n\t\tthe validation using Z3 and Alloy as back-end reasoners.},\n\tyear = {2017},\n\teissn = {1619-1374},\n\tpages = {357-392},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Despite the wide range of existing tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous DSL specifications. To detect such issues, we propose an automated mapping of EMF metamodels enriched with derived features and well-formedness constraints captured as graph queries in EMF-IncQuery or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Graph constraint evaluation over partial models by constraint rewriting.\n \n \n \n \n\n\n \n Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 10374: 138-154. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"GraphPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n 
@article{MTMT:3277444,\n\ttitle = {Graph constraint evaluation over partial models by constraint rewriting},\n\turl = {https://m2.mtmt.hu/api/publication/3277444},\n\tauthor = {Semeráth, Oszkár and Varró, Dániel},\n\tdoi = {10.1007/978-3-319-61473-1_10},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {10374},\n\tunique-id = {3277444},\n\tissn = {0302-9743},\n\tabstract = {In the early stages of model driven development, models are frequently incomplete and partial. Partial models represent multiple possible concrete models, and thus, they are able to capture uncertainty and possible design decisions. When using models of a complex modeling language, several well-formedness constraints need to be continuously checked to highlight conceptual design flaws for the engineers in an early phase. While well-formedness constraints can be efficiently checked for (fully specified) concrete models, checking the same constraints over partial models is more challenging since, for instance, a currently valid constraint may be violated (or an invalid constraint may be respected) when refining a partial model into a concrete model. In this paper we propose a novel technique to evaluate well-formedness constraints on partial models in order to detect if (i) a concretization may potentially violate or (ii) any concretization will surely violate a well-formedness constraint to help engineers gradually to resolve uncertainty without violating well-formedness. For that purpose, we map the problem of constraint evaluation over partial models into a regular graph pattern matching problem over complete models by semantically equivalent rewrites of graph queries.},\n\tkeywords = {Computer Science, Software Engineering},\n\tyear = {2017},\n\teissn = {1611-3349},\n\tpages = {138-154},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n In the early stages of model driven development, models are frequently incomplete and partial. Partial models represent multiple possible concrete models, and thus, they are able to capture uncertainty and possible design decisions. When using models of a complex modeling language, several well-formedness constraints need to be continuously checked to highlight conceptual design flaws for the engineers in an early phase. While well-formedness constraints can be efficiently checked for (fully specified) concrete models, checking the same constraints over partial models is more challenging since, for instance, a currently valid constraint may be violated (or an invalid constraint may be respected) when refining a partial model into a concrete model. In this paper we propose a novel technique to evaluate well-formedness constraints on partial models in order to detect if (i) a concretization may potentially violate or (ii) any concretization will surely violate a well-formedness constraint to help engineers gradually to resolve uncertainty without violating well-formedness. For that purpose, we map the problem of constraint evaluation over partial models into a regular graph pattern matching problem over complete models by semantically equivalent rewrites of graph queries.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Validation of Well-formedness Constraints on Uncertain Models.\n \n \n \n \n\n\n \n Semeráth, O.; and Varró, D.\n\n\n \n\n\n\n 2016.\n \n\n\n\n
\n\n\n\n \n \n \"ValidationPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@CONFERENCE{MTMT:3172186,\n\ttitle = {Validation of Well-formedness Constraints on Uncertain Models},\n\turl = {https://m2.mtmt.hu/api/publication/3172186},\n\tauthor = {Semeráth, Oszkár and Varró, Dániel},\n\tbooktitle = {The 10th Jubilee Conference of PhD Students in Computer Science},\n\tunique-id = {3172186},\n\tyear = {2016},\n\tpages = {57-57},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Incremental Backward Change Propagation of View Models by Logic Solvers.\n \n \n \n \n\n\n \n Semeráth, O.; Debreceni, C.; Horváth, Á.; and Varró, D.\n\n\n \n\n\n\n In MODELS '16, pages 306-316, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"IncrementalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MTMT:3169820,\n\ttitle = {Incremental Backward Change Propagation of View Models by Logic Solvers},\n\turl = {https://m2.mtmt.hu/api/publication/3169820},\n\tauthor = {Semeráth, Oszkár and Debreceni, Csaba and Horváth, Ákos and Varró, Dániel},\n\tbooktitle = {MODELS '16},\n\tdoi = {10.1145/2976767.2976788},\n\tunique-id = {3169820},\n\tabstract = {View models are key concepts of domain-specific modeling\n\t\tto provide task-specific focus (e.g., power or communication\n\t\tarchitecture of a system) to the designers by highlighting\n\t\tonly the relevant aspects of the system. View models\n\t\tcan be specified by unidirectional forward transformations\n\t\t(frequently captured by graph queries), and automatically\n\t\tmaintained upon changes of the underlying source model using\n\t\tincremental transformation techniques. However, tracing\n\t\tback complex changes from one or more abstract view\n\t\tto the underlying source model is a challenging task, which,\n\t\tin general, requires the simultaneous analysis of \n\t\ttransformation\n\t\tspecifications and well-formedness constraints to create\n\t\tvalid changes in the source model. In this paper we introduce\n\t\ta novel delta-based backward transformation technique\n\t\tusing SAT solvers to synthetize valid and consistent change\n\t\tcandidates in the source model, where only forward \n\t\ttransformation rules are specified for the view models.},\n\tyear = {2016},\n\tpages = {306-316},\n\torcid-numbers = {Debreceni, Csaba/0000-0002-6263-7758; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n View models are key concepts of domain-specific modeling to provide task-specific focus (e.g., power or communication architecture of a system) to the designers by highlighting only the relevant aspects of the system. View models can be specified by unidirectional forward transformations (frequently captured by graph queries), and automatically maintained upon changes of the underlying source model using incremental transformation techniques. However, tracing back complex changes from one or more abstract view to the underlying source model is a challenging task, which, in general, requires the simultaneous analysis of transformation specifications and well-formedness constraints to create valid changes in the source model. In this paper we introduce a novel delta-based backward transformation technique using SAT solvers to synthetize valid and consistent change candidates in the source model, where only forward transformation rules are specified for the view models.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Validation and Model Synthesis for Domain-specific Languages by Logic Solvers.\n \n \n \n \n\n\n \n Semeráth, O.\n\n\n \n\n\n\n 2016.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@CONFERENCE{MTMT:3169934,\n\ttitle = {Formal Validation and Model Synthesis for Domain-specific Languages by Logic Solvers},\n\turl = {https://m2.mtmt.hu/api/publication/3169934},\n\tauthor = {Semeráth, Oszkár},\n\tbooktitle = {ACM Student Research Competition at MODELS 2016},\n\tunique-id = {3169934},\n\tyear = {2016}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Change Propagation of View Models by Logic Synthesis using SAT solvers.\n \n \n \n \n\n\n \n Semeráth, O.; Debreceni, C.; Horváth, Á.; and Varró, D.\n\n\n \n\n\n\n CEUR WORKSHOP PROCEEDINGS, 1571: 40-44. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"ChangePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3092093,\n\ttitle = {Change Propagation of View Models by Logic Synthesis using SAT solvers},\n\turl = {https://m2.mtmt.hu/api/publication/3092093},\n\tauthor = {Semeráth, Oszkár and Debreceni, Csaba and Horváth, Ákos and Varró, Dániel},\n\tjournal-iso = {CEUR WORKSHOP PROC},\n\tjournal = {CEUR WORKSHOP PROCEEDINGS},\n\tvolume = {1571},\n\tunique-id = {3092093},\n\tyear = {2016},\n\teissn = {1613-0073},\n\tpages = {40-44},\n\torcid-numbers = {Debreceni, Csaba/0000-0002-6263-7758; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Iterative and incremental model generation by logic solvers.\n \n \n \n \n\n\n \n Semeráth, O.; Vörös, A.; and Varró, D.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 9633: 87-103. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"IterativePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3018468,\n\ttitle = {Iterative and incremental model generation by logic solvers},\n\turl = {https://m2.mtmt.hu/api/publication/3018468},\n\tauthor = {Semeráth, Oszkár and Vörös, András and Varró, Dániel},\n\tdoi = {10.1007/978-3-662-49665-7_6},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {9633},\n\tunique-id = {3018468},\n\tissn = {0302-9743},\n\tyear = {2016},\n\teissn = {1611-3349},\n\tpages = {87-103},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The TTC 2015 Train Benchmark Case for Incremental Model Validation.\n \n \n \n \n\n\n \n Szárnyas, G.; Semeráth, O.; Ráth, I. Z.; and Varró, D.\n\n\n \n\n\n\n CEUR WORKSHOP PROCEEDINGS, 1524: 129-141. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{MTMT:3017909,\n\ttitle = {The TTC 2015 Train Benchmark Case for Incremental Model Validation},\n\turl = {https://m2.mtmt.hu/api/publication/3017909},\n\tauthor = {Szárnyas, Gábor and Semeráth, Oszkár and Ráth, István Zoltán and Varró, Dániel},\n\tjournal-iso = {CEUR WORKSHOP PROC},\n\tjournal = {CEUR WORKSHOP PROCEEDINGS},\n\tvolume = {1524},\n\tunique-id = {3017909},\n\tabstract = {In model-driven development of safety-critical systems (like \n\t\tautomotive, avionics or railways), wellformedness\n\t\tof models is repeatedly validated in order to detect design \n\t\tflaws as early as possible.\n\t\tValidation rules are often implemented by a large amount of \n\t\timperative model traversal code which\n\t\tmakes those rule implementations complicated and hard to \n\t\tmaintain. Additionally as models are\n\t\trapidly increasing in size and complexity, efficient \n\t\texecution of these operations is challenging for\n\t\tthe currently available toolchains. However, checking well-\n\t\tformedness constraints can be interpreted\n\t\tas evaluation of model queries, and the operations as model \n\t\ttransformations, where the validation\n\t\ttask can be specified in a concise way, and executed \n\t\tefficiently.\n\t\tThis paper presents a benchmark case and an evaluation \n\t\tframework to systematically assess the\n\t\tscalability of validating and revalidating well-formedness \n\t\tconstraints over large models. The benchmark\n\t\tcase defines a typical well-formedness validation scenario in \n\t\tthe railway domain including\n\t\tthe metamodel, an instance model generator, and a set of \n\t\twell-formedness constraints captured by\n\t\tqueries and repair operations (imitating the work of systems \n\t\tengineers by model transformations).\n\t\tThe benchmark case focuses on the execution time of the query \n\t\tevaluations with a special emphasis\n\t\ton reevaluations, as well as simple repair transformations.},\n\tyear = {2015},\n\teissn = {1613-0073},\n\tpages = {129-141},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n In model-driven development of safety-critical systems (like automotive, avionics or railways), wellformedness of models is repeatedly validated in order to detect design flaws as early as possible. Validation rules are often implemented by a large amount of imperative model traversal code which makes those rule implementations complicated and hard to maintain. Additionally as models are rapidly increasing in size and complexity, efficient execution of these operations is challenging for the currently available toolchains. However, checking well- formedness constraints can be interpreted as evaluation of model queries, and the operations as model transformations, where the validation task can be specified in a concise way, and executed efficiently. This paper presents a benchmark case and an evaluation framework to systematically assess the scalability of validating and revalidating well-formedness constraints over large models. The benchmark case defines a typical well-formedness validation scenario in the railway domain including the metamodel, an instance model generator, and a set of well-formedness constraints captured by queries and repair operations (imitating the work of systems engineers by model transformations). The benchmark case focuses on the execution time of the query evaluations with a special emphasis on reevaluations, as well as simple repair transformations.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Movie database case: An EMF-IncQuery solution.\n \n \n \n \n\n\n \n Szárnyas, G.; Semeráth, O.; Izsó, B.; Debreceni, C.; Hegedüs, Á.; Ujhelyi, Z.; and Bergmann, G.\n\n\n \n\n\n\n 2014.\n \n\n\n\n
\n\n\n\n \n \n \"MoviePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@CONFERENCE{MTMT:2813997,\n\ttitle = {Movie database case: An EMF-IncQuery solution},\n\turl = {https://m2.mtmt.hu/api/publication/2813997},\n\tauthor = {Szárnyas, Gábor and Semeráth, Oszkár and Izsó, Benedek and Debreceni, Csaba and Hegedüs, Ábel and Ujhelyi, Zoltán and Bergmann, Gábor},\n\tbooktitle = {7th Transformation Tool Contest},\n\tunique-id = {2813997},\n\tabstract = {This paper presents a solution for the Movie Database Case of the \n\t\tTransformation Tool Contest 2014, using EMF-INCQUERY and Xtend \n\t\tfor implementing the model transformation.},\n\tyear = {2014},\n\tpages = {103-115},\n\torcid-numbers = {Debreceni, Csaba/0000-0002-6263-7758; Hegedüs, Ábel/0000-0002-8940-4348; Ujhelyi, Zoltán/0000-0002-2091-6441; Bergmann, Gábor/0000-0002-2556-2582}\n}\n\n
\n
\n\n\n
\n This paper presents a solution for the Movie Database Case of the Transformation Tool Contest 2014, using EMF-INCQUERY and Xtend for implementing the model transformation.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf.\n \n \n \n \n\n\n \n Micskei, Z. I.; Raimund-Andreas, K.; Benedek, H.; Semeráth, O.; Vörös, A.; and Varró, D.\n\n\n \n\n\n\n 2014.\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@CONFERENCE{MTMT:2801379,\n\ttitle = {On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf},\n\turl = {https://m2.mtmt.hu/api/publication/2801379},\n\tauthor = {Micskei, Zoltán Imre and Raimund-Andreas, Konnerth and Benedek, Horváth and Semeráth, Oszkár and Vörös, András and Varró, Dániel},\n\tbooktitle = {Proceedings of the 1st Workshop on Open Source Software for Model Driven Engineering},\n\tunique-id = {2801379},\n\tabstract = {Executable and well-defined models are a cornerstone of model \n\t\tdriven engineering. We are currently working on a \n\t\ttransformation chain from UML models to formal verification \n\t\ttools. In the context of the UML language, the fUML \n\t\tand Alf specifications offer a standardized way for the \n\t\tsemantics of the basic model elements and a textual \n\t\tspecification language. Open source modeling tools started to \n\t\tadapt these specifications. However, their support \n\t\tis of varying degree. This paper summarizes our experiences \n\t\twith the open source tools regarding fUML and Alf \n\t\tsupport, and different model transformation technologies in \n\t\torder to analyse them with formal verification tools.},\n\tyear = {2014},\n\tpages = {31-41},\n\torcid-numbers = {Micskei, Zoltán Imre/0000-0003-1846-261X; Varró, Dániel/0000-0002-8790-252X}\n}\n\n
\n
\n\n\n
\n Executable and well-defined models are a cornerstone of model driven engineering. We are currently working on a transformation chain from UML models to formal verification tools. In the context of the UML language, the fUML and Alf specifications offer a standardized way for the semantics of the basic model elements and a textual specification language. Open source modeling tools started to adapt these specifications. However, their support is of varying degree. This paper summarizes our experiences with the open source tools regarding fUML and Alf support, and different model transformation technologies in order to analyse them with formal verification tools.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver.\n \n \n \n \n\n\n \n Semeráth, O.; Horváth, Á.; and Varró, D.\n\n\n \n\n\n\n LECTURE NOTES IN COMPUTER SCIENCE, 8107: 538-554. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"ValidationPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n 
@article{MTMT:2694711,\n\ttitle = {Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver},\n\turl = {https://m2.mtmt.hu/api/publication/2694711},\n\tauthor = {Semeráth, Oszkár and Horváth, Ákos and Varró, Dániel},\n\tdoi = {10.1007/978-3-642-41533-3_33},\n\tjournal-iso = {LNCS},\n\tjournal = {LECTURE NOTES IN COMPUTER SCIENCE},\n\tvolume = {8107},\n\tunique-id = {2694711},\n\tissn = {0302-9743},\n\tabstract = {Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, derived features and constraints can be formalized incorrectly resulting in incomplete, ambiguous or inconsistent DSL specifications. To detect such issues, we propose an automated mapping of EMF metamodels enriched with derived features and well-formedness constraints captured as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.},\n\tkeywords = {model validation; Computer Science, Software Engineering; Model queries},\n\tyear = {2013},\n\teissn = {1611-3349},\n\tpages = {538-554},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n
\n
\n\n\n
\n Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, derived features and constraints can be formalized incorrectly resulting in incomplete, ambiguous or inconsistent DSL specifications. To detect such issues, we propose an automated mapping of EMF metamodels enriched with derived features and well-formedness constraints captured as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);