MURAL - Maynooth University Research Archive Library

    Exploiting attributed type graphs to generate metamodel instances using an SMT solver

    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

    Download (465kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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:
    Depositing User: Dr. James Power
    Date Deposited: 22 Sep 2015 15:02
    Publisher: IEEE
    Refereed: Yes
    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)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads