Formal verification has become an alternative to simulation for the validation of systems. Especially temporal logic model checking of finite state machines is a widely accepted verification technique. It automatically proves the correctness of design specifications. There exist several approaches extending model checking for the verification of timed systems. Things getting more complex if additionally multivalued signals are added to the systems. In this constellation, time effects and data dependencies merge. Therefore, a stand-alone model checking approach is in many cases not sufficient for verification, especially if extreme values of signals have to be determined.

In this paper we extend an existing real-time finite state model by multivalued signals (ranges, enumerations and bit vectors). We present algorithms computing minimal and maximal values of signals in specified states or within certain time bounds. We will show the practicability of our approach by means of a case study.