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

Tobe Toben

Sujets

• Informatik

Informations

• Publié par: carl_von_ossietzky_universitat_oldenburg
• Publié le: 01 janvier 2009
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Fakult¨at II – Informatik, Wirtschafts- und Rechtswissenschaften
Department fu¨r Informatik
Analysis of Dynamic Evolution Systems
by Spotlight Abstraction Refinement
Dissertation zur Erlangung des Grades eines
Doktors der Naturwissenschaften
vorgelegt von
Dipl.-Inform. Tobe Toben
Gutachter:
Prof.Dr.Werner Damm
Prof.Dr.Ernst-Ru¨diger Olderog
Tag der Disputation: 10. Februar 2009c 2009 by the author
[e-mail])
http://purl.oclc.org/net/phd/toben09Fu¨r meinen Vater.Abstract
Dynamic Evolution Systems describe an emerging class of systems that vary
dynamically in size and topology. Typical examples include the adhoc network-
ing principle where a routing infrastructure over a changing set of participants
is created and maintained. A corresponding routing protocol has to be able to
handle an arbitrary number of nodes and must in particular be prepared for
the integration of new and the proper dismissal of disappeared devices. Similar
structures occur in dynamic traffic management systems like the car platooning
scenario where physically adjacent cars establish interlinked groups.
This thesis presents a formal method to check whether a system in the sense
above adheres 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 spot-
light 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 dedi-
cated 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
refinementmethodisbasedontheobservationthattheprecisionoftheabstrac-
tion 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. We demonstrate that the approach can be further improved by
integrating auxiliary system invariants, and we devise a static analysis method
to obtain such invariants for an existing modelling language.
Our approach is realised in form of a tool implementation. On this basis, we
perform a practical evaluation of our approach on a number of case studies that
cover a broad range of the addressed class of systems. We are in particular able
to automatically establish system properties for which manual intervention was
required before.
vZusammenfassung
Dynamic Evolution Systems beschreiben eine neue Klasse von Systemen welche
sich dynamisch in ihrer Gr¨oße und Verbindungsstruktur ver¨andern. Ein typi-
sches Beispiel hierfu¨r sind ad-hoc Netzwerke in welchen sich eine Routingstruk-
tur u¨ber eine wechselnde Anzahl von Teilnehmern dynamisch bildet und an-
passt. Ein zugeh¨origes Routingprotokoll ist dafu¨r verantwortlich eine beliebige
Anzahl von Knoten zu integrieren und insbesondere auch verschwundene Teil-
¨nehmer sicher aus dem Netz zu entfernen. Ahnliche Strukturen entstehen in
Verkehrsmanagementsystemen wie dem Car Platooning in welchem sich be-
nachbarte Autos zu einer Gruppe zusammenschließen.
Diese Arbeit pr¨asentiert eine Methode mit welcher u¨berpru¨ft werden kann
ob ein solches System formale Anforderungen in Form von Szenarien erfu¨llt.
Wir zeigen, dass die Unbeschr¨anktheit der Systeme diese Aufgabe im Allge-
meinen unentscheidbar macht und pr¨asentieren eine sichere aber notwendiger-
weise unvollst¨andige L¨osung die auf dem Prinzip abstract-check-refine basiert.
UnserAnsatzbenutztdieTechnikder“SpotlightAbstraction”umeineendliche
DarstellungdesSystemsundderAnforderungzuerhalten. DieIdeehinterdieser
Technik ist eine endliche Anzahl von Spotlichtprozessen pr¨azise darzustellen
und alle anderen Prozesse zu einem abstrakten Prozess kollabieren zu lassen.
Da eine Eigenschaft oftmals nicht in der initialen Abstraktion bewiesen oder
widerlegt werden kann, schlagen wir eine Verfeinerungsmethode basierend auf
abstrakten Gegenbeispielen vor. Wir zeigen, dass die Pr¨azision der Abstraktion
aufzweigrunds¨atzlicheArtenverbessertwerdenkann,n¨amlichzumeinendurch
Vergr¨oßerung des Spotlights und zum anderen durch eine Verfeinerung des Ver-
haltens des abstrakten Prozesses. Zudem pr¨asentieren wir eine Methode aus
dem Bereich der statischen Modellanalyse mittels welcher das Verfahren weiter
verbessert werden kann.
WirhabeneineImplementierungvorgenommenumunserenAnsatzevaluieren
zu k¨onnen. Hierzu betrachten wir Fallstudien und Eigenschaften die einen
großen Bereich der gesamten Systemklasse abdecken. Wir sind insbesondere
in der Lage Eigenschaften automatisch zu beweisen, bei welchen bisher eine
manuelle Unterstu¨tzung n¨otig war.
viiAcknowledgements
I want to thank my supervisor Prof. Dr. Werner Damm for his constant effort
in creating a perfect research environment which offers a broad scope of coop-
eration and inspiration. In particular the collaborative work within the AVACS
(www.avacs.org) project provided me with new and interesting aspects regard-
ing my research topic. I’m very glad that Prof. Dr. Ernst-Ru¨diger Olderog
became the second reviewer of this thesis. My work in his group during my
studies fostered my interest in formal methods. In this context I also very much
appreciated the inspiring thoughts and lectures of Dr. habil. Henning Dierks.
The topic of this thesis has been developed in close collaboration with my
former colleague Bernd Westphal. Bernd is always a source of inspiration in
variousareaslikespecificationandabstractiontechniques,innovative(yetsome-
times weird) research ideas, travelling plans and on which text editor to use.
From the AVACS family I like to express my gratitude to J¨org Kreiker and Ina
Schaefer for openly sharing their ideas and scientific skills. I also thank my col-
leagues Jan-Hendrik Rakow for fruitful discussions concerning languages, tools
and swingsets, Christian Ammann for his reliable implementation work, Ingo
Schinz and Christian Mrugalla for thought-provoking conversations in the early
era, Ju¨rgen Niehaus for managing every possible and impossible request, and
rest of the Mensakarawane, Eckard, Thomas, Pate Ralf, thias, Lars and Eike,
for ensuring an enjoyable lunch break.
From my social circle I like to mention the members of DownStairs and the
Pilshotline who provide sonorous and convivial times of recreation and who are
remaining close friends for many years now. Finally I want to thank my whole
familyfortheirendlesstrustandsupport. ThisinparticularaddressesManuela
and Tammo who keep me focussed on the real important aspects of life.
ix