This thesis "Automated Generation of Timed Tests with Isabelle and HOL-TestGen" attempts to apply “proof-based testing techniques” [BW12b, BKLW10, BW12a, Fel12] on concrete embedded real-time systems to be concretized by project partners. The Isabelle/HOL-TestGen-system (a plugin in Isabelle/HOL) will be used to formalize wide-spread specification languages (UML,OCL, SysML, Scade) as logical embeddings and to extend them by techniques to generate tests from models involving real-time constraints, currently used in distributed and massively parallel processors. Particular emphasis will be put on integration of vizualization techniques to be integrated into the plateform Isabelle/PIDE underlying HOL-TestGen.