A Formal Specification of dMARS