Parallelisierung eines Software Modellprüfers für nebenläufige C++ Programme
©2007
Diplomarbeit
72 Seiten
Zusammenfassung
Inhaltsangabe:Einleitung:
Immer mehr Bereiche in unserem Leben werden durch Technik bestimmt. Musste man vor einiger Zeit den Wecker noch jeden Abend neu aufziehen, wechselt man heute nur ab und zu die Batterien. Die Zeit kommt, Atom-Uhr genau, per Funk. Baute man im Mittelalter Burgen ca. 30 km voneinander entfernt (dies entspricht der Distanz, die ein Mensch am Tag zu Fuß zurücklegen konnte) können wir heute nahezu jeden Ort der Welt innerhalb von 24 Stunden erreichen.
Nicht nur das Vordringen moderner Technik in immer mehr Lebensbereiche, auch die Weiterentwicklung dieser Technik, ob zur Steigerung der Lebensqualität oder zur Erhöhung der Sicherheit, stellt eine Herausforderung an Prüfmechanismen dar. Klingelt der Wecker morgens aufgrund eines Programmfehlers nicht, so ist dies nicht tragisch. Entscheidet aber eine Software aufgrund eines Modellierungsfehlers bei einer Landung eines Flugzeugs nicht zu bremsen, kann dieses sogar Menschenleben kosten.
Eine bis heute gängige Prüfmethode ist das Testen (Gelperin:Testing; Hetzel:Testing). Hierbei werden nach einem vorher bestimmten Ablaufplan nahezu alle Eigenschaften des Modells geprüft, die Prüfungen ausgewertet und gegebenenfalls Fehler eliminiert. Diese Methode ist nicht nur sehr zeitaufwändig, sondern auch nicht unbedingt zuverlässig. Da die Tests von Menschen ausgewählt werden, können unwahrscheinliche, jedoch fatale Fehler übersehen werden. Hinzu kommt der riesige Zeit- und Arbeitsaufwand, der nötig ist, um umfangreiche Software-Projekte zu überprüfen. Natürlich muss der Aufwand in nahezu gleichem Umfang wiederholt werden, falls ein Fehler entdeckt und entfernt wurde.
Bei Software, an die besonders hohe Sicherheitsanforderungen gestellt werden (zum Beispiel Software die in lebenserhaltenden Geräten eingesetzt wird) ist eine andere Vorgehensweise notwendig. Es werden Fehlerbedingungen in einer so genannten Metasprache definiert und die Software in diese Sprache übersetzt (Holzmann:Spin; ksu:bogor). Das so entstandene Modell kann nun von einem Modellprüfer (Clarke:ModelChecking) gelesen und bezüglich der Fehlerbedingungen verarbeitet werden. Verletzt die Software eine der Bedingungen so wird sie als Fehlerhaft eingestuft. Da die Übersetzung meist von Hand vorgenommen wird, entstehen zwei potentielle Quellen für falsche Testergebnisse. Erstens kann ein Fehler der während einer Prüfung diagnostiziert wurde, beim Übersetzten hinzugefügt worden sein. Zweitens ist es möglich, dass ein Fehler nicht […]
Immer mehr Bereiche in unserem Leben werden durch Technik bestimmt. Musste man vor einiger Zeit den Wecker noch jeden Abend neu aufziehen, wechselt man heute nur ab und zu die Batterien. Die Zeit kommt, Atom-Uhr genau, per Funk. Baute man im Mittelalter Burgen ca. 30 km voneinander entfernt (dies entspricht der Distanz, die ein Mensch am Tag zu Fuß zurücklegen konnte) können wir heute nahezu jeden Ort der Welt innerhalb von 24 Stunden erreichen.
Nicht nur das Vordringen moderner Technik in immer mehr Lebensbereiche, auch die Weiterentwicklung dieser Technik, ob zur Steigerung der Lebensqualität oder zur Erhöhung der Sicherheit, stellt eine Herausforderung an Prüfmechanismen dar. Klingelt der Wecker morgens aufgrund eines Programmfehlers nicht, so ist dies nicht tragisch. Entscheidet aber eine Software aufgrund eines Modellierungsfehlers bei einer Landung eines Flugzeugs nicht zu bremsen, kann dieses sogar Menschenleben kosten.
Eine bis heute gängige Prüfmethode ist das Testen (Gelperin:Testing; Hetzel:Testing). Hierbei werden nach einem vorher bestimmten Ablaufplan nahezu alle Eigenschaften des Modells geprüft, die Prüfungen ausgewertet und gegebenenfalls Fehler eliminiert. Diese Methode ist nicht nur sehr zeitaufwändig, sondern auch nicht unbedingt zuverlässig. Da die Tests von Menschen ausgewählt werden, können unwahrscheinliche, jedoch fatale Fehler übersehen werden. Hinzu kommt der riesige Zeit- und Arbeitsaufwand, der nötig ist, um umfangreiche Software-Projekte zu überprüfen. Natürlich muss der Aufwand in nahezu gleichem Umfang wiederholt werden, falls ein Fehler entdeckt und entfernt wurde.
Bei Software, an die besonders hohe Sicherheitsanforderungen gestellt werden (zum Beispiel Software die in lebenserhaltenden Geräten eingesetzt wird) ist eine andere Vorgehensweise notwendig. Es werden Fehlerbedingungen in einer so genannten Metasprache definiert und die Software in diese Sprache übersetzt (Holzmann:Spin; ksu:bogor). Das so entstandene Modell kann nun von einem Modellprüfer (Clarke:ModelChecking) gelesen und bezüglich der Fehlerbedingungen verarbeitet werden. Verletzt die Software eine der Bedingungen so wird sie als Fehlerhaft eingestuft. Da die Übersetzung meist von Hand vorgenommen wird, entstehen zwei potentielle Quellen für falsche Testergebnisse. Erstens kann ein Fehler der während einer Prüfung diagnostiziert wurde, beim Übersetzten hinzugefügt worden sein. Zweitens ist es möglich, dass ein Fehler nicht […]
Leseprobe
Inhaltsverzeichnis
Damian Sulewski
Parallelisierung eines Software Modellprüfers für nebenläufige C++ Programme
ISBN: 978-3-8366-1604-1
Druck Diplomica® Verlag GmbH, Hamburg, 2008
Zugl. Universität Dortmund, Dortmund, Deutschland, Diplomarbeit, 2007
Dieses Werk ist urheberrechtlich geschützt. Die dadurch begründeten Rechte,
insbesondere die der Übersetzung, des Nachdrucks, des Vortrags, der Entnahme von
Abbildungen und Tabellen, der Funksendung, der Mikroverfilmung oder der
Vervielfältigung auf anderen Wegen und der Speicherung in Datenverarbeitungsanlagen,
bleiben, auch bei nur auszugsweiser Verwertung, vorbehalten. Eine Vervielfältigung
dieses Werkes oder von Teilen dieses Werkes ist auch im Einzelfall nur in den Grenzen
der gesetzlichen Bestimmungen des Urheberrechtsgesetzes der Bundesrepublik
Deutschland in der jeweils geltenden Fassung zulässig. Sie ist grundsätzlich
vergütungspflichtig. Zuwiderhandlungen unterliegen den Strafbestimmungen des
Urheberrechtes.
Die Wiedergabe von Gebrauchsnamen, Handelsnamen, Warenbezeichnungen usw. in
diesem Werk berechtigt auch ohne besondere Kennzeichnung nicht zu der Annahme,
dass solche Namen im Sinne der Warenzeichen- und Markenschutz-Gesetzgebung als frei
zu betrachten wären und daher von jedermann benutzt werden dürften.
Die Informationen in diesem Werk wurden mit Sorgfalt erarbeitet. Dennoch können
Fehler nicht vollständig ausgeschlossen werden, und die Diplomarbeiten Agentur, die
Autoren oder Übersetzer übernehmen keine juristische Verantwortung oder irgendeine
Haftung für evtl. verbliebene fehlerhafte Angaben und deren Folgen.
© Diplomica Verlag GmbH
http://www.diplom.de, Hamburg 2008
Printed in Germany
Inhaltsverzeichnis
1
Einf ¨
uhrung
1
1.1
Vorwort . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1
1.2
Annahmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2
1.3
Struktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
1.4
Kontributionen
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
2
Der Software Modellpr ¨
ufer StEAM
5
2.1
Entstehung
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
2.2
Funktionsweise . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6
2.3
Suchalgorithmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
10
2.4
Speicherstruktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
12
2.5
Vergleich mit anderen Software Modellpr¨ufern
. . . . . . . . . . . . . . . . . . . .
13
2.6
Res¨umee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
3
Externalisierung
17
3.1
Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
3.2
Speicherstruktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
19
3.3
Der Algorithmus
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
3.4
Zugri
ff auf das sekund¨are Medium . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
3.5
Experimente . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
24
3.6
Res¨umee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
26
4
Virtualisierung
29
4.1
Speicherzugri
ff . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
29
4.2
Zugri
ff auf eine virtuelle Maschine . . . . . . . . . . . . . . . . . . . . . . . . . .
35
4.3
Res¨umee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
38
5
Parallelisierung
41
5.1
Einbindung der Externalisierung . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
5.2
Kommunikation zwischen den Knoten . . . . . . . . . . . . . . . . . . . . . . . . .
43
5.3
Verteilungsfunktionen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
45
i
ii
INHALTSVERZEICHNIS
5.4
Implementierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
48
5.5
Experimente . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
51
5.6
Res¨umee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
54
6
Fazit
55
A Die verwendeten Modelle
57
A.1 Speisenden Philosophen
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
57
A.2 N-Puzzle
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
59
A.3 Bakery Protokoll . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
60
Literaturverzeichnis
64
Abbildungsverzeichnis
2.1
Abbildung der Variablen in einem Zustand . . . . . . . . . . . . . . . . . . . . . . .
6
2.2
Ablauf einer Pr¨ufung in StEAM . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8
2.3
Pr¨ufen von C
++ Source mit Hilfe von StEAM . . . . . . . . . . . . . . . . . . . . .
9
2.4
Fehlerprotokoll der speisenden Philosophen . . . . . . . . . . . . . . . . . . . . . .
10
3.1
Interner Aufbau einer Festplatte
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
18
3.2
Externalisierung der Zust¨ande
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
20
3.3
Externe Collapse Kompression . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
3.4
Interner Speicherverbrauch, Npuzzle . . . . . . . . . . . . . . . . . . . . . . . . . .
25
3.5
Vergleich zwischen Swap Funktion und Externalisierung . . . . . . . . . . . . . . .
25
4.1
Direkter Zugri
ff auf Speicherbereiche . . . . . . . . . . . . . . . . . . . . . . . . .
30
4.2
MemoryPool in StEAM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
4.3
AUfteilung der virtuellen Adressen . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
4.4
Geschwindigkeit der Expandierung . . . . . . . . . . . . . . . . . . . . . . . . . . .
35
4.5
Kontrolle der VM ¨uber ein Interface . . . . . . . . . . . . . . . . . . . . . . . . . .
36
5.1
Vergleich Multicore und Cluster-System . . . . . . . . . . . . . . . . . . . . . . . .
41
5.2
Zwei-Wege-Kommunikation mit interen Cache Strukturen . . . . . . . . . . . . . .
44
5.3
Tiefenwert Verteilung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
47
5.4
Vertikale Aufteilung des Suchbaums . . . . . . . . . . . . . . . . . . . . . . . . . .
47
5.5
SpeedUp bei der L¨osung eines 15-Puzzle
. . . . . . . . . . . . . . . . . . . . . . .
52
5.6
SpeedUp, 200 Philosophen und DFS . . . . . . . . . . . . . . . . . . . . . . . . . .
53
5.7
Badewannen E
ffekt bei Verteilung entsprechend der Tiefe . . . . . . . . . . . . . . .
53
5.8
Expandierung des Bakery Protokolls . . . . . . . . . . . . . . . . . . . . . . . . . .
54
A.1 C
++ Quellcode eines Philosophen (run-Mathode der Klasse) . . . . . . . . . . . . .
57
A.2 C
++ Quellcode des speisende Philosophen Protokolls(main-Routine) . . . . . . . .
58
A.3 Beispiel eines 16-Puzzels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
59
A.5 Funktion um ein Pl¨atchen im nPuzzle zu verschiebenn
. . . . . . . . . . . . . . . .
59
A.4 C
++ Quelltext des NPuzzle Modells (main-Methode) . . . . . . . . . . . . . . . . .
61
iii
iv
ABBILDUNGSVERZEICHNIS
A.6 Initialisierung des Bakery Algorithmus als C
++ Quelltext . . . . . . . . . . . . . . .
62
A.7 Kunde einer B¨akerei als Thread in C
++ Quelltext . . . . . . . . . . . . . . . . . . .
62
A.8 Zuweisen einer Zahl und warten auf Eintritt im Bakery Protokoll . . . . . . . . . . .
63
Tabellenverzeichnis
3.1
Aufbau eines "Minizustands" . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
19
3.2
Vergleich verschiedener Methoden der Externalisierung beim 8 Puzzle.
. . . . . . .
26
3.3
Ergebnisse der Exploration des speisenden Philosophen Protokolls . . . . . . . . . .
28
A.1 Erl¨auterung des Fehlerpfades . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
58
v
Algorithmenverzeichnis
2.1
check (Zustandsraum auf Fehlerzust¨ande untersuchen) . . . . . . . . . . . . . . . .
11
2.2
getNext (n¨achsten zu expandierenden Zustand ausgeben) . . . . . . . . . . . . . . .
11
3.1
collapseCheck(Zust¨ande pr¨ufen unter Verwendung von Kompression) . . . . . . . .
22
3.2
collapseDecompress (einen Zustand aus einem Minizustand erzeugen) . . . . . . . .
23
3.3
read (lesen vom sekund¨aren Medium, Hash File Externalisierung) . . . . . . . . . .
24
4.1
getAddress (reale Adresse ermitteln) . . . . . . . . . . . . . . . . . . . . . . . . . .
33
4.2
getRealAddressFromPool (reale Adresse im Memory Pool ermitteln) . . . . . . . . .
34
4.3
expand (Ausf¨uhren von Opcodes in der virtuellen Maschine) . . . . . . . . . . . . .
38
5.1
search (Verteilte Suche mit zwei Kanal Kommunikation) . . . . . . . . . . . . . . .
49
5.2
getNext (n¨achsten aus der MPI Queue oder Open ausgeben)
. . . . . . . . . . . . .
51
vii
Kapitel 1
Einf ¨
uhrung
1.1
Vorwort
Immer mehr Bereiche in unserem Leben werden durch Technik bestimmt. Musste man vor einiger
Zeit den Wecker noch jeden Abend neu aufziehen, wechselt man heute nur ab und zu die Batterien.
Die Zeit kommt, Atom-Uhr genau, per Funk. Baute man im Mittelalter Burgen ca. 30 km voneinander
entfernt (dies entspricht der Distanz, die ein Mensch am Tag zu Fuß zur¨ucklegen konnte) k¨onnen wir
heute nahezu jeden Ort der Welt innerhalb von 24 Stunden erreichen.
Nicht nur das Vordringen moderner Technik in immer mehr Lebensbereiche, auch die Weiter-
entwicklung dieser Technik, ob zur Steigerung der Lebensqualit¨at oder zur Erh¨ohung der Sicherheit,
stellt eine Herausforderung an Pr¨ufmechanismen dar. Klingelt der Wecker morgens aufgrund eines
Programmfehlers nicht, so ist dies nicht tragisch. Entscheidet aber eine Software aufgrund eines Mo-
dellierungsfehlers bei einer Landung eines Flugzeugs nicht zu bremsen, kann dieses sogar Menschen-
leben kosten.
Eine bis heute g¨angige Pr¨ufmethode ist das Testen (Gelperin und Hetzel, 1988; Hetzel, 1990).
Hierbei werden nach einem vorher bestimmten Ablaufplan nahezu alle Eigenschaften des Modells
gepr¨uft, die Pr¨ufungen ausgewertet und gegebenenfalls Fehler eliminiert. Diese Methode ist nicht nur
sehr zeitaufw¨andig, sondern auch nicht unbedingt zuverl¨assig. Da die Tests von Menschen ausgew¨ahlt
werden, k¨onnen unwahrscheinliche, jedoch fatale Fehler ¨ubersehen werden. Hinzu kommt der riesige
Zeit- und Arbeitsaufwand, der n¨otig ist, um umfangreiche Software-Projekte zu ¨uberpr¨ufen. Nat¨urlich
muss der Aufwand in nahezu gleichem Umfang wiederholt werden, falls ein Fehler entdeckt und
entfernt wurde.
Bei Software, an die besonders hohe Sicherheitsanforderungen gestellt werden (zum Beispiel
Software die in lebenserhaltenden Ger¨aten eingesetzt wird) ist eine andere Vorgehensweise notwen-
dig. Es werden Fehlerbedingungen in einer so genannten Metasprache definiert und die Software in
diese Sprache ¨ubersetzt (Holzmann, 2004; Robby u. a., 2003). Das so entstandene Modell kann nun
von einem Modellpr¨ufer (Clarke u. a., 1999) gelesen und bez¨uglich der Fehlerbedingungen verarbei-
tet werden. Verletzt die Software eine der Bedingungen so wird sie als Fehlerhaft eingestuft. Da die
¨
Ubersetzung meist von Hand vorgenommen wird, entstehen zwei potentielle Quellen f¨ur falsche Test-
ergebnisse. Erstens kann ein Fehler der w¨ahrend einer Pr¨ufung diagnostiziert wurde, beim ¨
Ubersetzten
hinzugef¨ugt worden sein. Zweitens ist es m¨oglich, dass ein Fehler nicht erkannt wird, da dieser bei der
¨
Ubersetzung unwissentlich korrigiert wurde, in der Software allerdings weiterhin existiert. Des Wei-
teren kann eine Modellpr¨ufung nur Fehler diagnostizieren die in der Metasprache formuliert werden
k¨onnen.
1
2
Kapitel 1. Einf ¨
uhrung
Software Modellpr¨ufer
(Godefroid, 1997; Visser u. a., 2000a) sind hingegen in der Lage, Quelltex-
te zu pr¨ufen. Sie haben Ihre Wurzeln in der abstrakten Interpretaion (Cousot und Cousot, 1977) und
der Datenflussanalyse (Ste
ffen, 1993) Die vom Entwickler erstellte Software wird gelesen in einer
kontrollierten Umgebung ausgef¨uhrt und auf Fehler untersucht. Fehlerbedingungen k¨onnen sowohl in
den Quelltext, als auch in den Pr¨ufer eingebunden werden. StEAM
(Mehler, 2006), ein am Lehrstuhl
f¨ur Programmiersysteme der Universit¨at Dortmund entwickelter Software Modellpr¨ufer, der innerhalb
dieser Diplomarbeit erweitert wurde, verarbeitet die Programmiersprache C
++ (Stroustrup, 2000). Bei
dieser Sprache handelt es sich um eine h¨ohere Programmiersprache, die sowohl eine maschinenna-
he, als auch eine Programmierung auf hohem Abstraktionsniveau erm¨oglicht. Das Programm wird in
einer virtuellen Maschine (Visser u. a., 2000b) ausgef¨uhrt, die von StEAM kontrolliert wird.
Automatische Verifikationsmethoden k¨ampfen mit einem Problem: Der Anzahl der m¨oglichen
Programmzust¨ande
. Ein Programmzustand ist ein Abbild des Programms zu einem bestimmten Zeit-
punkt. Beim Testen werden zumeist so viele unterschiedliche Programmzust¨ande erzeugt, dass die
Ressourcen (Zeit oder Systemspeicher) nicht ausreichen, um komplexe Programme zu ¨uberpr¨ufen.
Bei der Software Modellpr¨ufung gibt es mehrere Ans¨atze, um diesem Ph¨anomen zu begegnen , z.B.
(Jard und J´eron, 1992; Lluch-Lafuente u. a., 2002; Holzmann, 1998). Ein m¨oglicher Ansatz ist die in
dieser Arbeit beschriebene Externalisierung und Parallelisierung. Dabei wird der Zustandsraum auf
mehrere Rechner verteilt, um so Zugang zu gr¨oßeren Ressourcen zu erhalten. Da die einzelnen Knoten
unterschiedliche, unabh¨angige Programmzust¨ande untersuchen, erwarten wir so eine schnellere Ant-
wort. Kombiniert mit der Vereinigung von Hauptspeicher k¨onnen auch komplizierte Software Modelle
untersucht werden. Diese Methode klingt verlockend, da sie auf den ersten Blick leicht skaliert. Falls
die gegebene Anzahl an Rechenknoten nicht ausreicht, f¨ugt man weitere hinzu. Dabei muss man aber
eines beachten. Wendet der Algorithmus zu viel Zeit f¨ur die Kommunikation zwischen Rechenknoten
auf, so geht der Zeitvorteil, der durch die Benutzung mehrerer Rechner erlangt wurde, verloren.
Ziel dieser Diplomarbeit war demnach den Software Modellpr¨ufer StEAM zu parallelisieren und
mehrere Rechner, die ¨uber ein Netzwerk verbunden sind, zur ¨
Uberpr¨ufung des Modells zu verwen-
den. Dabei sollte der zu entwickelnde Algorithmus, ¨uber geeignete Verteilungsfunktionen, nicht zu
viele Ressourcen f¨ur die Kommunikation verwenden, aber auch sicherstellen, dass Zust¨ande nicht
mehrfach expandiert werden. Der Modellpr¨ufer muss nat¨urlich weiterhin in der Lage sein, einen Feh-
lerzustand zu finden und den Fehlerpfad korrekt auszugeben. Des Weiteren sollte analysiert werden,
ob eine striktere Trennung, zwischen StEAM und der virtuellen Maschine, weitere M¨oglichkeiten zur
Modellpr¨ufung er¨o
ffnet.
1.2
Annahmen
In dieser Arbeit werden folgende plausiblen Annahmen getro
ffen.
1. Die Zust¨ande besitzen eine globale Repr¨asentation, da ein Rechner sonst die Zust¨ande anderer
Rechner nicht interpretieren kann.
2. Die Zust¨ande fordern Speicher dynamisch an und geben diesen wieder frei.
3. Die maximale Gr¨oße eines Programmzustands ist beschr¨ankt durch die Gr¨oße des Hauptspei-
chers des Rechenknoten mit minimalem Hauptspeicher.
4. Die zu pr¨ufenden Programme k¨onnen automatisch in die Sprache der virtuellen Maschine
¨ubersetzt werden.
State Exploring Assembly level Model Checker (http:
//steam.cs.uni-dortmund.de)
1.3. Struktur
3
5. Die Verteilungsfunktion ist global und wird w¨ahrend der Pr¨ufung nicht ver¨andert.
6. Ein Programmzustand enth¨alt alle zur Berechnung der Verteilungsfunktion ben¨otigten, Infor-
mationen.
1.3
Struktur
Die Arbeit ist wie folgt gegliedert:
Kapitel 2 stellt den verwendeten Software Modellpr¨ufer StEAM vor. Es wird die Funktionsweise
erl¨autert, und die unterst¨utzten Suchalgorithmen vorgestellt. Weiterhin wird die Speicherstruk-
tur n¨aher beschrieben und StEAM mit weiteren Software Modellpr¨ufern verglichen.
Kapitel 3 beschreibt eine Erweiterung von StEAM nicht direkt ben¨otigte Daten auf ein sekund¨ares
Medium (zum Beispiel eine Festplatte) auszulagern. Die Externalisierung ist Grundlage f¨ur die
Parallelisierung.
Kapitel 4 beschreibt zwei Erweiterungen, die f¨ur die Parallelisierung notwendig sind: Ein Interface,
¨uber welches auf die virtuelle Maschine zugegri
ffen wird und virtuelle Speicheradressen.
Kapitel 5 erl¨autert detailiert den Algorithmus zur Parallelisierung. Beschrieben wird die Kommuni-
kation, die Funktionen zur Verteilung der Zust¨ande und die Implementierung.
Kapitel 6 zieht ein Fazit und zeigt M¨oglichkeiten auf, StEAM zu erweitern.
Im Anhang werden die Modelle, im Quelltext, vorgestellt, die bei der Durchf¨uhrung der Experimen-
te verwendet wurden.
1.4
Kontributionen
Diese Arbeit erweitert den Software Modellpr¨ufer StEAM um folgende Eigenschaften.
Interface zur Steuerung einer virtuellen Maschine
Der Zugri
ff auf die virtuelle Maschine wurde ¨uber ein Interface realisiert. Dieses separiert die
virtuelle Maschine von dem Modellpr¨ufer und erm¨oglicht einen Austausch der selben. Mit dem
Wechsel der virtuellen Maschine w¨are StEAM in der Lage, Programme in beliebigen Program-
miersprachen zu pr¨ufen.
Virtuelle Speicheradressen
Das ausgef¨uhrte Programm greift nicht auf reale, sondern auf virtuelle Speicheradressen zu.
Diese stellen eine Verbindung zwischen der Speicherverwaltung des Betriebssystems und dem
Modell her. Durch Anpassung der virtuellen Adressen wird eine ¨
Ubertragung auf andere Rech-
ner und eine Verifikation auf weitere Fehlerarten m¨oglich.
Parallelisierung
Es werden mehrere Rechner, die durch ein Netzwerk verbunden sind, eingesetzt, um Modelle
zu pr¨ufen. Die gemeinsame Nutzung der Ressourcen, aller Rechner, erm¨oglicht es komplexe
Modelle in k¨urzerer Zeit zu untersuchen.
4
Kapitel 1. Einf ¨
uhrung
Modelle
Weitere Probleme wurden in C
++ implementiert. Diese demonstrieren sowohl die Fehlerarten,
als auch die Komplexit¨at der Modelle, die StEAM verarbeiten und pr¨ufen kann.
Kapitel 2
Der Software Modellpr ¨
ufer StEAM
Der schlimmste aller Fehler ist,
sich keines solchen bewußt zu sein.
Thomas Carlyle
2.1
Entstehung
Der Software Modellpr¨ufer StEAM (Mehler, 2006) pr¨uft nebenl¨aufige Programme, die in der Pro-
grammiersprache C
++ geschrieben wurden. Hierzu verwendet StEAM die "Internet C++ Virtual Ma-
chine"
(ICVM), die um spezielle Methoden zur Software Verifikation erweitert wurde.
Die ICVM wurde aufgrund ihrer Performance ausgew¨ahlt. Diese virtuelle Maschine wurde mit
dem Ziel programmiert, aktuelle Spiele, ohne diese neu kompilieren zu m¨ussen, auf verschiedenen
Plattformen auszuf¨uhren. Um die Geschwindigkeit der Maschine zu demonstrieren, wurde das kom-
merzielle 3D Spiel "DOOM" portiert.
Ein Programm, welches gepr¨uft werden soll, wird zuerst durch einen Compiler in Maschinenspra-
che, den sogenannten Objektcode, ¨ubersetzt. F¨ur die ICVM wird ein spezieller Compiler ben¨otigt, der
den Quelltext in Objektcode f¨ur einen Motorola 86K Chip ¨ubersetzt. Ein so kompilierter Objektcode
kann von der ICVM ausgef¨uhrt werden. Da StEAM Programme auf der Ebene des Objektcode pr¨uft,
ist es n¨otig, diese in einer kontrollierten Umgebung auszuf¨uhren. Eine solche Umgebung stellt eine
virtuelle Maschine zur Verf¨ugung. Wird ein Programm in einer virtuellen Maschine ausgef¨uhrt, so ist
es m¨oglich, Fehler zu erkennen. Hierf¨ur werden Fehlerzust¨ande definiert, die nicht von der virtuellen
Maschine erreicht werden d¨urfen.
StEAM ist in der Lage, ein kompiliertes C
++-Programm in die virtuelle Maschine zu laden, und
diese, auf Fehler zu untersuchen.
2.1.1
Fehlertypen
Folgende Fehler wedern von StEAM diagnostiziert:
Deadlocks beschreiben einen Zeitpunkt an dem alle Prozesse eines Programms blockiert sind. Ein
Prozess ist blockiert wenn er auf eine Ressource wartet.
http:
//ivm.sourceforge.net/
5
6
Kapitel 2. Der Software Modellpr ¨
ufer StEAM
char globalChar;
int globalBlocksize = 7;
int main(){
allocateBlock(blocksize);
}
void allocateBlock(int size){
void *memBlock;
memBlock = (void *) malloc(size);
}
Register der Maschine
Globale Variablen (ZERO initialisiert)
Globale Variablen (initialisiert)
Kompilierter Quellcode
Variablen der Methoden
Allozierte Speicherbl¨
ocke
Register
Stack
Text Section
Data Section
BSS Section
Memory Pool
Quellcode
Virtuelle Maschine
Abbildung 2.1: Abbildung der Variablen in einem Zustand
Assertion Violation werden erkannt indem die vom Programmierer gegebene Zusicherung ¨uberpr¨uft
wird. Den Variablen der boolschen Formel werden entsprechende Werte zugewiesen. Ist das
Ergebnis der Formel negativ so handelt es sich um einen Fehlerzustand.
Segmentation Fault entstehen beim Zugri
ff eines Modells auf einen nicht angeforderten Speicher.
2.2
Funktionsweise
2.2.1
Zust¨ande und Abschnitte
StEAM arbeitet mit Zust¨anden in einem Zustandsraum S . Bei einem Zustand (engl. state) s S
handelt es sich um ein Abbild der gesamten virtuellen Maschine zu einem bestimmten Zeitpunkt. Die
virtuelle Maschine besteht aus den in Abbildung 2.1 gezeigten Abschnitten (Reg, BSS, Data, Text,
Stack, MemPool
) (engl. sections).
Wird ein Zustand s als Abbild der virtuellen Maschine erzeugt, so wird von jedem Abschnitt eine
Kopie im Speicher abgelegt.
Enth¨alt ein Modell mehrere Prozesse (engl. threads), so muss ein Zustand dies widerspiegeln.
Die ICVM ist nicht in der Lage, mehrere Prozesse gleichzeitig auszuf¨uhren. In StEAM wird das
Programm auf mehreren virtuellen Maschinen simmuliert. Da jedoch nur eine virtuelle Maschine zur
Verf¨ugung steht, wird diese mehrfach verwendet. Die Abschnitte BSS, Data, Text, MemPool sind bei
allen Prozessen gleich, also werden nur die Abschnitte Reg und Stack einem Prozess zugeordnet.
Ein Zustand enth¨alt demnach einen Vektor aus Prozess-ID's
P
= p
1
, · · · , p
n
.
Jede p
id
, mit 1 id n besteht wiederum aus einer Kopie eines Register- und eines Stack-
Abschnittes der virtuellen Maschine, also:
p
id
= Reg, S tack .
Ein Zustand kann nun als Vektor
s
= P, BSS, Data, Text, MemPool
2.2. Funktionsweise
7
angesehen werden.
Da P wiedderum ein Vektor ist, der mehrere Abschnitte enth¨alt, beschreibt s die virtuelle Maschi-
ne zu |P| unterschiedlichen Zeitpunkten der Pr¨ufung.
Ist s ein Zustand und p
id
P s ein Paar aus Reg und Stack, so ordnet (s, p
id
) die virtuelle
Maschine einem eindeutigen Zeitpunkt zu.
Wird die virtuelle Maschine initialisiert, enth¨alt diese lediglich zwei Abschnitte: Die Register und
einen Stack. Bei dem Stack handelt es sich um einen Kellerspeicher in dem sowohl Variablen als auch
Informationen zur Ausf¨uhrung des Programms abgelegt werden k¨onnen. Register sind Speicherberei-
che, die direkt in dem Prozessor liegen und deshalb sehr kurze Zugri
ffszeiten haben. Die Gr¨oße beider
Sektionen ist einmal durch die Anzahl der Register im CPU Modell und einmal durch die Gr¨oße des
Stacks festgelegt.
L¨adt StEAM ein Modell in die virtuelle Maschine so werden die restlichen Abschnitte in der
folgenden Reihenfolge erzeugt:
· Der Text Abschnitt enth¨alt den Objektcode, dieser besteht aus Opcodes, den Maschinensprache-
befehlen die das Programm beschreiben.
· Globale Variablen, die bereits vor der Ausf¨uhrung des Programms mit einem Wert belegt wer-
den, liegen, direkt nach dem Text, in der Data Section.
· Die BSS Section enth¨alt alle globalen Variablen, denen zum Zeitpunkt der Initialisierung kein
Wert zugewiesen wurde.
· Der Memory Pool ist der einzige Abschnitt, der eine variable Gr¨oße w¨ahrend der Ausf¨uhrung
aufweist. Er wird mit einer Gr¨oße von 0 initialisiert und enth¨alt zur Laufzeit Speicherbereiche,
die das ausgef¨uhrte Programm anfordert.
Zus¨atzlich zu den Informationen, die die virtuelle Maschine beschreiben, enth¨alt ein Zustand wei-
tere Informationen, die zur Pr¨ufung ben¨otigt werden. So beinhaltet jeder Zustand eine Referenz auf
den Vaterzustand; den Dateinamen; die Zeile im Quellcode, die ausgef¨uhrt wurde, w¨ahrend der Zu-
stand generiert wurde und einen Hashwert. Dabei ist ein Hashwert das Ergebnis der Anwendung einer
Funktion k : S Z, die einen Zustand auf eine ganze Zahl abbildet.
Ein neuer Zustand entsteht am Ende einer jeden Zeile im Quelltext; An jeder nichtdeterministi-
schen Verzweigung, oder an einer speziellen, vom Programmierer im Quelltext gesetzten, Anweisung.
2.2.2
Ablauf einer Pr ¨
ufung
StEAM startet zuerst eine Instanz der virtuellen Maschine und l¨asst diese das Modell laden. Hierbei
wird laufend gepr¨uft, ob die "main" Routine erreicht wurde. Ist dies der Fall, so pausiert die virtuelle
Maschine und es wird ein Zustand erzeugt. Der so entstandene Zustand wird Initialzustand genannt,
und mit I bezeichnet. In I gilt |P|
= 1 da Prozesse erst in der "main"Methode gestartet werden
k¨onnen.
Erreicht die virtuelle Maschine eine Stelle im Programm, an der eine nichtdeterministische Ent-
scheidung gef¨allt werden soll, wird erneut pausiert. Erst jetzt greift StEAM signifikant in den Ablauf
des Programms ein. Wieder wird ein Zustand s erzeugt und der Programmablauf fortgef¨uhrt, aber nur
bis zur der Stelle an der ein Zustand s erzeugt worden ist. Nun entschiedet der gew¨ahlte Suchalgo-
rithmus welcher Weg verfolgt wird. Einerseits kann StEAM den Programmablauf, zum Zeitpunkt als
s
erzeugt wurde, auf einem weiteren Pfad fortf¨uhren, andrerseits kann s weiter ausgef¨uhrt werden.
Abbildung 2.2 verdeutlicht die Arbeitsweise des Modellpr¨ufers.
8
Kapitel 2. Der Software Modellpr ¨
ufer StEAM
initialisierung
Festplatte
Datei laden
"main" gefunden
Zustand auslesen
Initialzustand
speichern
Verzweigung gefunden
Zustand auslesen
speichern
Zustand
Verzweigung gefunden
Zustand auslesen
speichern
Zustand
Zustand laden
Zustand schreiben
StEAM
RAM
Ziel gefunden
"STOP" senden
Zustand auslesen
Zustand laden
Fehlerpfad ausgeben
"ausf¨
uhren" senden
"ausf¨
uhren" senden
"ausf¨
uhren" senden
Ausf¨
uhrbare
Virtuelle Maschine
Abbildung 2.2: Ablauf einer Pr¨ufung in StEAM
Details
- Seiten
- Erscheinungsform
- Originalausgabe
- Erscheinungsjahr
- 2007
- ISBN (eBook)
- 9783836616041
- DOI
- 10.3239/9783836616041
- Dateigröße
- 651 KB
- Sprache
- Deutsch
- Institution / Hochschule
- Technische Universität Dortmund – Informatik
- Erscheinungsdatum
- 2008 (Juli)
- Note
- 1,7
- Schlagworte
- modellprüfung parallelisierung modell checking software verifizierung
- Produktsicherheit
- Diplom.de
