Formal specification and verification of the OMA license choice algorithm in the OTS/CafeOBJ method

OMA-Digital Rights Management System is a standard proposed by the Open Mobile Alliance (OMA) for protecting digital content distribution via mobile networks. To solve the decision problem, in the case that multiple licenses refer to the same content, OMA suggests a license choice algorithm. This algorithm ensures the fine grained consumption of contents. CafeOBJ is a new generation algebraic specification language. We apply the OTS/CafeOBJ method to formally model, specify and verify the above mentioned license choice algorithm. More specifically, we develop the mathematical model of the OMA decision algorithm as an OTS, a kind of transition system expressed in an equational CafeOBJ specification style. Finally, we verify that this algorithm fulfills the following safety property: Whenever a license is chosen for a given content, then the license is valid at that specific time.