²See [88, 90] for a general methodology to specify real-time systems, including object-oriented ones, in rewriting logic.