Validation of Derived Features and Well-Formedness Constraints in DSLs

Publication Reference

Title: Validation of Derived Features and Well-Formedness Constraints in DSLs
Authors: Oszkár Semeráth, Ákos Horváth, Dániel Varró
Conference: MODELS 2013 - ACM/IEEE 16th International Conference on Model Driven Engineering Languages and Systems
Publisher: Springer
Series: Lecture Notes in Computer Science, vol 8107
Year: 2013
Pages: 537-553
DOI: https://doi.org/10.1007/978-3-642-41533-3_33

Extended Version:
Journal: Software and Systems Modeling
Volume: 16, Issue 2
Year: 2017
Pages: 357-392
DOI: https://doi.org/10.1007/s10270-015-0485-x

Abstract

As model-driven tools are frequently used in critical systems design, those tools should be validated with the same level of scrutiny as the underlying system tools as part of a software tool qualification process. This paper proposes an automated mapping from high-level DSL specifications to the Z3 SMT-solver for validation. The approach assumes that DSL tools are specified by their respective EMF metamodels extended with derived features and well-formedness constraints captured by graph queries within the EMF-IncQuery framework. The validation process gradually investigates derived features and well-formedness constraints to pinpoint inconsistency, ambiguity or incompleteness issues.

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)

---

Tags: emf-incquery, dsl-validation, z3-smt-solver, derived-features, well-formedness-constraints, model-validation, software-tool-qualification, metamodel-validation, graph-queries, formal-validation, publication