The goal of model checking is verifying that a system adheres to its specification. The model checking tool UPPAAL verifies Timed Automata and returns diagnostic traces to help users understand violations of the specifications. Due to the time abstractions used in the computations, the diagnostic traces returned are hard to comprehend for users, as they do not contain concrete delays.
In this thesis we describe several approaches to generating concrete delays for diagnostic traces. Two of these approaches are based on the diagnostic traces that violate safety properties and one approach is based on the diagnostic traces that violate liveness properties. We prove the correctness of all approaches and test the safety approaches against each other. The liveness approach is tested for viability.