Generating Metamodel Instances Satisfying Coverage Criteria via SMT Solving

Hao Wu

2016

Abstract

One of the challenges for using metamodels in Model Driven Engineering is to automatically generate metamodel instances. Each instance should satisfy many constraints defined by a metamodel. Such instances can then be used for verifying or validating metamodels. Recent studies have already shown that this can be tackled by using SAT/SMT solvers. However, such instance generation does not take coverage criteria into account, and instances satisfying specified coverage criteria could be useful for testing model transformation. In this paper, we present an approach consisting of two techniques for coverage oriented metamodel instance generation. The first technique realises the standard coverage criteria defined for UML class diagrams, while the second technique focuses on generating instances satisfying graph-based criteria. With our approach, both kinds of criteria are translated to SMT formulas which are then investigated by an SMT solver. Each successful assignment is then interpreted as a metamodel instance that provably satisfies a coverage criteria or a graph property. We have already integrated this approach into our existing tool to demonstrate the feasibility.

Paper Citation

in Harvard Style

Wu H. (2016). Generating Metamodel Instances Satisfying Coverage Criteria via SMT Solving . In Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-758-168-7, pages 40-51. DOI: 10.5220/0005650000400051

in Bibtex Style

@conference{modelsward16,
author={Hao Wu},
title={Generating Metamodel Instances Satisfying Coverage Criteria via SMT Solving},
booktitle={Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2016},
pages={40-51},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005650000400051},
isbn={978-989-758-168-7},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Generating Metamodel Instances Satisfying Coverage Criteria via SMT Solving
SN - 978-989-758-168-7
AU - Wu H.
PY - 2016
SP - 40
EP - 51
DO - 10.5220/0005650000400051