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]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