Formal validation of domain-specific languages with derived features and well-formedness constraints

Oszkár Semeráth, Ágnes Barta, Ákos Horváth, Zoltán Szatmári, D. Varró

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

Despite the wide range of existing 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. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous 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 or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.

Original languageEnglish
JournalSoftware and Systems Modeling
DOIs
Publication statusAccepted/In press - Jul 30 2015

Fingerprint

Domain-specific Languages
Specification languages
Electromagnetic Fields
Electric potential
Metamodel
Graph in graph theory
Avionics
Specification
Transitive Closure
Invariant
Tool Support
First-order Logic
Ambiguous
Inconsistent
Multiplicity
Fragment
Encoding
Query
Transform
Scenarios

Keywords

  • Derived features
  • Language validation
  • Model queries
  • Partial snapshots
  • SMT solvers

ASJC Scopus subject areas

  • Software
  • Modelling and Simulation

Cite this

Formal validation of domain-specific languages with derived features and well-formedness constraints. / Semeráth, Oszkár; Barta, Ágnes; Horváth, Ákos; Szatmári, Zoltán; Varró, D.

In: Software and Systems Modeling, 30.07.2015.

Research output: Contribution to journalArticle

@article{800706d221954b45aa3a38fdfb65f59a,
title = "Formal validation of domain-specific languages with derived features and well-formedness constraints",
abstract = "Despite the wide range of existing 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. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous 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 or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.",
keywords = "Derived features, Language validation, Model queries, Partial snapshots, SMT solvers",
author = "Oszk{\'a}r Semer{\'a}th and {\'A}gnes Barta and {\'A}kos Horv{\'a}th and Zolt{\'a}n Szatm{\'a}ri and D. Varr{\'o}",
year = "2015",
month = "7",
day = "30",
doi = "10.1007/s10270-015-0485-x",
language = "English",
journal = "Software and Systems Modeling",
issn = "1619-1366",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Formal validation of domain-specific languages with derived features and well-formedness constraints

AU - Semeráth, Oszkár

AU - Barta, Ágnes

AU - Horváth, Ákos

AU - Szatmári, Zoltán

AU - Varró, D.

PY - 2015/7/30

Y1 - 2015/7/30

N2 - Despite the wide range of existing 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. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous 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 or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.

AB - Despite the wide range of existing 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. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous 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 or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.

KW - Derived features

KW - Language validation

KW - Model queries

KW - Partial snapshots

KW - SMT solvers

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

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

U2 - 10.1007/s10270-015-0485-x

DO - 10.1007/s10270-015-0485-x

M3 - Article

JO - Software and Systems Modeling

JF - Software and Systems Modeling

SN - 1619-1366

ER -