Lightweight formalization and validation of ORM models

ORM (Object Role Modeling) is a rich and popular conceptual modeling method. ORM has been used for data modeling, ontology engineering, modeling business rules, XML-Schemes and data warehouses, requirements engineering and web forms. Automated reasoning like satisfiability testing allows developers to detect modeling mistakes in the early stages of development. In this paper we propose a lightweight formalization of the ORM meta-model in Alloy. Using this meta-model as a toolkit one can easily specify ORM models in Alloy and verify various properties on them using the Alloy Analyzer. In order to achieve scalability, we use the cardinality of concepts to model their population. This increases the scalability of the approach dramatically. To show an application of the meta-model we formalize some unsatisfiability patterns and check them on the Alloy representation of the ORM model.