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