Reachability in pushdown systems [Elektronische Ressource] : algorithms and applications / Dejvuth Suwimonteerabuth

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2009
• Nombre de lectures: 11
• Langue: Deutsch

Extrait

Lehrstuhl fu¨r Informatik VII
der Technischen Universit¨at Mu¨nchen
Reachability in Pushdown Systems:
Algorithms and Applications
Dejvuth Suwimonteerabuth
Vollst¨andiger Abdruck der von der Fakult¨at fu¨r Informatik der Techni-
schen Universit¨at Mu¨nchen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Helmut Seidl
Pru¨fer der Dissertation: 1. Univ.-Prof. Dr. Javier Esparza
2. Prof. Dr. Ahmed Bouajjani,
Universit¨at Paris Diderot/Frankreich
Die Dissertation wurde am 27.01.2009 bei der Technischen Universit¨at
Mu¨nchen eingereicht und durch die Fakult¨at fu¨r Informatik am 08.05.2009
angenommen.Kurzfassung
Diese Arbeit pr¨asentiert Erreichbarkeitsanalysen fu¨rPushdown-Systeme und
ihre Anwendungen auf unterschiedliche Bereiche. Ein Pushdown-System ist
einestack-basierteMaschine,derenStackunbegrenztist. Pushdown-Systeme
sind ein natu¨rliches Modell fu¨r sequenzielle Programme. Angeregt durch
einige Anwendungen analysiert diese Arbeit das Erreichbarkeitsproblem in
verallgemeinerten Pushdown-Modellen—alternierenden PushdownSystemen
und Pushdown-Netzwerken—und diskutiert sie im Detail.
EinPushdown-NetzwerkkannzurModellierungnebenl¨aufigerProgramme
verwendet werden. Die Erreichbarkeitsalgorithmen hierfu¨r, zusammen mit
¨einem Ubersetzer von Java-Bytecode in Pushdown-Netzwerke, wurden op-
timiert und in einem Tool namens jMoped implementiert. jMoped ist ein
Eclipse-Plugin, das Benutzern das einfache Testen von Java-Programmen
erm¨oglicht, ohne dass sie die dazu verwendeten Techniken verstehen mu¨ssen.
jMoped gibt fortlaufend den bislang erreichten Grad der Abdeckung aus und
entdeckt Fehler wie z.B. Verletzungen von Assertions. Die Arbeit berichtet
u¨ber praktische Experimente mit jMoped.
Alternierende Pushdown-Systeme werden als nu¨tzliches Modell fu¨rAuto-
risierungs- und Reputations-Systeme vorgestellt, deren Fragestellungen sich
auf Erreichbarkeitsprobleme in den Modellen reduzieren lassen.Abstract
This thesis presents reachability algorithms for pushdown systems and their
applications to different areas. Roughly speaking, a pushdown system is a
stack-based machine whose stack can be unbounded, making it a natural
model for sequential programs. Inspired by applications, the thesis analyzes
reachability in more generalized pushdown models—alternating pushdown
systems and pushdown networks—and discusses their complexities in detail.
A pushdown network can be used for modeling multithreaded programs.
The reachability algorithms, together with a translator from Java bytecodes
into pushdown networks, have been optimized and implemented in a tool
called jMoped. jMoped is an Eclipse plug-in which allows users to easily test
Java programs without any knowledge of the techniques behind it. jMoped
progressively outputs coverability information and uncovers errors such as
assertionviolations. SeveralpracticalexperimentswithjMopedarereported.
Alternating pushdown systems are shown to be suitable models for au-
thorization systems and reputation systems, where reasoning in the systems
boils down to solving reachability in the models.Acknowledgments
Thisthesiswouldnothavebeenpossiblewithoutthesupportofmanypeople.
I would like to express my deepest gratitude to my supervisor Prof. Javier
Esparza for his invaluable assistance, guidance, patience, and for giving me
the opportunity to conduct research in his group. Special thanks go to Ste-
fan Schwoon. Without his knowledge and assistance this research would not
have been successful. I am very grateful to Prof. Ahmed Bouajjani, Tayssir
Touili, and Mihaela Sighireanu for their abundant help with the research. I
would also like to convey thanks to SFB 627 Nexus, Universita¨t Stuttgart,
and Technische Universit¨at Mu¨nchen for providing the financial and organi-
zational support. Many thanks to my colleagues, especially to Stefan Kiefer
and Michael Luttenberger, for their endless help and the great working at-
mosphere.
I would like to acknowledge Prof. Prabhas Chongstitvatana, the super-
visor during my undergraduate study, for his inspiring advice. My parents
and my brother, their love, understanding, and encouragement have never
been absent, no matter when. YupadaraNetprapa, her love andunderstand-
ing complete my life. I feel indebted to many people, in particular friends,
for their bottomless help. They all play a role in this thesis, although not
mentioned here. I thank you all.Contents
1 Introduction 1
1.1 Contribution of the thesis . . . . . . . . . . . . . . . . . . . . 4
1.2 Related works . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Preliminaries 10
2.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.1 Semirings . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.2 Finite automata . . . . . . . . . . . . . . . . . . . . . . 12
2.2 Pushdown models . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.1 Pushdown systems . . . . . . . . . . . . . . . . . . . . 14
2.2.2 Alternating pushdown systems . . . . . . . . . . . . . . 15
2.2.3 Pushdown networks . . . . . . . . . . . . . . . . . . . . 17
2.3 Binary decision diagrams . . . . . . . . . . . . . . . . . . . . . 18
3 Reachability analyses 23
3.1 Bounded idempotent semirings . . . . . . . . . . . . . . . . . 23
3.1.1 Pushdown systems . . . . . . . . . . . . . . . . . . . . 23
3.1.2 Alternating pushdown systems . . . . . . . . . . . . . . 28
3.1.3 Pushdown networks . . . . . . . . . . . . . . . . . . . . 43
3.2 General semirings . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.2.1 Pushdown systems . . . . . . . . . . . . . . . . . . . . 51
3.2.2 Alternating pushdown systems . . . . . . . . . . . . . . 54
4 Application to Java testing 61
4.1 Java virtual machine . . . . . . . . . . . . . . . . . . . . . . . 62
4.1.1 Java bytecode basics . . . . . . . . . . . . . . . . . . . 63
4.1.2 Instruction set . . . . . . . . . . . . . . . . . . . . . . . 71
4.2 Translator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
i4.2.1 Control flow modeling . . . . . . . . . . . . . . . . . . 77
4.2.2 Variable modeling . . . . . . . . . . . . . . . . . . . . . 78
4.2.3 Java virtual machine modeling: Basics . . . . . . . . . 79
4.2.4 Java virtual machine modeling: Extensions . . . . . . . 89
4.3 Applying the reachability analyses . . . . . . . . . . . . . . . . 96
4.3.1 Representing variable relations as semirings . . . . . . 96
4.3.2 Specialized reachability algorithms . . . . . . . . . . . 100
4.3.3 Counterexample extraction . . . . . . . . . . . . . . . . 104
5 Experiments with jMoped 111
5.1 BDDs vs. bit vectors . . . . . . . . . . . . . . . . . . . . . . . 114
5.2 Quicksort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
5.2.1 Version 1 . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.2.2 Version 2 . . . . . . . . . . . . . . . . . . . . . . . . . 120
5.3 jMoped BDD library . . . . . . . . . . . . . . . . . . . . . . . 122
5.4 java.util.Vector class . . . . . . . . . . . . . . . . . . . . . 125
5.5 Windows NT Bluetooth driver . . . . . . . . . . . . . . . . . . 129
5.6 Binary search tree . . . . . . . . . . . . . . . . . . . . . . . . . 131
6 Applications to SPKI/SDSI 136
6.1 Authorization systems . . . . . . . . . . . . . . . . . . . . . . 136
6.1.1 SPKI/SDSI . . . . . . . . . . . . . . . . . . . . . . . . 137
6.1.2 Intersection certificates . . . . . . . . . . . . . . . . . . 140
6.1.3 Example and experiments . . . . . . . . . . . . . . . . 141
6.2 Reputation system . . . . . . . . . . . . . . . . . . . . . . . . 144
6.2.1 SDSIrep . . . . . . . . . . . . . . . . . . . . . . . . . . 145
6.2.2 Intersection certificates . . . . . . . . . . . . . . . . . . 150
6.2.3 Example and experiments . . . . . . . . . . . . . . . . 152
6.3 Pushdown games . . . . . . . . . . . . . . . . . . . . . . . . . 157
7 Conclusions 160
Bibliography 163
ii