Reports

Cunha A, Jorge T, Macedo N.  2015.  A Feature-based Classification of Model Repair Approaches. Abstract1504.03947v1.pdf

Consistency management, the ability to detect, diagnose and handle inconsistencies, is crucial during the development process in Model-driven Engineering (MDE). As the popularity and application scenarios of MDE expanded, a variety of different techniques were proposed to address these tasks in specific contexts. Of the various stages of consistency management, this work focuses on inconsistency fixing in MDE, where such task is embodied by model repair techniques. This paper proposes a feature-based classification system for model repair techniques, based on an systematic review of previously proposed approaches. We expect this work to assist both the developers of novel techniques and the MDE practitioners looking for suitable solutions.
Pacheco H, Macedo N, Cunha A, Voigtländer J.  2013.  A Generic Scheme and Properties of Bidirectional Transformations. CoRR. arXiv/1306.4473:19. Abstract1306.4473v2.pdf

The recent rise of interest in bidirectional transformations (BXs) has led to the development of many BX frameworks, originating in diverse computer science disciplines. From a user perspective, these frameworks vary significantly in both interface and predictability of the underlying bidirectionalization technique. In this paper we start by presenting a generic BX scheme that can be instantiated to different concrete interfaces, by plugging-in the desired notion of update and traceability. Based on that scheme, we then present several desirable generic properties that may characterize a BX framework, and show how they can be instantiated to concrete interfaces. This generic presentation is useful when exploring the BX design space: it might help developers when designing new frameworks and end-users when comparing existing ones. We support the latter claim, by applying it in a comparative survey of popular existing BX frameworks.
Macedo N, Pacheco H, Cunha A.  2012.  Relations as executable specifications: taming partiality and non-determinism using invariants. :146-161. Abstractndlenses12tech.pdf

The calculus of relations has been widely used in program specification and reasoning. It is very tempting to use such specifications as running prototypes of the desired program, but, even considering finite domains, the inherent partiality and non-determinism of relations makes this impractical and highly inefficient. To tame partiality we prescribe the usage of invariants, represented by coreflexives, to characterize the exact domains and codomains of relational specifications. Such invariants can be used as pre-condition checkers to avoid runtime errors. Moreover, we show how such invariants can be used to narrow the non-deterministic execution of relational specifications, making it viable for a relevant class of problems. In particular, we show how the proposed techniques can be applied to execute specifications of bidirectional transformations, a domain where partiality and non-determinism are paramount.
Macedo N, Cunha A.  2011.  Automatic unbounded verification of Alloy specifications with Prover 9. CoRR. abs/1209.5773:17. Abstract1209.5773v1.pdf

Alloy is an increasingly popular lightweight specification language based on relational logic. Alloy models can be automatically verified within a bounded scope using off-the-shelf SAT solvers. Since false assertions can usually be disproved using small counter-examples, this approach suffices for most applications. Unfortunately, it can sometimes lead to a false sense of security, and in critical applications a more traditional unbounded proof may be required. The automatic theorem prover Prover9 has been shown to be particularly effective for proving theorems of relation algebras, a quantifier-free (or point-free) axiomatization of a fragment of relational logic. In this paper we propose a translation from Alloy specifications to fork algebras (an extension of relation algebras with the same expressive power as relational logic) which enables their unbounded verification in Prover9. This translation covers not only logic assertions, but also the structural aspects (namely type declarations), and was successfully implemented and applied to several examples.