REAL

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

Semeráth, Oszkár and Barta, Ágnes and Horváth, Ákos and Szatmári, Zoltán and Varró, Dániel (2015) Formal validation of domain-specific languages with derived features and well-formedness constraints. SOFTWARE AND SYSTEMS MODELING. pp. 1-37. ISSN 1619-1366

[img]
Preview
Text
sosym_dslvalidation_14_u.pdf

Download (4MB) | Preview

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.

Item Type: Article
Subjects: Q Science / természettudomány > QA Mathematics / matematika > QA75 Electronic computers. Computer science / számítástechnika, számítógéptudomány
SWORD Depositor: MTMT SWORD
Depositing User: MTMT SWORD
Date Deposited: 15 Feb 2017 09:07
Last Modified: 15 Feb 2017 09:07
URI: http://real.mtak.hu/id/eprint/48989

Actions (login required)

Edit Item Edit Item