Formal validation of domain-specific languages with derived features and well-formedness constraints. Semeráth, O., Ágnes, B., Horváth, Á., Szatmári, Z., & Varró, D. SOFTWARE AND SYSTEMS MODELING, 16:357-392, 2017. ![Formal validation of domain-specific languages with derived features and well-formedness constraints [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex 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.
@article{MTMT:3018014,
title = {Formal validation of domain-specific languages with derived features and well-formedness constraints},
url = {https://m2.mtmt.hu/api/publication/3018014},
author = {Semeráth, Oszkár and Ágnes, Barta and Horváth, Ákos and Szatmári, Zoltán and Varró, Dániel},
doi = {10.1007/s10270-015-0485-x},
journal-iso = {SOFTW SYST MODEL},
journal = {SOFTWARE AND SYSTEMS MODELING},
volume = {16},
unique-id = {3018014},
issn = {1619-1366},
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.},
year = {2017},
eissn = {1619-1374},
pages = {357-392},
orcid-numbers = {Varró, Dániel/0000-0002-8790-252X}
}
Downloads: 0
{"_id":"yEDSNzyMz8qbKrNAX","bibbaseid":"semerth-gnes-horvth-szatmri-varr-formalvalidationofdomainspecificlanguageswithderivedfeaturesandwellformednessconstraints-2017","author_short":["Semeráth, O.","Ágnes, B.","Horváth, Á.","Szatmári, Z.","Varró, D."],"bibdata":{"bibtype":"article","type":"article","title":"Formal validation of domain-specific languages with derived features and well-formedness constraints","url":"https://m2.mtmt.hu/api/publication/3018014","author":[{"propositions":[],"lastnames":["Semeráth"],"firstnames":["Oszkár"],"suffixes":[]},{"propositions":[],"lastnames":["Ágnes"],"firstnames":["Barta"],"suffixes":[]},{"propositions":[],"lastnames":["Horváth"],"firstnames":["Ákos"],"suffixes":[]},{"propositions":[],"lastnames":["Szatmári"],"firstnames":["Zoltán"],"suffixes":[]},{"propositions":[],"lastnames":["Varró"],"firstnames":["Dániel"],"suffixes":[]}],"doi":"10.1007/s10270-015-0485-x","journal-iso":"SOFTW SYST MODEL","journal":"SOFTWARE AND SYSTEMS MODELING","volume":"16","unique-id":"3018014","issn":"1619-1366","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.","year":"2017","eissn":"1619-1374","pages":"357-392","orcid-numbers":"Varró, Dániel/0000-0002-8790-252X","bibtex":"@article{MTMT:3018014,\n\ttitle = {Formal validation of domain-specific languages with derived features and well-formedness constraints},\n\turl = {https://m2.mtmt.hu/api/publication/3018014},\n\tauthor = {Semeráth, Oszkár and Ágnes, Barta and Horváth, Ákos and Szatmári, Zoltán and Varró, Dániel},\n\tdoi = {10.1007/s10270-015-0485-x},\n\tjournal-iso = {SOFTW SYST MODEL},\n\tjournal = {SOFTWARE AND SYSTEMS MODELING},\n\tvolume = {16},\n\tunique-id = {3018014},\n\tissn = {1619-1366},\n\tabstract = {Despite the wide range of existing tool support, constructing \n\t\ta design environment for a complex domain-specific language \n\t\t(DSL) is still a tedious task as the large number of derived \n\t\tfeatures and well-formedness constraints complementing the \n\t\tdomain metamodel necessitate special handling. Such derived \n\t\tfeatures and constraints are frequently defined by \n\t\tdeclarative techniques (such graph patterns or OCL \n\t\tinvariants). However, for complex domains, derived features \n\t\tand constraints can easily be formalized incorrectly \n\t\tresulting in inconsistent, incomplete or ambiguous DSL \n\t\tspecifications. To detect such issues, we propose an \n\t\tautomated mapping of EMF metamodels enriched with derived \n\t\tfeatures and well-formedness constraints captured as graph \n\t\tqueries in EMF-IncQuery or (a subset of) OCL invariants into \n\t\tan effectively propositional fragment of first-order logic \n\t\twhich can be efficiently analyzed by back-end reasoners. On \n\t\tthe conceptual level, the main added value of our encoding is \n\t\t(1) to transform graph patterns of the EMF-IncQuery framework \n\t\tinto FOL and (2) to introduce approximations for complex \n\t\tlanguage features (e.g., transitive closure or \n\t\tmultiplicities) which are not expressible in FOL. On the \n\t\tpractical level, we identify and address relevant challenges \n\t\tand scenarios for systematically validating DSL \n\t\tspecifications. Our approach is supported by a tool, and it \n\t\twill be illustrated on analyzing a DSL in the avionics \n\t\tdomain. We also present initial performance experiments for \n\t\tthe validation using Z3 and Alloy as back-end reasoners.},\n\tyear = {2017},\n\teissn = {1619-1374},\n\tpages = {357-392},\n\torcid-numbers = {Varró, Dániel/0000-0002-8790-252X}\n}\n\n","author_short":["Semeráth, O.","Ágnes, B.","Horváth, Á.","Szatmári, Z.","Varró, D."],"key":"MTMT:3018014","id":"MTMT:3018014","bibbaseid":"semerth-gnes-horvth-szatmri-varr-formalvalidationofdomainspecificlanguageswithderivedfeaturesandwellformednessconstraints-2017","role":"author","urls":{"Paper":"https://m2.mtmt.hu/api/publication/3018014"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"https://oszkarsemerath.github.io/publications.bib","dataSources":["Zeqdy2BRdLE2kdGkL"],"keywords":[],"search_terms":["formal","validation","domain","specific","languages","derived","features","well","formedness","constraints","semeráth","ágnes","horváth","szatmári","varró"],"title":"Formal validation of domain-specific languages with derived features and well-formedness constraints","year":2017}