Software and Systems Modeling manuscript No. (will be inserted by the editor) Translating between Alloy Specifications and UML Class Diagrams Annotated with OCL

Abstract Model-Driven Engineering (MDE) is a Soft-ware Engineering approach based on model transfor-mations at di↵erent abstraction levels. It prescribes the development of software by successively transforming models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial a-doption is hampered by the lack of an ecosystem of MDE tools, namely code generators. This paper pre-sents a model transformation from Alloy to UML Class Diagrams annotated with OCL (UML+OCL), and shows how an existing transformation from UML+OCL to Al-loy can be improved to handle dynamic issues. The pro-posed bidirectional transformation enables a smooth in-tegration of Alloy in current MDE contexts, by allowing UML+OCL specifications to be transformed to Alloy for validation and verification, to correct and possibly refine them inside Alloy, and to translate them back to UML+OCL for sharing with stakeholders or to reuse current Model-Driven Architecture (MDA) tools to re-fine them towards code