A Formal Foundation of the RM-ODP Conceptual Framework

This paper presents an approach for formalizing the RM-ODP (Reference Model for Open Distributed Processing), an ISO and ITU standard. The goal of this formalization is to clarify the RM-ODP modeling framework to make it more accessible to modelers such as system architects, designers and implementers, while opening the way for the formal verification of RM-ODP models, either within an ODP viewpoint or across multiple ODP viewpoints. The result of this work is a consistent formal representation of clauses 5, 6, 8 and 9 of part 2 of RM-ODP in their interrelations, which while being officially declared as one of its goals is currently missing in the standard. Our formalization is based on set theory and the classical predicate logic, and is expressed in the Alloy language.