@inproceedings{MTMT:35286024, title = {Automated Transformation of a Domain-Specific Language for System Modeling to Stochastic Colored Petri Nets}, url = {https://m2.mtmt.hu/api/publication/35286024}, author = {Bedini, Francesco and Raeth, Timo and Maschotta, Ralph and Sattler, Kai-Uwe and Zimmermann, Armin}, booktitle = {18TH ANNUAL IEEE INTERNATIONAL SYSTEMS CONFERENCE, SYSCON 2024}, doi = {10.1109/SysCon61195.2024.10553543}, unique-id = {35286024}, keywords = {domain-specific language; Petri net; Model-to-Model Transformation; scpn}, year = {2024} } @article{MTMT:34278544, title = {Termination and Expressiveness of Execution Strategies for Networks of Bidirectional Model Transformations}, url = {https://m2.mtmt.hu/api/publication/34278544}, author = {Klare, Heiko and Gleitze, Joshua}, doi = {10.1145/3543845}, journal-iso = {FORM ASP COMPUT}, journal = {FORMAL ASPECTS OF COMPUTING}, volume = {35}, unique-id = {34278544}, issn = {0934-5043}, abstract = {When developers describe a software system with multiple models, such as architecture diagrams, deployment descriptions, and source code, these models must represent the system in a uniform way, i.e., they must be and stay consistent. One means to automatically preserve consistency after changes to models are model transformations, of which bidirectional transformations that preserve consistency between two models have been well researched. To preserve consistency between multiple models, such transformations can be combined to networks. When transformations are developed independently and reused modularly, the resulting network can be of arbitrary topology. For such networks, no universal strategy exists to orchestrate the execution of transformations such that the resulting models are consistent.In this article, we prove that termination of such a strategy can only be guaranteed if it is incomplete, i.e., if it is allowed to fail to restore consistency for some changes although an execution order of transformations exists that yields consistent models. We propose such a strategy, for which we prove termination and show that and why it makes it easier for users of model transformation networks to understand the reasons whenever the strategy fails. In addition, we provide a simulator for the comparison of different execution strategies. These findings help transformation developers and users in understanding when and why they can expect the execution of a transformation network to terminate and when they can even expect it to succeed. Furthermore, the proposed strategy guarantees them termination and supports them in finding the reason whenever it is not successful.}, keywords = {model transformation; Bidirectional transformation; model consistency; transformation network; transformation execution strategy; transformation termination}, year = {2023}, eissn = {1433-299X} } @article{MTMT:32769023, title = {Model Transformation Testing and Debugging: A Survey}, url = {https://m2.mtmt.hu/api/publication/32769023}, author = {Troya, Javier and Segura, Sergio and Burgueño, Lola and Wimmer, Manuel}, doi = {10.1145/3523056}, journal-iso = {ACM COMPUT SURV}, journal = {ACM COMPUTING SURVEYS}, volume = {55}, unique-id = {32769023}, issn = {0360-0300}, abstract = {Model transformations are the key technique in Model-Driven Engineering (MDE) to manipulate and construct models. As a consequence, the correctness of software systems built with MDE approaches relies mainly on the correctness of model transformations, and thus, detecting and locating bugs in model transformations have been popular research topics in recent years. This surge of work has led to a vast literature on model transformation testing and debugging, which makes it challenging to gain a comprehensive view of the current state-of-the-art. This is an obstacle for newcomers to this topic and MDE practitioners to apply these approaches. This article presents a survey on testing and debugging model transformations based on the analysis of 140 papers on the topics. We explore the trends, advances, and evolution over the years, bringing together previously disparate streams of work and providing a comprehensive view of these thriving areas. In addition, we present a conceptual framework to understand and categorize the different proposals. Finally, we identify several open research challenges and propose specific action points for the model transformation community.}, keywords = {Survey; model transformation; Testing; Debugging}, year = {2023}, eissn = {1557-7341} } @inproceedings{MTMT:32962493, title = {Finding a Universal Execution Strategy for Model Transformation Networks}, url = {https://m2.mtmt.hu/api/publication/32962493}, author = {Gleitze, Joshua and Klare, Heiko and Burger, Erik}, booktitle = {Fundamental Approaches to Software Engineering: 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021}, doi = {10.1007/978-3-030-71500-7_5}, unique-id = {32962493}, abstract = {When using multiple models to describe a (software) system, one can use a network of model transformations to keep the models consistent after changes. No strategy exists, however, to orchestrate the execution of transformations if the network has an arbitrary topology. In this paper, we analyse how often and in which order transformations need to be executed. We argue why linear execution bounds are too restrictive to be useful in practice and prove that there is no upper bound for the number of necessary executions. To avoid non-termination, we propose a conservative strategy that makes execution failures easier to understand. These insights help developers and users of transformation networks to understand under which circumstances their networks can terminate. Additionally, the proposed strategy helps them to find the cause when a network cannot restore consistency.}, keywords = {model consistency; model transformation networks}, year = {2021}, pages = {87-107}, orcid-numbers = {Gleitze, Joshua/0000-0002-0392-5338; Klare, Heiko/0000-0002-9711-8835; Burger, Erik/0000-0003-2832-3349} } @article{MTMT:32387575, title = {Towards language-to-language transformation}, url = {https://m2.mtmt.hu/api/publication/32387575}, author = {Kopetzki, Dawid and Lybecait, Michael and Naujokat, Stefan and Steffen, Bernhard}, doi = {10.1007/s10009-021-00630-2}, journal-iso = {INT J SOFTW TOOLS TECHN TRANSFER}, journal = {INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER}, unique-id = {32387575}, issn = {1433-2779}, abstract = {This paper proposes a simplicity-oriented approach and framework for language-to-language transformation of, in particular, graphical languages. Key to simplicity is the decomposition of the transformation specification into sub-rule systems that separately specify purpose-specific aspects. We illustrate this approach by employing a variation of Plotkin's Structural Operational Semantics (SOS) for pattern-based transformations of typed graphs in order to address the aspect 'computation' in a graph rewriting fashion. Key to our approach are two generalizations of Plotkin's structural rules: the use of graph patterns as the matching concept in the rules, and the introduction of node and edge types. Types do not only allow one to easily distinguish between different kinds of dependencies, like control, data, and priority, but may also be used to define a hierarchical layering structure. The resulting Type-based Structural Operational Semantics (TSOS) supports a well-structured and intuitive specification and realization of semantically involved language-to-language transformations adequate for the generation of purpose-specific views or input formats for certain tools, like, e.g., model checkers. A comparison with the general-purpose transformation frameworks ATL and Groove, illustrates along the educational setting of our graphical WebStory language that TSOS provides quite a flexible format for the definition of a family of purpose-specific transformation languages that are easy to use and come with clear guarantees.}, keywords = {ABSTRACTION; Model checking; Graph rewriting; graph pattern; Model-to-Model Transformation; Multi-level transformations; (Typed) structural operational semantics; Structural aggregation; Rule systems; Meta language}, year = {2021}, eissn = {1433-2787} } @article{MTMT:31457551, title = {An Approach for the Transformation and Verification of BPMN Models to Colored Petri Nets Models}, url = {https://m2.mtmt.hu/api/publication/31457551}, author = {Meghzili, Said and Chaoui, Allaoua and Strecker, Martin and Kerkouche, Elhillali}, doi = {10.4018/IJSI.2020010102}, journal-iso = {INTERNATIONAL JOURNAL OF SOFTWARE INNOVATION}, journal = {INTERNATIONAL JOURNAL OF SOFTWARE INNOVATION}, volume = {8}, unique-id = {31457551}, issn = {2166-7160}, abstract = {The correctness of transformations has recently begun to attract the attention of the researchers in Model Driven Engineering (MDE). The objective of this article is twofold. First, it presents an approach for transforming BPMN models to Colored Petri nets models using GROOVE and EMF/Xpand tools. Second, it proposes an approach for checking the correctness of the transformation itself. More precisely, we have defined the termination property of the transformation and the preservation of some structural properties of BPMN models by the transformation using the GROOVE graph transformation tool. The authors have also applied the approach on a case study through which the authors have verified the successful termination of the transformation using GROOVE Model Checker and the target model properties using CPN Tools.}, keywords = {Graph transformation; TERMINATION; formal verification; BPMN; Model-Driven engineering; Model checker; CPN; Transformation Correctness}, year = {2020}, eissn = {2166-7179}, pages = {17-49} } @article{MTMT:3393434, title = {Survey and classification of model transformation tools}, url = {https://m2.mtmt.hu/api/publication/3393434}, author = {Kahani, N and Bagherzadeh, M and Cordy, JR and Dingel, J and Varró, Dániel}, doi = {10.1007/s10270-018-0665-6}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {18}, unique-id = {3393434}, issn = {1619-1366}, year = {2019}, eissn = {1619-1374}, pages = {2361-2397}, orcid-numbers = {Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:30525047, title = {An Approach Based on Hierarchical Petri Nets for the Verification of Interconnected BPEL Processes}, url = {https://m2.mtmt.hu/api/publication/30525047}, author = {Saida, Boukhedouma and Zaia, Alimazighi}, doi = {10.4018/IJISMD.2018040103}, journal-iso = {IJISMD}, journal = {INTERNATIONAL JOURNAL OF INFORMATION SYSTEM MODELING AND DESIGN}, volume = {9}, unique-id = {30525047}, issn = {1947-8186}, abstract = {This article describes an MDE approach for transformation from BPEL specifications to WF-nets models for verifying behavioral properties on IOWF (Inter-Organizational Workflow) processes. The authors consider WF processes specified with BPEL and interconnected together according to specific cooperation patterns. They define a specific class of Petri nets called Hierarchical WF-nets (HWN) in order to formally check the "soundness" property on IOWF process models. For that, their verification approach is defined around three main phases: (i) recovery of the BPEL file(s) and generation of process tree(s), (ii) transformation from BPEL to WF-nets (resp. HWN) models using mapping and transformation rules and (iii) verification of the "soundness" property on the models obtained. They particularly define and implement a set of specific transformation rules which are closely linked to the interconnection rules attached to each cooperation pattern. Also, to show the feasibility of their verification method, the authors developed a "WF-Checking" tool which allows the implementation and testing of the proposed approach.}, keywords = {verification; SOA; Abstract Transition; BPEL; Cooperation Pattern; Hierarchical WF-net (HWN); IOWF; Soundness; WF-net}, year = {2018}, eissn = {1947-8194}, pages = {44-78} } @article{MTMT:27163183, title = {Using internal domain-specific languages to inherit tool support and modularity for model transformations}, url = {https://m2.mtmt.hu/api/publication/27163183}, author = {Hinkel, Georg and Goldschmidt, Thomas and Burger, Erik and Reussner, Ralf}, doi = {10.1007/s10270-017-0578-9}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, unique-id = {27163183}, issn = {1619-1366}, year = {2017}, eissn = {1619-1374}, pages = {1-27} } @article{MTMT:27319792, title = {Inter-model Consistency Checking Using Triple Graph Grammars and Linear Optimization Techniques}, url = {https://m2.mtmt.hu/api/publication/27319792}, author = {Leblebici, Erhan and Anjorin, Anthony and Schuerr, Andy}, doi = {10.1007/978-3-662-54494-5_11}, editor = {Rubin, J}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {10202}, unique-id = {27319792}, issn = {0302-9743}, year = {2017}, pages = {191-207} } @article{MTMT:25804377, title = {Pattern-based Rewriting through Abstraction}, url = {https://m2.mtmt.hu/api/publication/25804377}, author = {Bottoni, Paolo and Guerra, Esther and de Lara, Juan}, doi = {10.3233/FI-2016-1325}, journal-iso = {FUND INFOR}, journal = {FUNDAMENTA INFORMATICAE}, volume = {144}, unique-id = {25804377}, issn = {0169-2968}, year = {2016}, eissn = {1875-8681}, pages = {109-160} } @article{MTMT:26230248, title = {Assessing and improving quality of QVTo model transformations}, url = {https://m2.mtmt.hu/api/publication/26230248}, author = {Gerpheide, Christine M and Schiffelers, Ramon R H and Serebrenik, Alexander}, doi = {10.1007/s11219-015-9280-8}, journal-iso = {SOFTWARE QUAL J}, journal = {SOFTWARE QUALITY JOURNAL}, volume = {24}, unique-id = {26230248}, issn = {0963-9314}, year = {2016}, eissn = {1573-1367}, pages = {797-834}, orcid-numbers = {Serebrenik, Alexander/0000-0002-1418-0095} } @article{MTMT:25471396, title = {Grammar-based model transformations: Definition, execution, and quality properties}, url = {https://m2.mtmt.hu/api/publication/25471396}, author = {Besova, Galina and Steenken, Dominik and Wehrheim, Heike}, doi = {10.1016/j.cl.2015.05.003}, journal-iso = {COMPUT LANG SYST STR}, journal = {COMPUTER LANGUAGES SYSTEMS & STRUCTURES}, volume = {43}, unique-id = {25471396}, issn = {1477-8424}, year = {2015}, eissn = {1873-6866}, pages = {116-138} } @article{MTMT:25471395, title = {Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings}, url = {https://m2.mtmt.hu/api/publication/25471395}, author = {Bruggink, H J Sander and Koenig, Barbara and Nolte, Dennis and Zantema, Hans}, doi = {10.1007/978-3-319-21145-9_4}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {9151}, unique-id = {25471395}, issn = {0302-9743}, year = {2015}, pages = {52-68} } @article{MTMT:24905344, title = {Static Fault Localization in Model Transformations}, url = {https://m2.mtmt.hu/api/publication/24905344}, author = {Burgueno, Loli and Troya, Javier and Wimmer, Manuel and Vallecillo, Antonio}, doi = {10.1109/TSE.2014.2375201}, journal-iso = {IEEE T SOFTWARE ENG}, journal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING}, volume = {41}, unique-id = {24905344}, issn = {0098-5589}, year = {2015}, eissn = {1939-3520}, pages = {490-506} } @article{MTMT:2925179, title = {Validating Rule-based Algorithms}, url = {https://m2.mtmt.hu/api/publication/2925179}, author = {Lengyel, László}, doi = {10.12700/APH.12.4.2015.4.4}, journal-iso = {ACTA POLYTECH HUNG}, journal = {ACTA POLYTECHNICA HUNGARICA}, volume = {12}, unique-id = {2925179}, issn = {1785-8860}, year = {2015}, eissn = {1785-8860}, pages = {59-75}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @article{MTMT:25471397, title = {Confluence Detection for Transformations of Labelled Transition Systems}, url = {https://m2.mtmt.hu/api/publication/25471397}, author = {Wijs, Anton}, doi = {10.4204/EPTCS.181.1}, journal-iso = {ELECTRON PROC THEOR COMPUT SCI}, journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE}, volume = {181}, unique-id = {25471397}, year = {2015}, eissn = {2075-2180}, pages = {1-15} } @article{MTMT:24542043, title = {Combining termination proofs in model transformation systems}, url = {https://m2.mtmt.hu/api/publication/24542043}, author = {Bisztray, D and Heckel, R}, doi = {10.1017/S0960129512000369}, journal-iso = {MATH STRUCT COMP SCI}, journal = {MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE}, volume = {24}, unique-id = {24542043}, issn = {0960-1295}, year = {2014}, eissn = {1469-8072} } @article{MTMT:25892363, title = {Termination analysis for graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/25892363}, author = {Bruggink, HJS and König, B and Zantema, H}, doi = {10.1007/978-3-662-44602-7_15}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {8705 LNCS}, unique-id = {25892363}, issn = {0302-9743}, year = {2014}, pages = {179-194} } @article{MTMT:25892364, title = {A graphical specification of model composition with triple graph grammars}, url = {https://m2.mtmt.hu/api/publication/25892364}, author = {Anwar, A and Benelallam, A and Nassar, M and Coulette, B}, doi = {10.1007/978-3-642-38209-3_1}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {7706 LNCS}, unique-id = {25892364}, issn = {0302-9743}, year = {2013}, pages = {1-18} } @article{MTMT:2658440, title = {Formal specification and analysis of functional properties of graph rewriting-based model transformation}, url = {https://m2.mtmt.hu/api/publication/2658440}, author = {Asztalos, Márk and Lengyel, László and Levendovszky, Tihamér}, doi = {10.1002/stvr.1502}, journal-iso = {SOFTW TEST VERIF REL}, journal = {SOFTWARE TESTING VERIFICATION & RELIABILITY}, volume = {23}, unique-id = {2658440}, issn = {0960-0833}, year = {2013}, eissn = {1099-1689}, pages = {405-435}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @article{MTMT:27185241, title = {Verification of model transformations: A survey of the state-of-the-art}, url = {https://m2.mtmt.hu/api/publication/27185241}, author = {Calegari, D and Szasz, N}, doi = {10.1016/j.entcs.2013.02.002}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {292}, unique-id = {27185241}, issn = {1571-0661}, year = {2013}, pages = {5-25} } @inproceedings{MTMT:25892365, title = {A declarative and bidirectional model transformation approach based on graph co-spans}, url = {https://m2.mtmt.hu/api/publication/25892365}, author = {Lamo, Y and Mantz, F and Rutle, A and De Lara, J}, booktitle = {15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013}, doi = {10.1145/2505879.2505900}, publisher = {ACM}, unique-id = {25892365}, year = {2013}, pages = {1-12} } @article{MTMT:24135051, title = {Attributed graph transformation with inheritance: Efficient conflict detection and local confluence analysis using abstract critical pairs}, url = {https://m2.mtmt.hu/api/publication/24135051}, author = {Golas, U and Lambers, L and Ehrig, H and Orejas, F}, doi = {10.1016/j.tcs.2012.01.032}, journal-iso = {THEOR COMPUT SCI}, journal = {THEORETICAL COMPUTER SCIENCE}, volume = {424}, unique-id = {24135051}, issn = {0304-3975}, year = {2012}, eissn = {1879-2294}, pages = {46-68} } @article{MTMT:23929288, title = {Combining graph transformation and algebraic specification into model transformation}, url = {https://m2.mtmt.hu/api/publication/23929288}, author = {Kreowski, H -J and Kuske, S and Von Totth, C}, doi = {10.1007/978-3-642-28412-0_13}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {7137 LNCS}, unique-id = {23929288}, issn = {0302-9743}, year = {2012}, eissn = {1611-3349}, pages = {193-208} } @article{MTMT:24135052, title = {Formal specification and testing of model transformations}, url = {https://m2.mtmt.hu/api/publication/24135052}, author = {Vallecillo, A and Gogolla, M and Burgueño, L and Wimmer, M and Hamann, L}, doi = {10.1007/978-3-642-30982-3_11}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {7320}, unique-id = {24135052}, issn = {0302-9743}, year = {2012}, eissn = {1611-3349}, pages = {399-437} } @inproceedings{MTMT:24135053, title = {Typing model transformations using tracts}, url = {https://m2.mtmt.hu/api/publication/24135053}, author = {Vallecillo, A and Gogolla, M}, booktitle = {Theory and Practice of Model Transformations}, doi = {10.1007/978-3-642-30476-7_4}, unique-id = {24135053}, year = {2012}, pages = {56-71} } @inproceedings{MTMT:24135047, title = {Semantic clone detection for model-based development of embedded systems}, url = {https://m2.mtmt.hu/api/publication/24135047}, author = {Al-Batran, B and Schätz, B and Hummel, B}, booktitle = {Model Driven Engineering Languages and Systems}, doi = {10.1007/978-3-642-24485-8_19}, unique-id = {24135047}, year = {2011}, pages = {258-272} } @article{MTMT:21490088, title = {DSLTrans: a turing incomplete transformation language}, url = {https://m2.mtmt.hu/api/publication/21490088}, author = {Barroca, B and Lúcio, L and Amaral, V and Félix, R and Sousa, V}, doi = {10.1007/978-3-642-19440-5_19}, volume = {2011}, unique-id = {21490088}, year = {2011}, pages = {296-305} } @article{MTMT:24135049, title = {Tractable model transformation testing}, url = {https://m2.mtmt.hu/api/publication/24135049}, author = {Gogolla, M and Vallecillo, A}, doi = {10.1007/978-3-642-21470-7_16}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {6698}, unique-id = {24135049}, issn = {0302-9743}, year = {2011}, eissn = {1611-3349}, pages = {221-235} } @article{MTMT:23885457, title = {Verification and validation of model refinement implemented through graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/23885457}, author = {Khedmati, M and Rafeh, V and Rahmani, M}, journal-iso = {INT J PHYS SCI}, journal = {INTERNATIONAL JOURNAL OF PHYSICAL SCIENCES}, volume = {6}, unique-id = {23885457}, issn = {1992-1950}, year = {2011}, pages = {4086-4090} } @article{MTMT:21529106, title = {Graph multiset transformation: a new framework for massively parallel computation inspired by DNA computing}, url = {https://m2.mtmt.hu/api/publication/21529106}, author = {Kreowski, HJ and Kuske, S}, doi = {10.1007/s11047-010-9245-6}, journal-iso = {NAT COMPUT}, journal = {NATURAL COMPUTING}, volume = {10}, unique-id = {21529106}, issn = {1567-7818}, year = {2011}, eissn = {1572-9796}, pages = {961-986} } @article{MTMT:24135042, title = {Automated Formal Verification of Graph Rewriting-Based Model Transformations}, url = {https://m2.mtmt.hu/api/publication/24135042}, author = {Asztalos, M and Ekler, P and Lengyel, L and Levendovszky, T and Madari, I and Vajk, T}, journal-iso = {Buletinul stiintific si tehnic al Universitatii Tehnice din Timisoara, Seria Automatica si Calculatoare}, journal = {Buletinul stiintific si tehnic al Universitatii Tehnice din Timisoara, Seria Automatica si Calculatoare}, volume = {55(69)}, unique-id = {24135042}, issn = {1223-7299}, year = {2010}, pages = {175-184} } @inproceedings{MTMT:2654235, title = {Formal Verification of Model Transformations: an Automated Framework}, url = {https://m2.mtmt.hu/api/publication/2654235}, author = {Asztalos, Márk and Madari, István and Vajk, Tamás and Lengyel, László and Levendovszky, Tihamér}, booktitle = {IEEE International Joint Conferences on Computational Cybernetics and Technical Informatics, ICCC-CONTI 2010}, doi = {10.1109/ICCCYB.2010.5491223}, unique-id = {2654235}, abstract = {Verification of models and model processing programs are inevitable in real world model-based software development. Model transformation developers are often interested in offline verification methods, when only the definition of the model transformation and the specification of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented formal and algorithmic background for a possible verification framework. Based on this background, this paper introduces a realization of an automated verification framework for graph rewriting-based model transformations. We illustrate the operation of the framework and demonstrate its applicability on a case study. Our goal is to further improve our approach in order to be able to be applied in more complex industrial solutions as well.}, year = {2010}, pages = {493-498}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @inproceedings{MTMT:2654234, title = {Towards Automated, Formal Verification of Model Transformations}, url = {https://m2.mtmt.hu/api/publication/2654234}, author = {Asztalos, Márk and Lengyel, László and Levendovszky, Tihamér}, booktitle = {3rd International Conference on Software Testing, Verification and Validation, ICST 2010}, doi = {10.1109/ICST.2010.42}, unique-id = {2654234}, abstract = {Verification of models and model processing programs are inevitable in real-world model-based software development. Model transformation developers are interested in offline verification methods, when only the definition of the model transformation and the metamodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented a formalism to describe the characteristics of model transformations in separate formal expressions called assertions. This description is based on the first-order logic, therefore, if deduction rules are provided, a reasoning system can use an assertion set to automatically derive additional assertions describing additional properties of model transformations. In this paper, we propose deduction rules and present the verification of a model transformation of processing business process models.}, year = {2010}, pages = {15-24}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @article{MTMT:2654241, title = {Towards Formal Analysis of Multi-paradigm Model Transformations}, url = {https://m2.mtmt.hu/api/publication/2654241}, author = {Asztalos, Márk and Madari, István and Lengyel, László}, doi = {10.1177/0037549709343545}, journal-iso = {SIMULATION}, journal = {SIMULATION-TRANSACTIONS OF THE SOCIETY FOR COMPUTER SIMULATION INTERNATIONAL}, volume = {86}, unique-id = {2654241}, issn = {0037-5497}, abstract = {The Multi-Paradigm Modeling (MPM) approach of model-based development emphasizes the specification of a system by multiple models. We use transformations to automatically transform, integrate and synchronize models. Verification and validation of model transformations are fundamental issues: we need to express what a valid model is and how a valid model transformation may transform the models; otherwise, we have to analyze each transformed model individually, which makes it difficult to automate the process of using models. We have formally analyzed various model transformations in several case studies and industrial projects. From this experience, we have distilled the frequently recurring techniques and solutions, referred to as Model Transformation Analysis (MTA) methods. These instances, similarly to design patterns in object-oriented programming, define special constructions as solutions for recurring problems that arise when one implements a model transformation. Moreover, MTA methods contain special techniques and language features that should be taken into account when one designs a model transformation framework or a model transformation language. We hope that MTA methods may be the basis of automated formal analysis techniques of model transformations. This paper contributes the concept and instances of MTA methods and provides a case study based on an industrial project of mobile application development. With this real-world example, we want to demonstrate the role and use of MTA methods. The case study is implemented in Visual Modeling and Transformation System (VMTS), which is a tool that realizes the MPM concept to provide a model and model transformation-based environment for software development.}, year = {2010}, eissn = {1741-3133}, pages = {429-452}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @article{MTMT:21490096, title = {Combining termination criteria by isolating deletion}, url = {https://m2.mtmt.hu/api/publication/21490096}, author = {Bisztray, D and Heckel, R}, doi = {10.1007/978-3-642-15928-2_14}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {6372}, unique-id = {21490096}, issn = {0302-9743}, year = {2010}, eissn = {1611-3349}, pages = {203-217} } @article{MTMT:23929054, title = {Visual Modelling and Analysis of Model Transformations based on Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/23929054}, author = {Ermel, C}, journal-iso = {BULL EATCS}, journal = {BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE}, volume = {2009}, unique-id = {23929054}, issn = {0252-9742}, year = {2010}, eissn = {0252-9742}, pages = {135-152} } @article{MTMT:24135045, title = {Specification and verification of model transformations}, url = {https://m2.mtmt.hu/api/publication/24135045}, author = {Hermann, F and Hülsbusch, M and König, B}, journal-iso = {ELECTR COMMUN EASST}, journal = {ELECTRONIC COMMUNICATIONS OF THE EASST}, volume = {30}, unique-id = {24135045}, issn = {1863-2122}, year = {2010}, pages = {1-21} } @inproceedings{MTMT:21490094, title = {Generating transformation rules from examples for behavioral models}, url = {https://m2.mtmt.hu/api/publication/21490094}, author = {Kessentini, M and Wimmer, M and Sahraoui, H and Boukadoum, M}, booktitle = {BM-FA '10: proceedings of the Second International Workshop on Behaviour Modelling: Foundation and Applications}, doi = {10.1145/1811147.1811149}, unique-id = {21490094}, year = {2010} } @inproceedings{MTMT:24135050, title = {An approach to refactoring legacy systems}, url = {https://m2.mtmt.hu/api/publication/24135050}, author = {Moeini, A and Rafe, V and Mahdian, F}, booktitle = {ICACTE 2010 - 2010 3rd International Conference on Advanced Computer Theory and Engineering, Proceedings}, doi = {10.1109/ICACTE.2010.5579183}, unique-id = {24135050}, year = {2010}, pages = {V55-V58} } @mastersthesis{MTMT:21490093, title = {Réécriture de graphes pour la construction de modčles en logique modale}, url = {https://m2.mtmt.hu/api/publication/21490093}, author = {Said, B}, unique-id = {21490093}, year = {2010} } @article{MTMT:23935213, title = {Refactoring of Execution Control Charts in Basic Function Blocks of the IEC 61499 Standard}, url = {https://m2.mtmt.hu/api/publication/23935213}, author = {Vyatkin, V and Dubinin, V}, doi = {10.1109/TII.2009.2033051}, journal-iso = {IEEE T IND INFORM}, journal = {IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS}, volume = {6}, unique-id = {23935213}, issn = {1551-3203}, year = {2010}, eissn = {1941-0050}, pages = {155-165} } @article{MTMT:2653932, title = {Compositionality of Model Transformations}, url = {https://m2.mtmt.hu/api/publication/2653932}, author = {Bisztray, Dénes András and Reiko, Heckel and Hartmut, Ehrig}, doi = {10.1016/j.entcs.2009.03.011}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {236}, unique-id = {2653932}, issn = {1571-0661}, year = {2009}, pages = {5-19} } @CONFERENCE{MTMT:24117350, title = {Towards a compositional approach to model transformation for software development}, url = {https://m2.mtmt.hu/api/publication/24117350}, author = {Hidaka, S Hu and Z, Kato H and Nakano, K}, booktitle = {Proceedings of the 2009 ACM Symposium on Applied Computing}, doi = {10.1145/1529282.1529383}, unique-id = {24117350}, year = {2009}, pages = {468-475} } @CONFERENCE{MTMT:24135043, title = {Warshall Based Detection of Conflicts and Dependencies in Graph Transformation System}, url = {https://m2.mtmt.hu/api/publication/24135043}, author = {Junbing, C and Zhijian, W and Si, Q and Bo, C}, booktitle = {Computational Intelligence and Software Engineering, 2009. CiSE 2009. International Conference on}, publisher = {IEEE}, unique-id = {24135043}, year = {2009}, pages = {1-4} } @inproceedings{MTMT:21490101, title = {Automatic refinement of platform independent models}, url = {https://m2.mtmt.hu/api/publication/21490101}, author = {Miralvand, M R Z and Rafe, V and Rafeh, R and Hajiee, M}, booktitle = {ICCTD 2009 - 2009 International Conference on Computer Technology and Development}, doi = {10.1109/ICCTD.2009.170}, unique-id = {21490101}, year = {2009}, pages = {191-195} } @inproceedings{MTMT:24135046, title = {Correctness, Completeness and Termination of Pattern-Based Model-to-Model Transformation}, url = {https://m2.mtmt.hu/api/publication/24135046}, author = {Orejas, F and Guerra, E and de Lara, J and Ehrig, H}, booktitle = {Algebra and Coalgebra in Computer Science}, doi = {10.1007/978-3-642-03741-2_26}, unique-id = {24135046}, year = {2009}, pages = {383-397} } @inproceedings{MTMT:21490102, title = {Automatic development of service oriented models using graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/21490102}, author = {Raftari, M and Joodaki, S}, booktitle = {TENCON 2009, 2009 IEEE Region 10 Conference}, doi = {10.1109/TENCON.2009.5395983}, unique-id = {21490102}, year = {2009} } @article{MTMT:21490105, title = {Towards a Systematic Method for Proving Termination of Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/21490105}, author = {Bruggink, H J S}, doi = {10.1016/j.entcs.2008.04.072}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {213}, unique-id = {21490105}, issn = {1571-0661}, year = {2008}, pages = {23-38} } @mastersthesis{MTMT:21490113, title = {Approche de métamodélisation pour la simulation et la vérification de modčle}, url = {https://m2.mtmt.hu/api/publication/21490113}, author = {Combemale, B}, unique-id = {21490113}, year = {2008} } @inproceedings{MTMT:21490112, title = {From UML Activities to TAAL-Towards Behaviour-Preserving Model Transformations}, url = {https://m2.mtmt.hu/api/publication/21490112}, author = {Engels, G and Kleppe, A and Rensink, A and Semenyak, M and Soltenborn, C and Wehrheim, H}, booktitle = {4th European Conference on Model Driven Architecture - Foundations and Applications}, doi = {10.1007/978-3-540-69100-6_7}, unique-id = {21490112}, year = {2008}, pages = {94-109} } @misc{MTMT:21490146, title = {Towards Compositional Approach to Model Transformation for Software Development}, url = {https://m2.mtmt.hu/api/publication/21490146}, author = {Hidaka, S and Hu, Z and Kato, H and Nakano, K}, unique-id = {21490146}, year = {2008} } @article{MTMT:21490103, title = {Undecidable Control Conditions in Graph Transformation Units}, url = {https://m2.mtmt.hu/api/publication/21490103}, author = {Hölscher, K and Klempien-Hinrichs, R and Knirsch, P}, doi = {10.1016/j.entcs.2007.08.028}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {195}, unique-id = {21490103}, issn = {1571-0661}, year = {2008}, pages = {95-111} } @mastersthesis{MTMT:23928884, title = {Graph-Based Software Specification and Verification}, url = {https://m2.mtmt.hu/api/publication/23928884}, author = {Kastenberg, Harmen}, unique-id = {23928884}, year = {2008} } @article{MTMT:21490110, title = {Graph multiset transformation as a framework for massively parallel computation}, url = {https://m2.mtmt.hu/api/publication/21490110}, author = {Kreowski, H J and Kuske, S}, doi = {10.1007/978-3-540-87405-8_24}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {5214}, unique-id = {21490110}, issn = {0302-9743}, year = {2008}, eissn = {1611-3349}, pages = {351-365} } @mastersthesis{MTMT:21490111, title = {Geraçao de expressoes algébricas para processos de negócio usando reduçoes de digrafos série-paralelo}, url = {https://m2.mtmt.hu/api/publication/21490111}, author = {Oikawa, M K}, unique-id = {21490111}, year = {2008} } @misc{MTMT:24135037, title = {Matrix Graph Grammars}, url = {https://m2.mtmt.hu/api/publication/24135037}, author = {Perez, Velasco P P}, unique-id = {24135037}, year = {2008} } @article{MTMT:21490811, title = {Graph Transformation Semantics for a QVT Language}, url = {https://m2.mtmt.hu/api/publication/21490811}, author = {Rensink, A and Nederpel, R}, doi = {10.1016/j.entcs.2008.04.029}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {211}, unique-id = {21490811}, issn = {1571-0661}, year = {2008}, pages = {51-62} } @CONFERENCE{MTMT:24135038, title = {Analysis of Model Transformations via Alloy}, url = {https://m2.mtmt.hu/api/publication/24135038}, author = {Anastasakis, K and Bordbar, B and Kuster, J M}, booktitle = {The 4th MoDeVVa workshop Model-Driven Engineering, Verification and Validation}, unique-id = {24135038}, year = {2007} } @article{MTMT:21490116, title = {Attributed graph transformation with node type inheritance}, url = {https://m2.mtmt.hu/api/publication/21490116}, author = {de Lara, J and Bardohl, R and Ehrig, H and Ehrig, K and Prange, U and Taentzer, G}, doi = {10.1016/j.tcs.2007.02.001}, journal-iso = {THEOR COMPUT SCI}, journal = {THEORETICAL COMPUTER SCIENCE}, volume = {376}, unique-id = {21490116}, issn = {0304-3975}, year = {2007}, eissn = {1879-2294}, pages = {139-163} } @mastersthesis{MTMT:23929628, title = {Erweiterung des Kantenkonzepts deklarativer Graphersetzungssysteme von Einfachkantenuber Hyperkanten zu}, url = {https://m2.mtmt.hu/api/publication/23929628}, author = {Denninger, O}, unique-id = {23929628}, year = {2007} } @{MTMT:25892366, title = {Meta-modelling and graph transformation for the definition of multi-view visual languages}, url = {https://m2.mtmt.hu/api/publication/25892366}, author = {Guerra, E and de Lara, J}, booktitle = {Visual Languages for Interactive Computing: Definitions and Formalizations}, doi = {10.4018/978-1-59904-534-4.ch004}, publisher = {IGI Global}, unique-id = {25892366}, year = {2007}, pages = {74-101} } @article{MTMT:21490114, title = {Incremental Resolution of Model Inconsistencies}, url = {https://m2.mtmt.hu/api/publication/21490114}, author = {Mens, T and Van, Der Straeten R}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4409}, unique-id = {21490114}, issn = {0302-9743}, year = {2007}, eissn = {1611-3349}, pages = {111-126} } @article{MTMT:21490122, title = {Termination of Algebraic Rewriting with Inhibitors}, url = {https://m2.mtmt.hu/api/publication/21490122}, author = {Bottoni, P and Hoffmann, K and Presicce, F P}, journal-iso = {ELECTR COMMUN EASST}, journal = {ELECTRONIC COMMUNICATIONS OF THE EASST}, volume = {4}, unique-id = {21490122}, issn = {1863-2122}, year = {2006}, pages = {1-13} } @CONFERENCE{MTMT:24135041, title = {Towards a Unified View of Model Mapping and Transformation}, url = {https://m2.mtmt.hu/api/publication/24135041}, author = {D'Antonio, F and Bottoni, P and Missikoff, M}, booktitle = {EMOI - INTEROP'06, Enterprise Modelling and Ontologies for Interoperability, Proceedings of the Open Interop Workshop on Enterprise Modelling and Ontologies for Interoperability}, unique-id = {24135041}, year = {2006} } @article{MTMT:23885380, title = {Overview of formal concepts for model transformations based on typed attributed graph transformation}, url = {https://m2.mtmt.hu/api/publication/23885380}, author = {Ehrig, H and Ehrig, K}, doi = {10.1016/j.entcs.2006.01.011}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {152}, unique-id = {23885380}, issn = {1571-0661}, year = {2006}, pages = {3-22} } @article{MTMT:23885382, title = {Towards model transformation in generated Eclipse editor plug-ins}, url = {https://m2.mtmt.hu/api/publication/23885382}, author = {Ehrig, K and Ermel, C and Hansgen, S}, doi = {10.1016/j.entcs.2006.01.013}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {152}, unique-id = {23885382}, issn = {1571-0661}, year = {2006}, pages = {39-52} } @article{MTMT:23929310, title = {Weakest preconditions for high-level programs}, url = {https://m2.mtmt.hu/api/publication/23929310}, author = {Habel, A and Pennemann, KH and Rensink, A}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4178}, unique-id = {23929310}, issn = {0302-9743}, year = {2006}, eissn = {1611-3349}, pages = {445-460} } @misc{MTMT:23929875, title = {Weakest Preconditions for High-Level Programs (Long Version)}, url = {https://m2.mtmt.hu/api/publication/23929875}, author = {Habel, A and Pennemann, K H and Rensink, A}, unique-id = {23929875}, year = {2006} } @article{MTMT:2665111, title = {Model Transformation with a Visual Control Flow Language}, url = {https://m2.mtmt.hu/api/publication/2665111}, author = {Lengyel, László and Levendovszky, Tihamér and Mezei, Gergely and Charaf, Hassan}, journal-iso = {INT J COMP SCI}, journal = {INTERNATIONAL JOURNAL OF COMPUTER SCIENCE}, volume = {1}, unique-id = {2665111}, issn = {1306-4428}, year = {2006}, pages = {45-53}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @CONFERENCE{MTMT:24135040, title = {Graph-Based Tool Support to Improve Model Quality}, url = {https://m2.mtmt.hu/api/publication/24135040}, author = {Mens, T and Van, Der Straeten R and Warny, J F}, booktitle = {Workshop on Quality in Modeling}, unique-id = {24135040}, year = {2006}, pages = {47-61} } @misc{MTMT:21490127, title = {Eine attributierte getypte Graphgrammatik zum syntaxgesteuerten Editieren von UML State Machines}, url = {https://m2.mtmt.hu/api/publication/21490127}, author = {Modica, T}, unique-id = {21490127}, year = {2006} } @article{MTMT:1635273, title = {Termination analysis of model transformations by Petri nets}, url = {https://m2.mtmt.hu/api/publication/1635273}, author = {Varró, Dániel and Varró-Gyapay, Szilvia and Ehrig, H and Prange, U and Taentzer, G}, doi = {10.1007/11841883_19}, journal-iso = {LNCS}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4178}, unique-id = {1635273}, issn = {0302-9743}, abstract = {Despite the increasing relevance of model transformation techniques in model-driven software development, research is mainly conducted to the specification and the automation of such transformations. However, since the transformations themselves may also contain conceptual flaws, it is essential to formally analyze them prior to executing them on user models. In the current paper, we focus on a central validation problem of trusted model transformations, namely, termination and propose a Petri net based analysis method that provides a sufficient criterion for the termination problem of model transformations captured by graph transformation systems.}, year = {2006}, eissn = {1611-3349}, pages = {260-274}, orcid-numbers = {Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:21490128, title = {High-level replacement units and their termination properties}, url = {https://m2.mtmt.hu/api/publication/21490128}, author = {Bottoni, P and Hoffmann, K and Presicce, FP and Taentzer, G}, doi = {10.1016/j.jvlc.2005.07.001}, journal-iso = {J VISUAL LANG COMPUT}, journal = {JOURNAL OF VISUAL LANGUAGES AND COMPUTING}, volume = {16}, unique-id = {21490128}, issn = {1045-926X}, year = {2005}, eissn = {1095-8533}, pages = {485-507} } @CONFERENCE{MTMT:1076669, title = {A Visual Control Flow Language and Its Termination Properties}, url = {https://m2.mtmt.hu/api/publication/1076669}, author = {Lengyel, László and Levendovszky, Tihamér and Charaf, Hassan}, booktitle = {Transactions on Enformatika, Systems Sciences and Engineering}, unique-id = {1076669}, keywords = {UML; Termination properties; OCL; Metamodel-based visual model transformation; Control flow}, year = {2005}, pages = {163-168}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} }