In this article two views on DRM are presented and modelled in VDM. The contribution from this modelling process is two-fold. A set of properties that are of interest while designing DRM systems are presented. Then, the two models are compared to elaborate our understanding of DRM elements and their inter- play. This work is an exploration towards realizing a core model and terminology upon which extended models can be built.
Proceedings of the 10th Overture Workshop, 2012, p. 20-29