Innovations in Systems and Software Engineering manuscript No. (will be inserted by the editor) Transforming OntoUML into Alloy: Towards Conceptual Model Validation using a Lightweight Formal Method

Abstract While conceptual modeling is strongly related to the final quality of the software product [15], conceptual modeling itself remains a challenging activity. In particular, modelers must ensure that conceptual models properly formalize their intended conceptualization of a domain. This paper proposes an approach to facilitate the validation process of conceptual models defined in OntoUML by transforming these models into specifications in the logic-based language Alloy and using its analyzer to generate instances of the model and assertion counter-examples. By allowing the observation of sequences of snapshots of model instances, the dynamics of object creation, classification, association and destruction are revealed. This confronts the modeler with the implications of modeling choices and allows them to uncover mistakes or gain confidence in the quality of conceptual models