@article{MTMT:33890784, title = {A graph-based framework for model-driven optimization facilitating impact analysis of mutation operator properties}, url = {https://m2.mtmt.hu/api/publication/33890784}, author = {John, Stefan and Kosiol, Jens and Lambers, Leen and Taentzer, Gabriele}, doi = {10.1007/s10270-022-01078-x}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, unique-id = {33890784}, issn = {1619-1366}, abstract = {Optimization problems in software engineering typically deal with structures as they occur in the design and maintenance of software systems. In model-driven optimization (MDO), domain-specific models are used to represent these structures while evolutionary algorithms are often used to solve optimization problems. However, designing appropriate models and evolutionary algorithms to represent and evolve structures is not always straightforward. Domain experts often need deep knowledge of how to configure an evolutionary algorithm. This makes the use of model-driven meta-heuristic search difficult and expensive. We present a graph-based framework for MDO that identifies and clarifies core concepts and relies on mutation operators to specify evolutionary change. This framework is intended to help domain experts develop and study evolutionary algorithms based on domain-specific models and operators. In addition, it can help in clarifying the critical factors for conducting reproducible experiments in MDO. Based on the framework, we are able to take a first step toward identifying and studying important properties of evolutionary operators in the context of MDO. As a showcase, we investigate the impact of soundness and completeness at the level of mutation operator sets on the effectiveness and efficiency of evolutionary algorithms.}, keywords = {EVOLUTIONARY COMPUTATION; Search-based software engineering; Model-Driven engineering}, year = {2023}, eissn = {1619-1374} } @article{MTMT:34277514, title = {Towards Mechanised Proofs in Double-Pushout Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/34277514}, author = {Soldner, Robert and Plump, Detlef}, doi = {10.4204/EPTCS.374.6}, journal-iso = {ELECTRON PROC THEOR COMPUT SCI}, journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE}, unique-id = {34277514}, abstract = {We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition of direct derivations based on deletion and gluing. We then formalise graph pushouts and prove with Isabelle's help that both deletions and gluings are pushouts. We also prove that pushouts are unique up to isomorphism. The formalisation comprises around 2000 lines of source text. Our motivation is to pave the way for rigorous, machine-checked proofs in the theory of the double-pushout approach, and to lay the foundations for verifying graph transformation systems and rule-based graph programs by interactive theorem proving.}, year = {2022}, eissn = {2075-2180}, pages = {59-75} } @article{MTMT:32379486, title = {Proving the Correctness of Knowledge Graph Update: A Scenario From Surveillance of Adverse Childhood Experiences}, url = {https://m2.mtmt.hu/api/publication/32379486}, author = {Brenas, Jon Hael and Shaban-Nejad, Arash}, doi = {10.3389/fdata.2021.660101}, journal-iso = {FRONT BIG DATA}, journal = {FRONTIERS IN BIG DATA}, volume = {4}, unique-id = {32379486}, abstract = {Knowledge graphs are a modern way to store information. However, the knowledge they contain is not static. Instances of various classes may be added or deleted and the semantic relationship between elements might evolve as well. When such changes take place, a knowledge graph might become inconsistent and the knowledge it conveys meaningless. In order to ensure the consistency and coherency of dynamic knowledge graphs, we propose a method to model the transformations that a knowledge graph goes through and to prove that the new transformations do not yield inconsistencies. To do so, we express the knowledge graphs as logically decorated graphs, then we describe the transformations as algorithmic graph transformations and we use a Hoare-like verification process to prove correctness. To demonstrate the proposed method in action, we use examples from Adverse Childhood Experiences (ACEs), which is a public health crisis.}, keywords = {CLONING; Graph transformation; Program Verification; Merging; adverse childhood experiences; Knowledge graph}, year = {2021}, eissn = {2624-909X}, orcid-numbers = {Shaban-Nejad, Arash/0000-0003-2047-4759} } @article{MTMT:32389784, title = {Virtual network embedding: ensuring correctness and optimality by construction using model transformation and integer linear programming techniques}, url = {https://m2.mtmt.hu/api/publication/32389784}, author = {Tomaszek, Stefan and Speith, Roland and Schuerr, Andy}, doi = {10.1007/s10270-020-00852-z}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {20}, unique-id = {32389784}, issn = {1619-1366}, abstract = {Virtualization technology allows service providers to operate data centers in a cost-effective and scalable manner. The data center network (substrate network) and the applications executed in the data center (virtual networks) are often modeled as graphs. The nodes of the graphs represent (physical or virtual) servers and switches, and the edges represent communication links. Nodes and links are annotated with the provided and required resources (e.g., memory and bandwidth). The NP-hard virtual network embedding (VNE) problem deals with the embedding of a set of virtual networks to the substrate network such that (i) all (resource) constraints of the substrate network are fulfilled, and (ii) an objective is optimized (e.g., minimizing the communication costs). The existing two-step highly customizable model-driven virtual network embedding (MdVNE) approach combines model transformation (MT) and integer linear programming (ILP) techniques to solve the VNE problem based on a declarative specification. MdVNE generates element mapping candidates from an MT specification and identifies an optimal and correct embeddings using an ILP solver. In the past, developers created the MT and ILP specifications manually and needed to ensure carefully that both are compatible and respect the problem description. In this article, we present a novel construction methodology for synthesizing the MT and ILP specification from a given declarative model-based VNE problem description. This problem description consists of a metamodel for substrate and virtual networks, additional OCL constraints, and an objective function that assigns costs to a given model. This methodology ensures that the derived embeddings are correct w.r.t. the metamodel and the OCL constraints, and optimal w.r.t. the optimization goal. The novel model-based VNE specification is applicable to different network domains, environments, and constraints. Thus, the construction methodology allows to automate most of the steps to realize a correct and optimal VNE algorithm compared to a hand-crafted VNE implementation. Furthermore, the simulative evaluation confirms that using MT techniques reduces the time for solving the VNE problem considerably in comparison with a purely ILP-based approach.}, keywords = {model transformation; Graph transformation; integer linear programming; Model-driven development; Data center; object constraint language; virtual network embedding; Triple-graph grammar}, year = {2021}, eissn = {1619-1374}, pages = {1299-1332} } @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:30650843, title = {A systematic approach to constructing families of incremental topology control algorithms using graph transformation}, url = {https://m2.mtmt.hu/api/publication/30650843}, author = {Kluge, R. and Stein, M. and Varró, G. and Schürr, A. and Hollick, M. and Mühlhäuser, M.}, doi = {10.1007/s10270-017-0587-8}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {18}, unique-id = {30650843}, issn = {1619-1366}, year = {2019}, eissn = {1619-1374}, pages = {279-319} } @article{MTMT:31063806, title = {Reconfigurable GSPNs: A modeling formalism of evolvable discrete-event systems}, url = {https://m2.mtmt.hu/api/publication/31063806}, author = {Tigane, Samir and Kahloul, Laid and Benharzallah, Saber and Baarir, Souheib and Bourekkache, Samir}, doi = {10.1016/j.scico.2019.102302}, journal-iso = {SCI COMPUT PROGRAM}, journal = {SCIENCE OF COMPUTER PROGRAMMING}, volume = {183}, unique-id = {31063806}, issn = {0167-6423}, abstract = {Nowadays, a wide range of systems are becoming structurally dynamic, variably interconnected, and highly complex. The use of classical formal approaches, such as Petri nets, in the design of such systems becomes neither convenient nor sufficient. Indeed, they cannot handle, in a natural way, the dynamic structure and the growing complexity of modern systems.Introducing reconfigurability in Petri nets, as well as generalized stochastic Petri nets increases the modeling power, but decreases the applicability of analysis techniques. In fact, several properties become undecidableIn this paper, we extend generalized stochastic Petri nets to a reconfigurable formalism, while maintaining verifiability with reduced complexity. The proposed approach identifies a set of properties that are preserved after reconfiguration. These properties are decidable with reduced time and space complexity. The use of the proposed formalism is illustrated through a running example. (C) 2019 Elsevier B.V. All rights reserved.}, keywords = {performance evaluation; Formal Modeling and Verification; Reconfigurable generalized stochastic Petri nets; Net rewriting systems}, year = {2019}, eissn = {1872-7964}, orcid-numbers = {Tigane, Samir/0000-0001-9093-1180; Kahloul, Laid/0000-0002-9739-7715; Bourekkache, Samir/0000-0003-2038-6257} } @article{MTMT:30558176, title = {Applied Graph Transformation and Verification With Use Cases in Malaria Surveillance}, url = {https://m2.mtmt.hu/api/publication/30558176}, author = {Brenas, Jon Hael and Strecker, Martin and Echahed, Rachid and Shaban-Nejad, Arash}, doi = {10.1109/ACCESS.2018.2878311}, journal-iso = {IEEE ACCESS}, journal = {IEEE ACCESS}, volume = {6}, unique-id = {30558176}, issn = {2169-3536}, abstract = {Malaria is one of the leading causes of death and illness in sub-Saharan Africa. In order to make timely decisions for control and elimination of malaria, researchers, and clinicians need access to integrated consistent knowledge sources. These knowledge sources often rely on dynamic and constantly changing databases and ontologies. It is crucial to manage changes and ensure that these changes do not cause inconsistencies in the integrated knowledge source. To this end, we propose the use of a formal model using graph transformations to monitor and manage the changes in a coherent way while preserving the consistency of the integrated structure through classical verification. In this paper, we use an algorithmic approach to graph transformation, instead of the more classical algebraic approach, to express the evolution of the data and ontological structures. In this model, each transformation is the result of applying rules to the graph, where the left-hand side is used to select a subgraph and the right-hand side is a sequence of elementary actions to be performed. Strategies are used to define how transformation rules should be applied. This approach enables us to define a Hoare-like calculus that can be used to verify the transformations and manage the changes. In this paper, we demonstrate the feasibility and significance of the proposed method through different use cases in malaria surveillance.}, keywords = {Change management; Graph transformation; Verification; ontologies; malaria surveillance}, year = {2018}, eissn = {2169-3536}, pages = {64728-64741}, orcid-numbers = {Brenas, Jon Hael/0000-0001-9395-9365; Shaban-Nejad, Arash/0000-0003-2047-4759} } @{MTMT:30558174, title = {Multi-Granular Conflict and Dependency Analysis in Software Engineering based on Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/30558174}, author = {Lambers, Leen and Strueber, Daniel and Taentzer, Gabriele and Born, Kristopher and Huebert, Jevgenij}, booktitle = {PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE)}, doi = {10.1145/3180155.3180258}, unique-id = {30558174}, abstract = {Conflict and dependency analysis (CDA) of graph transformation has been shown to be a versatile foundation for understanding interactions in many software engineering domains, including software analysis and design, model-driven engineering, and testing. In this paper, we propose a novel static CDA technique that is multi-granular in the sense that it can detect all conflicts and dependencies on multiple granularity levels. Specifically, we provide an efficient algorithm suite for computing binary, coarse-grained, and fine-grained conflicts and dependencies: Binary granularity indicates the presence or absence of conflicts and dependencies, coarse granularity focuses on root causes for conflicts and dependencies, and fine granularity shows each conflict and dependency in full detail. Doing so, we can address specific performance and usability requirements that we identified in a literature survey of CDA usage scenarios. In an experimental evaluation, our algorithm suite computes conflicts and dependencies rapidly. Finally, we present a user study, in which the participants found our coarse-grained results more understandable than the fine-grained ones reported in a state-of-the-art tool. Our overall contribution is twofold: (i) we significantly speed up the computation of fine-grained and binary CDA results and, (ii) complement them with coarse-grained ones, which offer usability benefits for numerous use cases.}, year = {2018}, pages = {716-727} } @article{MTMT:27351350, title = {Variability-based model transformation: formal foundation and application}, url = {https://m2.mtmt.hu/api/publication/27351350}, author = {Strueber, D and Rubin, J and Arendt, T and Chechik, M and Taentzer, G and Ploeger, J}, doi = {10.1007/s00165-017-0441-3}, journal-iso = {FORM ASP COMPUT}, journal = {FORMAL ASPECTS OF COMPUTING}, volume = {30}, unique-id = {27351350}, issn = {0934-5043}, year = {2018}, eissn = {1433-299X}, pages = {133-162} } @article{MTMT:3417124, title = {A feature-based classification of formal verification techniques for software models}, url = {https://m2.mtmt.hu/api/publication/3417124}, author = {Gabmeyer, S and Kaufmann, P and Seidl, Martina and Gogolla, M and Kappel, G}, doi = {10.1007/s10270-017-0591-z}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {2017}, unique-id = {3417124}, issn = {1619-1366}, year = {2017}, eissn = {1619-1374}, pages = {1-26} } @article{MTMT:26753411, title = {A systematic approach to constructing incremental topology control algorithms using graph transformation}, url = {https://m2.mtmt.hu/api/publication/26753411}, author = {Kluge, Roland and Stein, Michael and Varro, Gergely and Schuerr, Andy and Hollick, Matthias and Muehlhaeuser, Max}, doi = {10.1016/j.jvlc.2016.10.003}, journal-iso = {J VISUAL LANG COMPUT}, journal = {JOURNAL OF VISUAL LANGUAGES AND COMPUTING}, volume = {38}, unique-id = {26753411}, issn = {1045-926X}, year = {2017}, eissn = {1095-8533}, pages = {47-83} } @inproceedings{MTMT:27319803, title = {Translating target to source constraints in model-to-model transformations}, url = {https://m2.mtmt.hu/api/publication/27319803}, author = {Sanchez, Cuadrado Jesus and Guerra, Esther and de Lara, Juan and Clariso, Robert and Cabot, Jordi}, booktitle = {2017 ACM/IEEE 20TH INTERNATIONAL CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS (MODELS 2017)}, doi = {10.1109/MODELS.2017.12}, publisher = {Institute of Electrical and Electronics Engineers}, unique-id = {27319803}, year = {2017}, pages = {12-22} } @article{MTMT:27573158, title = {Henshin: A Usability-Focused Framework for EMF Model Transformation Development}, url = {https://m2.mtmt.hu/api/publication/27573158}, author = {Strueber, Daniel and Born, Kristopher and Gill, Kanwal Daud and Groner, Raffaela and Kehrer, Timo and Ohrndorf, Manuel and Tichy, Matthias}, doi = {10.1007/978-3-319-61470-0_12}, editor = {Plump, D}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {10373}, unique-id = {27573158}, issn = {0302-9743}, year = {2017}, pages = {196-208} } @article{MTMT:25471423, title = {Spider Graphs: a graph transformation system for spider diagrams}, url = {https://m2.mtmt.hu/api/publication/25471423}, author = {Bottoni, Paolo and Fish, Andrew and Presicce, Francesco Parisi}, doi = {10.1007/s10270-013-0381-1}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {14}, unique-id = {25471423}, issn = {1619-1366}, year = {2015}, eissn = {1619-1374}, pages = {1421-1453} } @article{MTMT:25471425, title = {A Methodology for Designing Dynamic Topology Control Algorithms via Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/25471425}, author = {Kluge, Roland and Varro, Gergely and Schuerr, Andy}, doi = {10.1007/978-3-319-21155-8_15}, journal-iso = {LECT NOTES ARTIF INT}, journal = {LECTURE NOTES IN ARTIFICIAL INTELLIGENCE}, volume = {9152}, unique-id = {25471425}, issn = {0302-9743}, year = {2015}, pages = {199-213} } @article{MTMT:2926326, title = {Open issues in model transformations for multimodal applications}, url = {https://m2.mtmt.hu/api/publication/2926326}, author = {Lengyel, László and Charaf, Hassan}, doi = {10.1007/s12193-015-0192-5}, journal-iso = {J MULTIMODAL USER IN}, journal = {JOURNAL ON MULTIMODAL USER INTERFACES}, volume = {9}, unique-id = {2926326}, issn = {1783-7677}, year = {2015}, eissn = {1783-8738}, pages = {377-385}, orcid-numbers = {Lengyel, László/0000-0002-5129-4198} } @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:24905399, title = {Verifying specifications with associated attributes in graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/24905399}, author = {Zhou, Yu and Huang, Yankai and Wei, Ou and Huang, Zhiqiu}, doi = {10.1007/s11704-015-4290-4}, journal-iso = {FRONT COMPUT SCI CHI}, journal = {FRONTIERS OF COMPUTER SCIENCE}, volume = {9}, unique-id = {24905399}, issn = {2095-2236}, year = {2015}, eissn = {2095-2228}, pages = {364-374} } @article{MTMT:24905342, title = {Design and Safety Analysis for System Architecture: A Breeze/ADL-based Approach}, url = {https://m2.mtmt.hu/api/publication/24905342}, author = {Chen, Luxi and Huang, Linpeng and Li, Chen and Wu, Linzhu and Luo, Weichao}, doi = {10.1109/COMPSAC.2014.35}, editor = {Chang, CK and Gao, Y and Hurson, A and Matskin, M and McMillin, B and Okabe, Y and Seceleanu, C and Yoshida, K}, journal-iso = {IEEE ANN INT COMPUT SOFTW APPL CONF}, journal = {IEEE ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC)}, volume = {2014}, unique-id = {24905342}, issn = {0730-3157}, year = {2014}, pages = {261-266} } @article{MTMT:24905341, title = {Specifying model changes with UMLchange to support security verification of potential evolution}, url = {https://m2.mtmt.hu/api/publication/24905341}, author = {Wenzel, S and Poggenpohl, D and Juerjens, J and Ochoa, M}, doi = {10.1016/j.csi.2013.12.011}, journal-iso = {COMPUT STAND INTER}, journal = {COMPUTER STANDARDS & INTERFACES}, volume = {36}, unique-id = {24905341}, issn = {0920-5489}, year = {2014}, eissn = {1872-7018}, pages = {776-791} } @article{MTMT:23929075, title = {Verification of graph grammars using a logical approach}, url = {https://m2.mtmt.hu/api/publication/23929075}, author = {Da, Costa S A and Ribeiro, L}, doi = {10.1016/j.scico.2010.02.006}, journal-iso = {SCI COMPUT PROGRAM}, journal = {SCIENCE OF COMPUTER PROGRAMMING}, volume = {77}, unique-id = {23929075}, issn = {0167-6423}, year = {2012}, eissn = {1872-7964}, pages = {480-504} } @inproceedings{MTMT:23946470, title = {Knowledge-based graph exploration analysis}, url = {https://m2.mtmt.hu/api/publication/23946470}, author = {Galvão, Ismênia and Zambon, Eduardo and Rensink, Arend and Wevers, Lesley and Aksit, Mehmet}, booktitle = {Applications of Graph Transformations with Industrial Relevance}, doi = {10.1007/978-3-642-34176-2_11}, unique-id = {23946470}, year = {2012}, pages = {105-120} } @article{MTMT:23929074, title = {Graph transformations for MDE, adaptation, and models at runtime}, url = {https://m2.mtmt.hu/api/publication/23929074}, author = {Giese, H and Lambers, L and Becker, B and Hildebrandt, S and Neumann, S and Vogel, T and Wätzoldt, S}, doi = {10.1007/978-3-642-30982-3_5}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {7320}, unique-id = {23929074}, issn = {0302-9743}, year = {2012}, eissn = {1611-3349}, pages = {137-191} } @article{MTMT:23929073, title = {Verification of graph programs}, url = {https://m2.mtmt.hu/api/publication/23929073}, author = {Poskitt, C M}, doi = {10.1007/978-3-642-33654-6_30}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {7562}, unique-id = {23929073}, issn = {0302-9743}, year = {2012}, eissn = {1611-3349}, pages = {420-422} } @article{MTMT:24002566, title = {Hoare-Style Verification of Graph Programs}, url = {https://m2.mtmt.hu/api/publication/24002566}, author = {Poskitt, CM and Plump, D}, doi = {10.3233/FI-2012-708}, journal-iso = {FUND INFOR}, journal = {FUNDAMENTA INFORMATICAE}, volume = {118}, unique-id = {24002566}, issn = {0169-2968}, year = {2012}, eissn = {1875-8681}, pages = {135-175} } @article{MTMT:23929916, title = {Correct transformation: From object-based graph grammars to PROMELA}, url = {https://m2.mtmt.hu/api/publication/23929916}, author = {Ribeiro, Leila and dos Santos, Osmar Marchi and Dotti, Fernando Luís and Foss, Luciana}, doi = {10.1016/j.scico.2011.03.010}, journal-iso = {SCI COMPUT PROGRAM}, journal = {SCIENCE OF COMPUTER PROGRAMMING}, volume = {77}, unique-id = {23929916}, issn = {0167-6423}, year = {2012}, eissn = {1872-7964}, pages = {214-246} } @article{MTMT:23929064, title = {Incremental Security Verification for Evolving UMLsec models}, url = {https://m2.mtmt.hu/api/publication/23929064}, author = {Jürjens, J and Marchal, L and Ochoa, M and Schmidt, H}, doi = {10.1007/978-3-642-21470-7_5}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {6698}, unique-id = {23929064}, issn = {0302-9743}, year = {2011}, eissn = {1611-3349}, pages = {52-68} } @article{MTMT:23929063, title = {Modelling Secure Systems Evolution: Abstract and Concrete Change Specifications}, url = {https://m2.mtmt.hu/api/publication/23929063}, author = {Jürjens, J and Ochoa, M and Schmidt, H and Marchal, L and Houmb, S and Islam, S}, doi = {10.1007/978-3-642-21455-4_15}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {6659}, unique-id = {23929063}, issn = {0302-9743}, year = {2011}, eissn = {1611-3349}, pages = {504-526} } @article{MTMT:23929510, title = {Formal analysis of service-oriented architectures. Analiza formalna architektury typu service-oriented}, url = {https://m2.mtmt.hu/api/publication/23929510}, author = {Rafe, V}, journal-iso = {PRZ ELEKTROTECHN}, journal = {PRZEGLAD ELEKTROTECHNICZNY}, volume = {87}, unique-id = {23929510}, issn = {0033-2097}, year = {2011}, eissn = {2449-9544}, pages = {310-313} } @mastersthesis{MTMT:24127231, title = {Compositional verification of model-level refactorings based on graph transformations}, url = {https://m2.mtmt.hu/api/publication/24127231}, author = {Bisztray, D A}, unique-id = {24127231}, year = {2010} } @mastersthesis{MTMT:23929056, title = {Relational approach of graph grammars}, url = {https://m2.mtmt.hu/api/publication/23929056}, author = {Cavalheiro, S A C}, unique-id = {23929056}, year = {2010} } @article{MTMT:23929506, title = {Formal analysis and verification of self-healing systems}, url = {https://m2.mtmt.hu/api/publication/23929506}, author = {Ehrig, H and Ermel, C and Runge, O and Bucchiarone, A and Pelliccione, P}, doi = {10.1007/978-3-642-12029-9_10}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {6013}, unique-id = {23929506}, issn = {0302-9743}, year = {2010}, eissn = {1611-3349}, pages = {139-153} } @misc{MTMT:24127242, title = {Formal analysis and verification of self-healing systems: Long version}, url = {https://m2.mtmt.hu/api/publication/24127242}, author = {Ehrig, H and Ermel, C and Runge, O and Bucchiarone, A and Pelliccione, P}, unique-id = {24127242}, year = {2010} } @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}, pages = {135-152} } @inproceedings{MTMT:23929057, title = {Lightweight Executability Analysis of Graph Transformation Rules}, url = {https://m2.mtmt.hu/api/publication/23929057}, author = {Planas, E and Cabot, J and de Nantes, I E M and Gómez, C and Guerra, E and de Lara, J}, booktitle = {IEEE Symposium on Visual Languages and Human-Centric Computing}, doi = {10.1109/VLHCC.2010.26}, unique-id = {23929057}, year = {2010}, pages = {127-130} } @CONFERENCE{MTMT:23929058, title = {Hoare logic for graph programs}, url = {https://m2.mtmt.hu/api/publication/23929058}, author = {Poskitt, C M and Plump, D}, booktitle = {THEORY Workshop at Verified Software: Theories, Tools and Experiments (VS-THEORY 2010)}, unique-id = {23929058}, year = {2010} } @inproceedings{MTMT:24002567, title = {A Hoare Calculus for Graph Programs}, url = {https://m2.mtmt.hu/api/publication/24002567}, author = {Poskitt, CM and Plump, D}, booktitle = {Proceeding of ICGT'10 Doctoral Symposium}, doi = {10.1007/978-3-642-15928-2_10}, unique-id = {24002567}, year = {2010}, pages = {139-154} } @misc{MTMT:23929055, title = {Towards a shape analysis for graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/23929055}, author = {Steenken, D and Wehrheim, H and Wonisch, D}, unique-id = {23929055}, year = {2010} } @article{MTMT:23929052, title = {Formal Verification of Graph Grammars using Mathematical Induction}, url = {https://m2.mtmt.hu/api/publication/23929052}, author = {da Costa, S A and Ribeiro, L}, doi = {10.1016/j.entcs.2009.05.044}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {240}, unique-id = {23929052}, issn = {1571-0661}, year = {2009}, pages = {43-60} } @inproceedings{MTMT:24130261, title = {An approach to automatic verification of stochastic graph transformations}, url = {https://m2.mtmt.hu/api/publication/24130261}, author = {Mir, Al Vand MZ and Hajee, M}, booktitle = {TENCON 2009, 2009 IEEE Region 10 Conference}, doi = {10.1109/TENCON.2009.5395989}, publisher = {Institute of Electrical and Electronics Engineers}, unique-id = {24130261}, year = {2009} } @article{MTMT:23929047, title = {Towards automated software model checking using graph transformationsystems and Bogor}, url = {https://m2.mtmt.hu/api/publication/23929047}, author = {Rafe, V and Rahmani, AT}, doi = {10.1631/jzus.A0820415}, journal-iso = {J ZHEJIANG UNIV-SCI A}, journal = {JOURNAL OF ZHEJIANG UNIVERSITY-SCIENCE A}, volume = {10}, unique-id = {23929047}, issn = {1673-565X}, year = {2009}, eissn = {1862-1775}, pages = {1093-1105} } @article{MTMT:24135026, title = {Towards automated verification of layered graph transformation specifications}, url = {https://m2.mtmt.hu/api/publication/24135026}, author = {Rafe, V and Rahmani, AT and Baresi, L and Spoletini, P}, doi = {10.1049/iet-sen.2008.0059}, journal-iso = {IET SOFTW}, journal = {IET SOFTWARE}, volume = {3}, unique-id = {24135026}, issn = {1751-8806}, year = {2009}, eissn = {1751-8814}, pages = {276-291} } @article{MTMT:23929907, title = {A NOVEL APPROACH TO VERIFY GRAPH SCHEMA-BASED SOFTWARE SYSTEMS}, url = {https://m2.mtmt.hu/api/publication/23929907}, author = {RAFE, Vahid and RAHMANI, Adel T}, doi = {10.1142/S0218194009004398}, journal-iso = {INT J SOFTW ENG KNOW}, journal = {INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING}, volume = {19}, unique-id = {23929907}, issn = {0218-1940}, year = {2009}, eissn = {1793-6403}, pages = {857-870} } @mastersthesis{MTMT:23929600, title = {Abstraction and Abstraction Refinement in the Verification of Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/23929600}, author = {V, Kozyura}, unique-id = {23929600}, year = {2009} } @article{MTMT:21490652, title = {An Efficient Solution for Model Checking Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/21490652}, author = {Baresi, L and Rafe, V and Rahmani, AT and Spoletini, P}, doi = {10.1016/j.entcs.2008.04.071}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {213}, unique-id = {21490652}, issn = {1571-0661}, year = {2008}, pages = {3-21} } @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} } @inproceedings{MTMT:21489696, title = {AGTIVE 2007 Graph Transformation Tool Contest}, url = {https://m2.mtmt.hu/api/publication/21489696}, author = {Rensink, A and Taentzer, G}, booktitle = {3rd International Symposium on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2007}, doi = {10.1007/978-3-540-89020-1-33}, unique-id = {21489696}, year = {2008}, pages = {487-492} } @inproceedings{MTMT:23929067, title = {Graph-Based Tools: The Contest}, url = {https://m2.mtmt.hu/api/publication/23929067}, author = {Rensink, A and Van, Gorp P}, booktitle = {Graph Transformations}, doi = {10.1007/978-3-540-87405-8_33}, unique-id = {23929067}, year = {2008}, pages = {463-466} } @article{MTMT:23929032, title = {Towards Model-Driven Unit Testing}, url = {https://m2.mtmt.hu/api/publication/23929032}, author = {Engels, G and Guldali, B and Lohmann, M}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4364}, unique-id = {23929032}, issn = {0302-9743}, year = {2007}, eissn = {1611-3349}, pages = {182} } @article{MTMT:23929028, title = {Verification of Random Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/23929028}, author = {Kozioura, V}, doi = {10.1016/j.entcs.2007.04.017}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {175}, unique-id = {23929028}, issn = {1571-0661}, year = {2007}, pages = {63-72} } @article{MTMT:21490168, title = {Constraint-based Model Transformation: Tracing the Preservation of Semantic Properties}, url = {https://m2.mtmt.hu/api/publication/21490168}, author = {Triebsees, T}, journal-iso = {JOURNAL OF SOFTWARE}, journal = {JOURNAL OF SOFTWARE}, volume = {2}, unique-id = {21490168}, issn = {1796-217X}, year = {2007}, pages = {19-29} } @CONFERENCE{MTMT:23929031, title = {Effective verification of systems with a dynamic number of components}, url = {https://m2.mtmt.hu/api/publication/23929031}, author = {Vaeková, P and Moravec, P and Cerná, I and Zimmerova, B}, booktitle = {2007 Conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering}, doi = {10.1145/1292316.1292317}, unique-id = {23929031}, year = {2007}, pages = {3-13} } @inproceedings{MTMT:23929033, title = {Reflecting Creation and Destruction of Instances in CBSs Modelling and Verification}, url = {https://m2.mtmt.hu/api/publication/23929033}, author = {Zimmerova, B and Varekova, P}, booktitle = {MEMICS proceedings}, unique-id = {23929033}, year = {2007}, pages = {257-264} } @inproceedings{MTMT:23929038, title = {Addressing Unbounded Parallelism in Verification of Software Components}, url = {https://m2.mtmt.hu/api/publication/23929038}, author = {Adamek, J}, booktitle = {SNPD-SAWN ?06: Proceedings of the Seventh ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing}, doi = {10.1109/SNPD-SAWN.2006.15}, unique-id = {23929038}, year = {2006}, pages = {49-56} } @article{MTMT:23929050, title = {On the use of alloy to analyze graph transformation systems}, url = {https://m2.mtmt.hu/api/publication/23929050}, author = {Baresi, L and Spoletini, P}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4178}, unique-id = {23929050}, issn = {0302-9743}, year = {2006}, eissn = {1611-3349}, pages = {306-320} } @article{MTMT:2612533, title = {Style-based modeling and refinement of service-oriented architectures: A graph transformation-base approach}, url = {https://m2.mtmt.hu/api/publication/2612533}, author = {Baresi, L and Heckel, R and Thöne, S and Varró, Dániel}, doi = {10.1007/s10270-006-0001-4}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {5}, unique-id = {2612533}, issn = {1619-1366}, abstract = {Service-oriented architectures (SOA) provide a flexible and dynamic platform for implementing business solutions. In this paper, we address the modeling of such architectures by refining business-oriented architectures, which abstract from technology aspects, into service-oriented ones, focusing on the ability of dynamic reconfiguration (binding to new services at run-time) typical for SOA. The refinement is based on conceptual models of the platforms involved as architectural styles, formalized by graph transformation systems. Based on a refinement relation between abstract and platform-specific styles we investigate how to realize business-specific scenarios on the SOA platform by automatically deriving refined, SOA-specific reconfiguration scenarios. ? Springer-Verlag 2006.}, year = {2006}, eissn = {1619-1374}, pages = {187-207}, orcid-numbers = {Varró, Dániel/0000-0002-8790-252X} } @CONFERENCE{MTMT:23929037, title = {Analysis of Dynamic Communicating Systems by Hierarchical Abstraction}, url = {https://m2.mtmt.hu/api/publication/23929037}, author = {Bauer, J and Wilhelm, R}, booktitle = {Software Verification: Infinite-State Model Checking and Static Program Analysis}, unique-id = {23929037}, year = {2006} } @article{MTMT:23929877, title = {Verifying Object-based Graph Grammars}, url = {https://m2.mtmt.hu/api/publication/23929877}, author = {Dotti, F L and Ribeiro, L and Santos, O M and Pasini, F}, doi = {10.1007/s10270-006-0014-z}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {5}, unique-id = {23929877}, issn = {1619-1366}, year = {2006}, eissn = {1619-1374}, pages = {289-311} } @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 = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {4178}, unique-id = {23929310}, issn = {0302-9743}, year = {2006}, eissn = {1611-3349}, pages = {445-460} } @inproceedings{MTMT:24127246, title = {Modeling the Static Aspects of Trust for Open MAS}, url = {https://m2.mtmt.hu/api/publication/24127246}, author = {Kaffille, Sven and Wirtz, Guido}, booktitle = {Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation (CIMCA 2006)}, doi = {10.1109/CIMCA.2006.150}, unique-id = {24127246}, year = {2006}, pages = {186} } @misc{MTMT:23929036, title = {Integrated Visual Specification of Structural and Temporal Properties}, url = {https://m2.mtmt.hu/api/publication/23929036}, author = {Klein, F and Giese, H}, unique-id = {23929036}, year = {2006} } @article{MTMT:23929034, title = {Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/23929034}, author = {Konig, B and Kozioura, V}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {3920}, unique-id = {23929034}, issn = {0302-9743}, year = {2006}, eissn = {1611-3349}, pages = {197} } @article{MTMT:2612531, title = {Applying a model transformation taxonomy to graph transformation technology}, url = {https://m2.mtmt.hu/api/publication/2612531}, author = {Mens, T and Van, Gorp P and Varró, Dániel and Karsai, G}, doi = {10.1016/j.entcs.2005.10.022}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {152}, unique-id = {2612531}, issn = {1571-0661}, abstract = {A taxonomy of model transformations was introduced in [T. Mens, P.V. Gorp, A taxonomy of model transformation, in: Proc. Int'l Workshop on Graph and Model Transformation (GraMoT 2005), Electronic Notes in Computer Science (2005)]. Among others, such a taxonomy can help developers in deciding which language, forma lism, tool or mechanism is best suited to carry out a particular model transformation activity. In this paper we apply the taxonomy to the technique of graph transformation, and we exemplify it by referring to four representative graph transformation tools. As a byproduct of our analysis, we discuss how well each of the considered tools carry out the activity of model transformation. ? 2006 Elsevier B.V. All rights reserved.}, year = {2006}, pages = {143-159}, orcid-numbers = {Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:23929035, title = {Abstract Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/23929035}, author = {Rensink, A and Distefano, D}, doi = {10.1016/j.entcs.2006.01.022}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {157}, unique-id = {23929035}, issn = {1571-0661}, year = {2006}, pages = {39-59} } @mastersthesis{MTMT:23929040, title = {Kompositionale Softwareverifikation mechatronischer Systeme}, url = {https://m2.mtmt.hu/api/publication/23929040}, author = {Schilling, D}, unique-id = {23929040}, year = {2006} } @article{MTMT:23929051, title = {Verifying fault-tolerant distributed systems using Object-Based GraphGrammars}, url = {https://m2.mtmt.hu/api/publication/23929051}, author = {Dotti, FL and Mendizabal, OM and dos, Santos OM}, doi = {10.1007/11572329_9}, journal-iso = {LECT NOTES COMPUT SC}, journal = {LECTURE NOTES IN COMPUTER SCIENCE}, volume = {3747}, unique-id = {23929051}, issn = {0302-9743}, year = {2005}, eissn = {1611-3349}, pages = {80-100} } @article{MTMT:21490598, title = {Augur - A Tool for the Analysis of Graph Transformation Systems}, url = {https://m2.mtmt.hu/api/publication/21490598}, author = {König, Barbara and Kozioura, Vitali}, journal-iso = {BULL EATCS}, journal = {BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE}, volume = {87}, unique-id = {21490598}, issn = {0252-9742}, year = {2005}, pages = {126-137} } @article{MTMT:23929878, title = {Time and Space Issues in the Generation of Graph Transition Systems}, url = {https://m2.mtmt.hu/api/publication/23929878}, author = {Rensink, Arend}, doi = {10.1016/j.entcs.2004.12.036}, journal-iso = {ELECTR NOTES COMPUT SCI}, journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE}, volume = {127}, unique-id = {23929878}, issn = {1571-0661}, year = {2005}, pages = {127-139} } @mastersthesis{MTMT:23928976, title = {Dynamic Software Architectures}, url = {https://m2.mtmt.hu/api/publication/23928976}, author = {Thöne, S}, unique-id = {23928976}, year = {2005} } @CONFERENCE{MTMT:23929042, title = {Extending Fault Tolerance Patterns by Visual Degradation Rules}, url = {https://m2.mtmt.hu/api/publication/23929042}, author = {Tichy, M and Giese, H}, booktitle = {Workshop on Visual Modeling for Software Intensive Systems (VMSIS) at the the IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC'05)}, unique-id = {23929042}, year = {2005}, pages = {67-74} } @CONFERENCE{MTMT:23929045, title = {A Taxonomy of Model Transformation and its Application to Graph Transformation}, url = {https://m2.mtmt.hu/api/publication/23929045}, author = {Mens, T and Van, Gorp P}, booktitle = {Proceedings of the International Workshop on Graph and Model Transformation}, unique-id = {23929045}, year = {2004}, pages = {7-23} }