Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver

Oszkár Semeráth, Ákos Horváth, D. Varró

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, 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 as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages538-554
Number of pages17
Volume8107 LNCS
DOIs
Publication statusPublished - 2013
Event16th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2013 - Miami, FL, United States
Duration: Sep 29 2013Oct 4 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8107 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other16th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2013
CountryUnited States
CityMiami, FL
Period9/29/1310/4/13

Fingerprint

DSL
Surface mount technology
Domain-specific Languages
Query
Electromagnetic Fields
Electric potential
Graph in graph theory
Metamodel
Specification languages
Avionics
Transitive Closure
Tool Support
First-order Logic
Ambiguous
Inconsistent
Fragment
Specification
Model
Range of data

Keywords

  • model queries
  • model validation
  • SMT-solvers

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Semeráth, O., Horváth, Á., & Varró, D. (2013). Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8107 LNCS, pp. 538-554). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8107 LNCS). https://doi.org/10.1007/978-3-642-41533-3_33

Validation of derived features and well-formedness constraints in DSLs : By mapping graph queries to an SMT-solver. / Semeráth, Oszkár; Horváth, Ákos; Varró, D.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8107 LNCS 2013. p. 538-554 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8107 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semeráth, O, Horváth, Á & Varró, D 2013, Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 8107 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8107 LNCS, pp. 538-554, 16th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2013, Miami, FL, United States, 9/29/13. https://doi.org/10.1007/978-3-642-41533-3_33
Semeráth O, Horváth Á, Varró D. Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8107 LNCS. 2013. p. 538-554. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-41533-3_33
Semeráth, Oszkár ; Horváth, Ákos ; Varró, D. / Validation of derived features and well-formedness constraints in DSLs : By mapping graph queries to an SMT-solver. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8107 LNCS 2013. pp. 538-554 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{418257d01ef04afd84bc5881a97328cc,
title = "Validation of derived features and well-formedness constraints in DSLs: By mapping graph queries to an SMT-solver",
abstract = "Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, 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 as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.",
keywords = "model queries, model validation, SMT-solvers",
author = "Oszk{\'a}r Semer{\'a}th and {\'A}kos Horv{\'a}th and D. Varr{\'o}",
year = "2013",
doi = "10.1007/978-3-642-41533-3_33",
language = "English",
isbn = "9783642415326",
volume = "8107 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "538--554",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Validation of derived features and well-formedness constraints in DSLs

T2 - By mapping graph queries to an SMT-solver

AU - Semeráth, Oszkár

AU - Horváth, Ákos

AU - Varró, D.

PY - 2013

Y1 - 2013

N2 - Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, 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 as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.

AB - Despite the wide range of existing generative tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Incremental model queries as provided by the EMF-IncQuery framework can (i) uniformly specify derived features and well-formedness constraints and (ii) automatically refresh their result set upon model changes. However, for complex domains, 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 as graph queries in EMF-IncQuery into an effectively propositional fragment of first-order logic which can be efficiently analyzed by the Z3 SMT-solver. Moreover, overapproximations are proposed for complex query features (like transitive closure and recursive calls). Our approach will be illustrated on analyzing a DSL being developed for the avionics domain.

KW - model queries

KW - model validation

KW - SMT-solvers

UR - http://www.scopus.com/inward/record.url?scp=84886860124&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84886860124&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-41533-3_33

DO - 10.1007/978-3-642-41533-3_33

M3 - Conference contribution

AN - SCOPUS:84886860124

SN - 9783642415326

VL - 8107 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 538

EP - 554

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -