This year (well, also the last one 🙂 ) we got two papers accepted at the MoDELS 2012 conference . As usual, later on I´ll publish a guest blog post for each paper but for those that can’t wait, the titles, authors and abstracts of the papers are the following:
- On verifying ATL transformations using ‘off-the-shelf’ SMT solvers by Fabian Büttner, Marina Egea and Jordi Cabot.
Abstract: MDE is a software development process where models constitute pivotal elements of the software to be built. Ideally, if these models are sufficiently
well specified, transformations can be employed for different purposes, e.g., they may be used to finally produce actual code. However, transformations are only meaningful when they are ‘correct’ in the sense that they must output ‘valid’ models from ‘valid’ input models. A valid model is one that has conformance to
its meta-model and fulfils its constraints, usually written in OCL, that is, the OMG standard constraint language for models. In this paper we propose a methodology for verifying ATL transformations. The main component of our methodology 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. Our approach is a practical one, and we report on our experience using SMT solvers, e.g. Z3, to automatically verify transformations with respect to non-trivial pre- and post-conditions, based on our first-order semantics.
- ATLTest: A White-Box Test Generation Approach for ATL Transformations by Carlos A. González and Jordi Cabot.
Abstract: MDE is being applied to the development of increasingly complex systems that require larger model transformations. Given that the specification of such transformations is an error-prone task, techniques to guarantee their quality must be provided. Testing is a well-known technique for finding errors in programs. In this sense, adoption of testing techniques in the model transformation domain would be helpful to improve their quality. So far, testing of model transformations has focused on black-box testing techniques. Instead, in this paper we provide a white-box test model generation approach for ATL model transformations.