Wu, Hao and Monahan, Rosemary and Power, James F.
(2013)
Exploiting attributed type graphs to generate
metamodel instances using an SMT solver.
In:
International Symposium on Theoretical Aspects of Software Engineering (TASE), 2013.
IEEE, pp. 175-182.
ISBN 9780768550534
Abstract
In this paper we present an approach to generating
instances of metamodels using a Satisfiability Modulo
Theories (SMT) solver as a back-end engine. Our goal is to
automatically translate a metamodel and its invariants into
SMT formulas which can be investigated for satisfiability by an
external SMT solver, with each satisfying assignment for SMT
formulas interpreted as an instance of the original metamodel.
Our automated translation works by interpreting a metamodel as
a bounded Attributed Type Graph with Inheritance (ATGI) and
then deriving a finite universe of all bounded attribute graphs
typed over this bounded ATGI. The graph acts as an intermediate
representation which we then translate into SMT formulas. The
full translation process, from metamodels to SMT formulas, and
then from SMT instances back to metamodel instances, has been
successfully automated in our tool, with the results showing the
feasibility of this approach.
| Item Type: |
Book Section
|
| Additional Information: |
This is the postprint version of the article published at DOI: 10.1109/TASE.2013.31 |
| Keywords: |
attributed type graphs;
metamodel instances; SMT solver; |
| Academic Unit: |
Faculty of Science and Engineering > Computer Science |
| Item ID: |
6375 |
| Identification Number: |
https://doi.org/10.1109/TASE.2013.31 |
| Depositing User: |
Dr. James Power
|
| Date Deposited: |
22 Sep 2015 15:02 |
| Publisher: |
IEEE |
| Refereed: |
Yes |
| URI: |
|
| Use Licence: |
This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available
here |
Repository Staff Only(login required)
 |
Item control page |
Downloads per month over past year
Origin of downloads
Altmetric
Altmetric