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ániel Varró

Research output: Contribution to journalArticle

13 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
Pages (from-to)357-392
Number of pages36
JournalSoftware and Systems Modeling
Volume16
Issue number2
DOIs
Publication statusPublished - May 1 2017

Keywords

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

ASJC Scopus subject areas

  • Software
  • Modelling and Simulation

Fingerprint Dive into the research topics of 'Formal validation of domain-specific languages with derived features and well-formedness constraints'. Together they form a unique fingerprint.

  • Cite this