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 - 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 AU - Varró, Dániel TI - Validation of Well-formedness Constraints on Uncertain Models T2 - The 10th Jubilee Conference of PhD Students in Computer Science (CS2) : June 27 – June 29, 2016. Szeged, Hungary 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 - Debreceni, Csaba AU - Horváth, Ákos AU - Hegedüs, Ábel AU - Ujhelyi, Zoltán AU - Ráth, István Zoltán AU - Varró, Dániel ED - C, Atkinson ED - E, Burger ED - T, Goldschmidt ED - R, Reussner TI - Query-driven Incremental Synchronization of View Models T2 - Proceedings of the 2nd Workshop on View-Based, Aspect-Oriented and Orthographic Software Modelling PB - ACM Press CY - New York, New York SN - 9781450329002 PY - 2014 SP - 31 EP - 38 PG - 8 DO - 10.1145/2631675.2631677 UR - https://m2.mtmt.hu/api/publication/2763253 ID - 2763253 AB - Views are key concepts of domain-specific modeling in order to provide specific focus of the designers by abstracting from unnecessary details of the underlying abstract model. Usually, these views are represented as models themselves (view models), computed from the source model. However, the efficient maintenance of views when the source model changes is challenging, as recalculation from scratch has to be avoided to achieve scalability. In the paper, we propose an approach to define view models in a highly automated way, based on declarative model queries. The views are automatically populated in accordance with the lifecycle of regular model elements - however, their existence is entirely bound to the underlying abstract model. This means that view models are automatically and incrementally maintained. Our contribution can also be interpreted as extending the concepts of derived features to derived objects, specified and maintained by incremental queries. LA - English DB - MTMT ER - TY - CHAP AU - Horváth, Ákos AU - Hegedüs, Ábel AU - Búr, Márton AU - Varró, Dániel AU - Starr, Rodrigo R AU - Mirachi, Samoel ED - IEEE, null TI - Hardware-software allocation specification of IMA systems for early simulation T2 - 33rd Digital Avionics Systems Conference, DASC 2014 PB - Institute of Electrical and Electronics Engineers (IEEE) CY - New York, New York SN - 9781479950010 PY - 2014 SP - 4D3-1 EP - 4D3-15 PG - 15 DO - 10.1109/DASC.2014.6979474 UR - https://m2.mtmt.hu/api/publication/2801126 ID - 2801126 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 -