TY - JOUR AU - Varró, Dániel TI - Automated Formal Verification of Visual Modeling Languages by Model Checking JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 3 PY - 2004 IS - 2 SP - 85 EP - 113 PG - 29 SN - 1619-1366 DO - 10.1007/s10270-003-0050-x UR - https://m2.mtmt.hu/api/publication/2612540 ID - 2612540 AB - Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level. LA - English DB - MTMT ER - TY - JOUR AU - Varró-Gyapay, Szilvia AU - Varró, Dániel AU - Heckel, R TI - Graph transformation with time JF - FUNDAMENTA INFORMATICAE J2 - FUND INFOR VL - 58 PY - 2003 IS - 1 SP - 1 EP - 22 PG - 22 SN - 0169-2968 UR - https://m2.mtmt.hu/api/publication/1635269 ID - 1635269 AB - Following TER nets, an approach to the modeling of time in high-level Petri nets, we propose a model of time within (attributed) graph transformation systems where logical clocks are represented as distinguished node attributes. Corresponding axioms for the time model in TER nets are generalized to graph transformation systems and semantic variations are discussed. They are summarized by a general theorem ensuring the consistency of temporal order and casual dependencies. The resulting notions of typed graph transformation with time specialize the algebraic double-pushout (DPO) approach to typed graph transformation. In particular, the concurrency theory of the DPO approach can be used in the transfer of the basic theory of TER nets. LA - English DB - MTMT ER - TY - JOUR AU - Schmidt, A AU - Varró, Dániel TI - CheckVML: A tool for model checking visual modeling languages JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 2863 PY - 2003 SP - 92 EP - 95 PG - 4 SN - 0302-9743 DO - 10.1007/b14063 UR - https://m2.mtmt.hu/api/publication/2612510 ID - 2612510 AB - In the paper, we present a tool for model checking dynamic consistency properties in arbitrary well-formed instance models of any modeling language defined visually by metamodeling and graph transformation techniques. Our tool first translates such high-level specifications into a tool independent abstract representation of transition systems defined by a corresponding metamodel. From this intermediate representation the input language of the back-end model checker tool (i.e., SPIN in our case) is generated automatically. LA - English DB - MTMT ER - TY - JOUR AU - Varró, Dániel TI - Towards symbolic analysis of visual modeling languages JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 72 PY - 2003 IS - 3 SP - 51 EP - 64 PG - 14 SN - 1571-0661 DO - 10.1016/S1571-0661(04)80611-X UR - https://m2.mtmt.hu/api/publication/1635278 ID - 1635278 N1 - Cited By :16 Export Date: 20 May 2022 Correspondence Address: Varro, D.; Department of Measurement and Information Systems, Magyar tudosok körutja 2, H-1117, Budapest, Hungary; email: varro@mit.bme.hu AB - Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture the operational semantics of modeling languages based on metamodeling techniques as demonstrated by benchmark applications focusing on the formal treatment of the Unified Modeling Language (UML). In the paper, we enable model checking-based symbolic verification for such modeling languages by providing a meta-level transformation of well-formed model instances into SAL specifications. We also discuss several optimizations in the translation process that makes our approach efficient and independent of the SAL framework. ?2003 Published by Elsevier Science B. V. LA - English DB - MTMT ER - TY - JOUR AU - Domokos, P AU - Varró, Dániel TI - An open visualization framework for metamodel-based modeling languages JF - ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE J2 - ELECTR NOTES COMPUT SCI VL - 72 PY - 2002 IS - 2 SP - 69 EP - 78 PG - 10 SN - 1571-0661 DO - 10.1016/S1571-0661(05)80531-6 UR - https://m2.mtmt.hu/api/publication/2612519 ID - 2612519 N1 - Cited By :9 Export Date: 20 May 2022 Correspondence Address: Domokos, P.; Department of Measurement and Information Systems Budapest University for Technology and Economics, Magyar tudosok korutja 2, H-1111, Budapest, Hungary; email: pdomokos@mit.bme.hu AB - In the paper, we propose an automated, SVG-based visualization framework for modeling languages defined by metamodeling techniques. Our framework combines XML standards with existing graph transformation and graph drawing technologies in order to provide an open, tool-independent architecture. LA - English DB - MTMT ER -