Analysis of dynamic evolution systems by spotlight abstraction refinement [Elektronische Ressource] / vorgelegt von Tobe Toben

Fakult¨at II – Informatik, Wirtschafts- und RechtswissenschaftenDepartment fu¨r InformatikAnalysis of Dynamic Evolution Systemsby Spotlight Abstraction RefinementDissertation zur Erlangung des Grades einesDoktors der Naturwissenschaftenvorgelegt vonDipl.-Inform. Tobe TobenGutachter:Prof.Dr.Werner DammProf.Dr.Ernst-Ru¨diger OlderogTag der Disputation: 10. Februar 2009c 2009 by the authortoben@informatik.uni-oldenburg.de)http://purl.oclc.org/net/phd/toben09Fu¨r meinen Vater.AbstractDynamic Evolution Systems describe an emerging class of systems that varydynamically in size and topology. Typical examples include the adhoc network-ing principle where a routing infrastructure over a changing set of participantsis created and maintained. A corresponding routing protocol has to be able tohandle an arbitrary number of nodes and must in particular be prepared forthe integration of new and the proper dismissal of disappeared devices. Similarstructures occur in dynamic traffic management systems like the car platooningscenario where physically adjacent cars establish interlinked groups.This thesis presents a formal method to check whether a system in the senseabove adheres to requirements given in form of temporal scenarios. We observethat the inherent unboundedness of the systems renders this task in generalundecidable and we present a sound but necessarily incomplete solution that isbased on the abstract-check-refine paradigm.