Dealing with Different Time Granularities in Formal Specifications of Real-Time Systems