Skip to content

Validation of Derived Features and Well Formedness Constraints in DSLs

Jump to bottom
Anett Kiss edited this page Nov 2, 2015 · 5 revisions

######Tags: EMF-IncQuery publication

This page is created as to supplement the proposed paper Validation of Derived Features and Well-Formedness Constraints in DSLs by mapping graph queries to an SMT-solver by Oszkár Semeráth, Ákos Horváth and Dániel Varró

###Overview

As model-driven tools are frequently used in critical systems design to detect conceptual flaws of the system model early in the development process to decrease verification and validation (V&V) costs, those tools should be validated with the same level of scrutiny as the underlying system tools as part of a software tool qualification process issues in order to provide trust in their output. Therefore software tool qualification raises several challenges for building trusted DSL tools in a specific domain.

We aim to validate DSL tools by proposing an automated mapping from their high-level specification to the state-of-the-art Z3 SMT-solver. We assume that DSL tools are specified by their respective EMF metamodels extended with derived features and well-formedness constraints captured (and implemented) by graph queries within the EMF-IncQuery framework. We define a validation process, which gradually investigates derived features and well-formedness constraints to pinpoint inconsistency, ambiguity or incompleteness issues. Additionally, We identify constraints and derived features which can be mapped to effectively propositional logic formula, which are a decidable fragment of first order logic with effective reasoning support. Moreover, we provide several approximations for constraints which lie outside of this fragment to enable formal analysis of a practically relevant set of constraints.

The main innovation of our approach is to provide: a combined validation of metamodels, derived features and well-formedness constraints defined by an advanced graph query language (instead of OCL) using approximations to cover complex query features

###Additional material

Apart from the submitted paper for the ACM/IEEE 16th International Conference on Model Driven Engineering Languages and Systems, you can find two separate artifact uploaded to the current page. The DSL2SMT_TechReport describes how the actual mapping rules are defined between the DSL captured as a combination of EMF metamodel and derived features and well-formedness constraints specified by EMF-IncQuery graph patterns. The mapping is defined specifically for the Z3 SM solver. Additionally, in order to be able to reevaluate the case study presented in the submited paper the test case.zip contains all twelve generated SMT input files for the Z3 solver.

Executing the Case-Study

  • Install Z3 version on 4.1
  • Extract the test cases.zip
  • Execute the run.bat present in the topmost folder.
  • results will be generated to the out folder, while all input formulas are present in the in folder

Our own measurements were executed on Win 8 64 bit.

Attachment:

DSL2SMT_TechReport_v3.pdf

[test cases.zip](https://github.com/FTSRG/publication-pages/wiki/Validation/test cases.zip)

Clone this wiki locally