Verification of DSMLs using graph transformation
Zekai Demirezen, Marjan Mernik, Jeff Gray, Barrett R. Bryant · 2009
Domain-Specific Modeling Languages (DSMLs) enable domain experts to participate in software development tasks and to specify their own programs using domain abstractions. Many Model-Driven Engineering (MDE) platforms primarily concentrate on structural aspects of DSMLs and only provide techniques to define abstract and concrete syntax. Only a few platforms provide built-in support for specification of behavioral semantics and verification tasks. In this paper, we focus on how to specify the behavioral semantics of a DSML by a sequence of graph transformation rules. We also discuss how to transform a DSML specification into Alloy, a model checking tool. These transformations demonstrate that DSML models specified in a visual notation can be verified by means of existing model checking tools.