This talk discusses how verification techniques, in particular \emph{model checking} can be used to guide \emph{discrete event simulation}. We believe that this combination is very promising, and rich in potential applications. 

The mathematical workhorse for this approach is a nondeterministic \emph{and} stochastic model, in particular the model of a stochatic timed automata. These models are rich in modelling power, which makes them well-suited for many diverse application areas. However, discrete-event-simulation can only be used in a meaningful way, 
if nondeterminism is resolved by some means. This is where model-checking comes into play, to provide examples (or counterexamples) of interesting behaviour sequences to be studied via simulation. 

A concrete example will be used to illustrate this general approach. In the example, we use real-time model checking with UPPAAL to synthesize feasible production schedules for a laquer production plant. Then we study the effect of machine breakdowns and repairs for the synthesized schedules using the discrete-event simulator of the M{\"o}bius toolset. The entire toolflow is supported by the modelling language MODEST, and its accompanying tool MOTOR.