@article{MTMT:2612540,
	title = {Automated Formal Verification of Visual Modeling Languages by Model Checking},
	url = {https://m2.mtmt.hu/api/publication/2612540},
	author = {Varró, Dániel},
	doi = {10.1007/s10270-003-0050-x},
	journal-iso = {SOFTW SYST MODEL},
	journal = {SOFTWARE AND SYSTEMS MODELING},
	volume = {3},
	unique-id = {2612540},
	issn = {1619-1366},
	abstract = {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.},
	year = {2004},
	eissn = {1619-1374},
	pages = {85-113},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:1635269,
	title = {Graph transformation with time},
	url = {https://m2.mtmt.hu/api/publication/1635269},
	author = {Varró-Gyapay, Szilvia and Varró, Dániel and Heckel, R},
	journal-iso = {FUND INFOR},
	journal = {FUNDAMENTA INFORMATICAE},
	volume = {58},
	unique-id = {1635269},
	issn = {0169-2968},
	abstract = {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.},
	year = {2003},
	eissn = {1875-8681},
	pages = {1-22},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:2612510,
	title = {CheckVML: A tool for model checking visual modeling languages},
	url = {https://m2.mtmt.hu/api/publication/2612510},
	author = {Schmidt, A and Varró, Dániel},
	doi = {10.1007/b14063},
	journal-iso = {LNCS},
	journal = {LECTURE NOTES IN COMPUTER SCIENCE},
	volume = {2863},
	unique-id = {2612510},
	issn = {0302-9743},
	abstract = {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.},
	year = {2003},
	eissn = {1611-3349},
	pages = {92-95},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:1635278,
	title = {Towards symbolic analysis of visual modeling languages},
	url = {https://m2.mtmt.hu/api/publication/1635278},
	author = {Varró, Dániel},
	doi = {10.1016/S1571-0661(04)80611-X},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {72},
	unique-id = {1635278},
	issn = {1571-0661},
	abstract = {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.},
	year = {2003},
	pages = {51-64},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:2612519,
	title = {An open visualization framework for metamodel-based modeling languages},
	url = {https://m2.mtmt.hu/api/publication/2612519},
	author = {Domokos, P and Varró, Dániel},
	doi = {10.1016/S1571-0661(05)80531-6},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {72},
	unique-id = {2612519},
	issn = {1571-0661},
	abstract = {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.},
	year = {2002},
	pages = {69-78},
	orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}