Dynamic Evolution Systems describe an emerging class of systems that vary dynamically in size and topology. This thesis presents a formal method to check whether such systems adhere to requirements given in form of temporal scenarios. We observe that the inherent unboundedness of the systems renders this task in general undecidable and we present a sound but necessarily incomplete solution that is based on the abstract-check-reﬁne paradigm. Our approach employs the spotlight abstraction principle to obtain a ﬁnite description of both the system and the requirement. The idea of this abstraction technique is to exactly preserve the behaviour of a ﬁnite set of spotlight processes and to provide one dedicated abstract process to over-approximate the behaviour of the non-spotlight processes. As the validity of a requirement often cannot be deﬁnitely decided in the initial abstraction, we propose an automatic and iterative reﬁnement of the abstraction that is guided by the analysis of abstract counterexamples. The reﬁnement method is based on the observation that the precision of the abstraction can be tuned by two complementary principles, namely by enlarging the size of the spotlight and by reﬁning the behaviour of the non-spotlight part of the abstraction.