TY - JOUR AU - Babikian, Aren A. AU - Semeráth, Oszkár AU - Varró, Dániel TI - Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search JF - IEEE TRANSACTIONS ON SOFTWARE ENGINEERING J2 - IEEE T SOFTWARE ENG VL - 50 PY - 2024 IS - 1 SP - 48 EP - 68 PG - 21 SN - 0098-5589 DO - 10.1109/TSE.2023.3331254 UR - https://m2.mtmt.hu/api/publication/34375495 ID - 34375495 N1 - Department of Electrical and Computer Engineering, McGill University, Canada Department of Measurement and Information Systems, Budapest University of Technology and Economics, Hungary Export Date: 30 November 2023 CODEN: IESED Funding Agency and Grant Number: NSERC Funding text: No Statement Available AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Babikian, Aren A. AU - Semeráth, Oszkár AU - Li, Anqi AU - Marussy, Kristóf AU - Varró, Dániel TI - Automated generation of consistent models using qualitative abstractions and exploration strategies JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 21 PY - 2022 IS - 5 SP - 1763 EP - 1787 PG - 25 SN - 1619-1366 DO - 10.1007/s10270-021-00918-6 UR - https://m2.mtmt.hu/api/publication/32394785 ID - 32394785 AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Chen, Boqi AU - Marussy, Kristóf AU - Pilarski, Sebastian AU - Semeráth, Oszkár AU - Varró, Dániel ED - Aehnelt, M. ED - Kirste, T. TI - Consistent Scene Graph Generation by Constraint Optimization T2 - ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450394758 T3 - ACM international conference proceeding PY - 2022 SP - 1 EP - 13 PG - 13 DO - 10.1145/3551349.3560433 UR - https://m2.mtmt.hu/api/publication/33648748 ID - 33648748 N1 - Electrical and Computer Engineering, McGill University, Montreal, QC, Canada Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary LA - English DB - MTMT ER - TY - CHAP AU - Ficsor, Attila AU - Semeráth, Oszkár ED - Renczes, Balázs TI - An Initial Performance Analysis of Graph Predicate Evaluation over Partial Models T2 - Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218722 PY - 2022 SP - 1 EP - 4 PG - 4 DO - 10.3311/MINISY2022-001 UR - https://m2.mtmt.hu/api/publication/33283704 ID - 33283704 LA - English DB - MTMT ER - TY - JOUR AU - Marussy, Kristóf AU - Semeráth, Oszkár AU - Varró, Dániel TI - Automated Generation of Consistent Graph Models with Multiplicity Reasoning JF - IEEE TRANSACTIONS ON SOFTWARE ENGINEERING J2 - IEEE T SOFTWARE ENG VL - 48 PY - 2022 IS - 5 SP - 1610 EP - 1629 PG - 20 SN - 0098-5589 DO - 10.1109/TSE.2020.3025732 UR - https://m2.mtmt.hu/api/publication/31360895 ID - 31360895 N1 - Funding Agency and Grant Number: BME-Artificial Intelligence FIKP grant of EMMI (BME FIKP-MI/SC); BME NC TKP2020 grant of NKFIH Hungary; New National Excellence Program of the Ministry for Innovation and Technology from National Research, Development and Innovation Fund [UNKP-20-4]; NSERC [RGPIN-04573-16] Funding text: This work was partially supported by BME-Artificial Intelligence FIKP grant of EMMI (BME FIKP-MI/SC), the BME NC TKP2020 grant of NKFIH Hungary, the UNKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and the NSERC RGPIN-04573-16 project. AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Kovacs, Laszlo AU - Semeráth, Oszkár ED - Andrey, Brito ED - Fernando, Pedone TI - Towards the Formal Semantics of Scenario Tests for Autonomous Vehicles T2 - 2021 10th Latin-American Symposium on Dependable Computing (LADC) PB - IEEE CY - Piscataway (NJ) SN - 9781665478311 PY - 2021 SP - 01 EP - 04 PG - 4 DO - 10.1109/LADC53747.2021.9672554 UR - https://m2.mtmt.hu/api/publication/32605462 ID - 32605462 LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Aren, A. Babikian AU - Boqi, Chen AU - Chuning, Li AU - Marussy, Kristóf AU - Szárnyas, Gábor AU - Varró, Dániel TI - Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 20 PY - 2021 IS - 5 SP - 1713 EP - 1734 PG - 22 SN - 1619-1366 DO - 10.1007/s10270-021-00884-z UR - https://m2.mtmt.hu/api/publication/32028274 ID - 32028274 N1 - MTA-BME Lendület Cyber-Physical Systems Res. Grp. Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tudósok krt. 2, Budapest, 1117, Hungary Department of Electrical and Computer Engineering, McGill University, 3480 Rue University, Montréal, QC H3A 0E9, Canada Cited By :1 Export Date: 9 June 2022 Correspondence Address: Semeráth, O.; MTA-BME Lendület Cyber-Physical Systems Res. Grp. Department of Measurement and Information Systems, Magyar tudósok krt. 2, Hungary; email: semerath@mit.bme.hu Funding details: Natural Sciences and Engineering Research Council of Canada, NSERC, PGSD3-546810-2020, RGPIN-04573-16 Funding details: Fonds de recherche du Québec – Nature et technologies, FRQNT, 272709 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding details: Innovációs és Technológiai Minisztérium Funding text 1: We would like to thank all three reviewers for their detailed and insightful feedback. This paper was partially supported by the NSERC RGPIN-04573-16 project, the NSERC PGSD3-546810-2020 scholarship, the McGill Grad Excellence Award-90025, the Fonds de recherche du Québec - Nature et technologies (FRQNT) B1X scholarship (file number: 272709), the ÚNKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and by the NRDI Fund based on the charter of bolster issued by the NRDI Office under the auspices of the Ministry for Innovation and Technology. We would like to thank the Department of Electrical and Computer Engineering, and the School of Computer Science of McGill University for providing resources to run our measurements. During the development of the achievements, we took into consideration the goals set by the Balatonfüred System Science Innovation Cluster and the plans of the “BME Balatonfüred Knowledge Center,” supported by EFOP 4.2.1-16-2017-00021. Funding text 2: We would like to thank all three reviewers for their detailed and insightful feedback. This paper was partially supported by the NSERC RGPIN-04573-16 project, the NSERC PGSD3-546810-2020 scholarship, the McGill Grad Excellence Award-90025, the Fonds de recherche du Qu?bec - Nature et technologies (FRQNT) B1X scholarship (file number: 272709), the ?NKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and by the NRDI Fund based on the charter of bolster issued by the NRDI Office under the auspices of the Ministry for Innovation and Technology. We would like to thank the Department of Electrical and Computer Engineering, and the School of Computer Science of McGill University for providing resources to run our measurements. During the development of the achievements, we took into consideration the goals set by the Balatonf?red System Science Innovation Cluster and the plans of the ?BME Balatonf?red Knowledge Center,? supported by EFOP 4.2.1-16-2017-00021. AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Aren, Babikian AU - Semeráth, Oszkár AU - Varró, Dániel ED - Wehrheim, Heike ED - Cabot, Jordi TI - Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers T2 - Fundamental Approaches to Software Engineering PB - Springer Netherlands CY - Cham SN - 9783030452339 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 12076. PY - 2020 SP - 441 EP - 461 PG - 21 DO - 10.1007/978-3-030-45234-6_22 UR - https://m2.mtmt.hu/api/publication/31160534 ID - 31160534 N1 - Cited By :3 Export Date: 27 June 2022 Correspondence Address: Babikian, A.A.; McGill UniversityCanada; email: aren.babikian@mail.mcgill.ca LA - English DB - MTMT ER - TY - CHAP AU - Chen, Boqi AU - Havelock, Dylan AU - Plante, Connor AU - Sukkarieh, Michael AU - Semeráth, Oszkár AU - Varró, Dániel ED - Esther, Guerra ED - Ludovico, Iovino TI - Automated video game world map synthesis by model-based techniques T2 - Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450381352 PY - 2020 SP - 1 EP - 5 PG - 5 DO - 10.1145/3417990.3422001 UR - https://m2.mtmt.hu/api/publication/31872191 ID - 31872191 LA - English DB - MTMT ER - TY - JOUR AU - Marussy, Kristóf AU - Semeráth, Oszkár AU - Aren, A. Babikian AU - Varró, Dániel TI - A specification language for consistent model generation based on partial models JF - JOURNAL OF OBJECT TECHNOLOGY J2 - J OBJECT TECHNOL VL - 19 PY - 2020 IS - 3 SP - 1 EP - 22 PG - 22 SN - 1660-1769 DO - 10.5381/jot.2020.19.3.a12 UR - https://m2.mtmt.hu/api/publication/31361799 ID - 31361799 LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Farkas, Rebeka AU - Bergmann, Gábor AU - Varró, Dániel TI - Diversity of Graph Models and Graph Generators in Mutation Testing JF - INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER J2 - INT J SOFTW TOOLS TECHN TRANSFER VL - 22 PY - 2020 SP - 57 EP - 78 PG - 22 SN - 1433-2779 DO - 10.1007/s10009-019-00530-6 UR - https://m2.mtmt.hu/api/publication/30748493 ID - 30748493 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Babikian, Aren A. AU - Li, Anqi AU - Marussy, Kristóf AU - Varró, Dániel TI - Automated generation of consistent models with structural and attribute constraints T2 - Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450370196 PY - 2020 SP - 187 EP - 199 PG - 13 DO - 10.1145/3365438.3410962 UR - https://m2.mtmt.hu/api/publication/31872205 ID - 31872205 LA - English DB - MTMT ER - TY - CHAP AU - Majzik, István AU - Semeráth, Oszkár AU - Hajdu, Csaba AU - Marussy, Kristóf AU - Szatmári, Zoltán AU - Micskei, Zoltán Imre AU - Vörös, András AU - Aren, A. Babikian AU - Varró, Dániel TI - Towards System-Level Testing with Coverage Guarantees for Autonomous Vehicles T2 - Proceedings of the IEEE / ACM 22nd International Conference on Model Driven Engineering Languages and Systems (MODELS) PB - IEEE CY - Munich SN - 9781728125367 PY - 2019 SP - 89 EP - 94 PG - 6 SN - 9781728125367 DO - 10.1109/MODELS.2019.00-12 UR - https://m2.mtmt.hu/api/publication/30748490 ID - 30748490 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Aren, A Babikian AU - Sebastian, Pilarski AU - Varró, Dániel ED - Silvia, Abrahão TI - Viatra Solver: A Framework for the Automated Generation of Consistent Domain-Specific Models T2 - 2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) PB - IEEE CY - Piscataway (NJ) SN - 9781728117645 PY - 2019 SP - 43 EP - 46 PG - 4 DO - 10.1109/ICSE-Companion.2019.00034 UR - https://m2.mtmt.hu/api/publication/30748475 ID - 30748475 N1 - ISSN:2574-1926 AB - 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. LA - English DB - MTMT ER - TY - THES AU - Semeráth, Oszkár TI - Formal validation and model generation for domain-specific languages by logic solvers PB - Budapesti Műszaki és Gazdaságtudományi Egyetem PY - 2019 UR - https://m2.mtmt.hu/api/publication/31347768 ID - 31347768 LA - English DB - MTMT ER - TY - CHAP AU - Varró, Dániel AU - Semeráth, Oszkár AU - Szárnyas, Gábor AU - Horváth, Ákos ED - Reiko, Heckel ED - Gabriele, Taentzer TI - Towards the Automated Generation of Consistent, Diverse, Scalable and Realistic Graph Models T2 - Graph Transformation, Specifications, and Nets PB - Springer Netherlands CY - Berlin CY - Heidelberg SN - 9783319753959 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 10800. PY - 2018 SP - 285 EP - 312 PG - 28 DO - 10.1007/978-3-319-75396-6_16 UR - https://m2.mtmt.hu/api/publication/3327320 ID - 3327320 LA - English DB - MTMT ER - TY - CHAP AU - Marussy, Kristóf AU - Semeráth, Oszkár AU - Varró, Dániel ED - Andrzej, Wąsowski ED - Richard, Paige ED - Øystein, Haugen TI - Incremental View Model Synchronization Using Partial Models T2 - ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) SN - 9781450349499 PY - 2018 SP - 323 EP - 333 PG - 11 DO - 10.1145/3239372.3239412 UR - https://m2.mtmt.hu/api/publication/3398313 ID - 3398313 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Nagy, András Szabolcs AU - Varró, Dániel ED - Marsha, Chechik ED - Mark, Harman TI - A Graph Solver for the Automated Generation of Consistent Domain-Specific Models T2 - ICSE '18 PB - ACM Press CY - New York, New York SN - 9781450356381 PY - 2018 SP - 980 EP - 980 PG - 12 DO - 10.1145/3180155.3180186 UR - https://m2.mtmt.hu/api/publication/3335161 ID - 3335161 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Varró, Dániel ED - Alessandra, Russo ED - Andy, Schürr TI - Iterative Generation of Diverse Models for Testing Specifications of DSL Tools T2 - Fundamental Approaches to Software Engineering PB - Springer Netherlands CY - Cham (Németország) SN - 9783319893624 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 10802. PY - 2018 SP - 227 EP - 245 PG - 17 DO - 10.1007/978-3-319-89363-1_13 UR - https://m2.mtmt.hu/api/publication/3335171 ID - 3335171 LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Varró, Dániel TI - Evaluating Well-Formedness Constraints on Incomplete Models JF - ACTA CYBERNETICA J2 - ACTA CYBERN-SZEGED VL - 23 PY - 2017 IS - 2 SP - 687 EP - 713 PG - 26 SN - 0324-721X DO - 10.14232/actacyb.23.2.2017.15 UR - https://m2.mtmt.hu/api/publication/3229152 ID - 3229152 AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Ágnes, Barta AU - Horváth, Ákos AU - Szatmári, Zoltán AU - Varró, Dániel TI - Formal validation of domain-specific languages with derived features and well-formedness constraints JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 16 PY - 2017 IS - 2 SP - 357 EP - 392 PG - 36 SN - 1619-1366 DO - 10.1007/s10270-015-0485-x UR - https://m2.mtmt.hu/api/publication/3018014 ID - 3018014 N1 - Admin megjegyzés-26708308 #JournalID1# Name: Software & Systems Modeling ISSN: 1619-1366 #JournalID2# AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Varró, Dániel TI - Graph constraint evaluation over partial models by constraint rewriting JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 10374 PY - 2017 SP - 138 EP - 154 PG - 17 SN - 0302-9743 DO - 10.1007/978-3-319-61473-1_10 UR - https://m2.mtmt.hu/api/publication/3277444 ID - 3277444 AB - n 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. LA - English DB - MTMT ER - TY - CONF AU - Semeráth, Oszkár AU - Varró, Dániel ED - Ferenc, Rudolf ED - Bánhelyi, Balázs ED - Gergely, Tamás ED - Kertész, Attila ED - Kincses, Zoltán TI - Validation of Well-formedness Constraints on Uncertain Models T2 - The 10th Jubilee Conference of PhD Students in Computer Science (CS2) PB - University of Szeged, Institute of Informatics C1 - Szeged PY - 2016 SP - 68 EP - 68 PG - 1 UR - https://m2.mtmt.hu/api/publication/3172186 ID - 3172186 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Debreceni, Csaba AU - Horváth, Ákos AU - Varró, Dániel ED - Benoit, Baudry ED - Benoit, Combemale TI - Incremental Backward Change Propagation of View Models by Logic Solvers T2 - MODELS '16 PB - ACM Press CY - New York, New York SN - 9781450343213 PY - 2016 SP - 306 EP - 316 PG - 11 DO - 10.1145/2976767.2976788 UR - https://m2.mtmt.hu/api/publication/3169820 ID - 3169820 AB - 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. LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Vörös, András AU - Varró, Dániel ED - Perdita, Stevens ED - Andrzej, Wasowski TI - Iterative and incremental model generation by logic solvers T2 - Fundamental Approaches to Software Engineering PB - Springer Netherlands CY - Berlin CY - Heidelberg SN - 9783662496640 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 9633. PY - 2016 SP - 87 EP - 103 PG - 17 DO - 10.1007/978-3-662-49665-7_6 UR - https://m2.mtmt.hu/api/publication/3018468 ID - 3018468 LA - English DB - MTMT ER - TY - CONF AU - Semeráth, Oszkár ED - Jeff, Gray ED - Ruth, Breu TI - Formal Validation and Model Synthesis for Domain-specific Languages by Logic Solvers T2 - ACM Student Research Competition at MODELS 2016 PB - CEUR Workshop Proceedings T3 - CEUR Workshop Proceedings, ISSN 1613-0073 ; 1775. PY - 2016 PG - 7 UR - https://m2.mtmt.hu/api/publication/3169934 ID - 3169934 LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Debreceni, Csaba AU - Horváth, Ákos AU - Varró, Dániel ED - A, Anjorin ED - J, Gibbons TI - Change Propagation of View Models by Logic Synthesis using SAT solvers. T2 - Proceedings of the 5th International Workshop on Bidirectional Transformations, Bx 2016, co-located with The European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 8, 2016. PB - CEUR Workshop Proceedings CY - Aachen T3 - CEUR Workshop Proceedings, ISSN 1613-0073 ; 1571. PY - 2016 SP - 40 EP - 44 PG - 5 UR - https://m2.mtmt.hu/api/publication/3092093 ID - 3092093 LA - English DB - MTMT ER - TY - CONF AU - Szárnyas, Gábor AU - Semeráth, Oszkár AU - Ráth, István Zoltán AU - Varró, Dániel ED - Louis, M Rose ED - Tassilo, Horn ED - Filip, Křikava TI - The TTC 2015 Train Benchmark Case for Incremental Model Validation T2 - 8th Transformation Tool Contest 2015 PB - CEUR Workshop Proceedings T3 - CEUR Workshop Proceedings, ISSN 1613-0073 ; 1524. PY - 2015 SP - 129 EP - 141 PG - 13 UR - https://m2.mtmt.hu/api/publication/3017909 ID - 3017909 AB - 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. LA - English DB - MTMT ER - TY - CONF AU - Szárnyas, Gábor AU - Semeráth, Oszkár AU - Izsó, Benedek AU - Debreceni, Csaba AU - Hegedüs, Ábel AU - Ujhelyi, Zoltán AU - Bergmann, Gábor ED - Krause, C ED - Horn, T ED - Rose, L M TI - Movie database case: An EMF-IncQuery solution T2 - 7th Transformation Tool Contest PB - CEUR Workshop Proceedings C1 - York T3 - CEUR Workshop Proceedings, ISSN 1613-0073 ; 1305. PY - 2014 SP - 103 EP - 115 PG - 13 UR - https://m2.mtmt.hu/api/publication/2813997 ID - 2813997 AB - 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. LA - English DB - MTMT ER - TY - CONF AU - Micskei, Zoltán Imre AU - Raimund-Andreas, Konnerth AU - Benedek, Horváth AU - Semeráth, Oszkár AU - Vörös, András AU - Varró, Dániel ED - Francis, Bordelau ED - Juergen, Dingel ED - Sebastien, Gerard ED - Sebastian, Voss TI - On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf T2 - Proceedings of the 1st Workshop on Open Source Software for Model Driven Engineering PB - CEUR Workshop Proceedings PY - 2014 SP - 31 EP - 41 PG - 11 UR - https://m2.mtmt.hu/api/publication/2801379 ID - 2801379 AB - 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. LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Horváth, Ákos AU - Varró, Dániel TI - Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 8107 PY - 2013 SP - 538 EP - 554 PG - 17 SN - 0302-9743 DO - 10.1007/978-3-642-41533-3_33 UR - https://m2.mtmt.hu/api/publication/2694711 ID - 2694711 LA - English DB - MTMT ER -