Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
On Verifying ATL Transformations Using ‘off-the-shelf’ SMT Solvers
verfasst von : Fabian Büttner, Marina Egea, Jordi Cabot
Erschienen in: Model Driven Engineering Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
MDE is a software development process where models constitute pivotal elements of the software to be built. If models are well-specified, transformations can be employed for various purposes, e.g., to produce final code. However, transformations are only meaningful when they are ‘correct’: they must produce valid models from valid input models. A valid model has conformance to its meta-model and fulfils its constraints, usually written in OCL. In this paper, we propose a novel methodology to perform automatic, unbounded verification of ATL transformations. Its main component is a novel first-order semantics for ATL transformations, based on the interpretation of the corresponding rules and their execution semantics as first-order predicates. Although, our semantics is not complete, it does cover a significant subset of the ATL language. Using this semantics, transformation correctness can be automatically verified with respect to non-trivial OCL pre- and postconditions by using SMT solvers, e.g. Z3 and Yices.