I have never had occasion to write a practical real-time
specification, so I can't say what really works. Often, engineers
think they need to use real time because their system uses timeouts.
However, in most of today's distributed systems, timeouts are used
only to ensure some liveness property. In that case, a timeout can be
modeled as an action that can be (but need not be) taken at any time.
If you really need to check that some actions happen within some
specific length of time, them you need real-time specification.
The method described in "Specifying Systems" might work for proofs,
but it's not for model checking. I wrote a paper called "Real Time is
Really Simple" with a method for model checking real-time properties.
The non-obvious part of that paper probably doesn't apply to what
you're doing, since checking your spec over a fixed time period is
probably good enough. You can find the paper and a discussion of it at
http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#real-simple
Leslie