Download Bug-Finder Enhanced E

3.2. Heuristiken
3.1.4
14
Zustandsexpansion
Der Zustandsraum des Programmes wird von StEAM mit den folgenden Schritten erzeugt:
1. Einen der laufenden Threads auswählen
2. Inhalte der CPU-Register, des Stacks und der Variablen-Bereiche wiederherstellen (Kontextwechsel)
3. Eine einzelne Anweisung (oder automaren Block) ausführen (Zustandstransition)
4. Inhalte der CPU-Register, des Stacks und der Variablen-Bereiche einlesen, um den Nachfolgezustand
zu erzeugen
5. Neuen Zustand in Hash-Tabelle speichern, falls der Zustand neu ist
6. Die ersten fünf Schritte für alle laufenden Threads wiederholen
3.2
Heuristiken
Einer der wichtigsten Ansatzpunkte für die Effizienz-Verbesserung von StEAM ist die Verbesserung der
Such-Heuristiken. Eine Heuristik h gibt zu einem gegebenen Ausgangszustand s die geschätze Distanz h(s)
zu einem Fehlerzustand e an. Ein Problem beim Model Checking ist die Tatsache, dass fast nie der gesamte
Zustandsraum des Programms bekannt ist und deshalb nicht immer klar zu entscheiden ist, ob eine bestimmte
Heuristik zulässig oder konsistent ist.
3.2.1
Fehlerspezifische Heuristiken
Fehlerspezifische Heuristiken sind solche Heuristiken, die darauf zielen, einen Fehler eines bestimmten Typs
zu finden.
Most Blocked
Die Most-Blocked-Heuristik schätzt die Distanz mit der Anzahl der nicht-blockierten Prozesse. [ELL01],
[GV02]
Lock and Block
Die Lock-and-Block-Heuristik schätzt die Distanz als Anzahl der nicht-blockierten Prozesse plus Anzahl der
nicht blockierten Ressourcen.
Formelbasierte Heuristik
Die formelbasierte Heuristik schätzt die Distanz als Anzahl der Transitionen, die nötig sind, um eine gegebene
Formel wahr (falsch) werden zu lassen. Diese Heuristik kann von StEAM nicht ohne weiteres eingesetzt werden, weil es keine benannten Variablen(-namen), Funktionen(-namen) und Parameter(-namen) gibt, sondern
nur Speicheradressen.