@phdthesis{Tob2009,
Author = {Toben, Tobe},
Title = {Analysis of Dynamic Evolution Systems by Spotlight Abstraction Refinement},

Year = {2009},
Month = {02},
Publisher = {Carl von Ossietzky Universität Oldenburg},
Address = {Oldenburg,  Germany},
type = {phdthesis},
note = {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 },
Abstract = {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-refine paradigm. Our approach employs the spotlight abstraction principle to obtain a finite description of both the system and the requirement. The idea of this abstraction technique is to exactly preserve the behaviour of a finite 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 definitely decided in the initial abstraction, we propose an automatic and iterative refinement of the abstraction that is guided by the analysis of abstract counterexamples. The refinement 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 refining the behaviour of the non-spotlight part of the abstraction.}
}
@COMMENT{Bibtex file generated on }