@inproceedings {csduml2003,
	title = {Automated Formal Verification of Model Transformations},
	booktitle = {CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML{\textquoteright}03 Workshop},
	series = {Technical Report},
	number = {TUM-I0323},
	year = {2003},
	month = {September},
	pages = {63{\textendash}78},
	publisher = {Technische Universit{\"a}t M{\"u}nchen},
	organization = {Technische Universit{\"a}t M{\"u}nchen},
	abstract = {When designing safety critical applications in UML, the system models are frequently projected into various mathematical domains (such as Petri nets, transition systems, process algebras, etc.) to carry out a formal analysis of the system under design by \emph{automatic model transformations}. Automation surely increases the quality of such transformations as errors manually implanted into transformation programs during implementation are eliminated; however, conceptual flaws in transformation design still remain undetected. In this paper, we present a model-level, modeling language independent and highly automated technique to formally verify by model checking that a model transformation from an arbitrary well-formed model instance of the source modeling language into its target equivalent preserves (language specific) dynamic consistency properties. We demonstrate the feasibility of our approach on a complex mathematical model transformation from UML statecharts to Petri nets.},
	url = {http://www.inf.mit.bme.hu/FTSRG/Publications/varro/2003/csduml2003_vp.pdf},
	author = {D{\'a}niel Varr{\'o} and Andr{\'a}s Pataricza},
	editor = {Jan J{\"u}rjens and Bernhard Rumpe and Robert France and Eduardo B. Fernandez}
}
