A sensible model of a system that uses real time will not depend on continuity properties of the reals. Hence, systems can be modeled with time assuming integer values. Whether model checking can be effective at catching errors in such specs is a question I can't answer because I have no experience with industrial systems that make use of real time. Except in embedded systems, real-time is generally used only for timeouts and can be modeled by letting timeout be an asynchronous event unrelated to time, since it's dangerous to rely on timeout values for correctness. (Fairness conditions can be used to ensure that a timeout eventually happens if a desired action doesn't occur.) For embedded systems, you might want to look at a paper I wrote called something like "Real Time is Really Simple".