Validation of Derived Features and Well-Formedness Constraints in DSLs by mapping graph queries to an SMT-solver

Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Recently, we proposed to use incremental model queries as provided by the EMF-IncQuery framework to uniformly specify derived features and well-formedness constraints and automatically refresh their result set upon model changes. However, for complex domains such as avionics or automotive, derived features and constraints can be formalized incorrectly resulting in incomplete, ambiguous or inconsistent DSL specifications. To detect such issues, we propose an automated mapping of EMF metamodels enriched with derived features and well-formedness constraints captured in EMF-IncQuery into the Z3 SMT-solver. Our approach will be illustrated on analyzing DSL being developed for the avionics domain.
http://incquery.net/publications/dslvalid