Ziel meines Projekts ist es, formale Methoden zu entwickeln, die bei der Suche und dem Beheben von Heisenbugs unterstützen. Um formale Methoden anwenden zu können, braucht es ein formales Modell der untersuchten Systeme. Daher habe ich mich im ersten Schritt damit beschäftigt, wie man Systeme, die potentiell Heisenbugs enthalten, am besten modellieren kann.

Ansätze zur formalen Modellierung

Grundsätzlich werden drei Ansätze unterschieden, mit denen man die Funktionsweise von Computerprogrammen mathematisch modellieren kann.

1. Denotational: Hier wird ein Programm mit mathematischen Funktionen beschrieben, die Eingabewerte auf Ausgabewerte abbilden.
2. Operational: Hier wird ein Programm beschrieben durch die Schritte, die zu seiner Ausführung erforderlich sind.
3. Axiomatisch: Hier wird das Programm beschrieben durch Schlussregeln, die festlegen, wie man aus Eigenschaften, die vor der Ausführung gelten, Eigenschaften, die nach der Ausführung gelten, ableiten kann.

Operationale Modellierungen haben den Vorteil, dass sie besonders nahe an der tatsächlichen Implementierung des Systems sind. Wenn man bei einer Analyse des operationalen Modells entdeckt, dass Fehler vorliegen, kann man die Ausführungsschritte durchgehen und herausfinden, was den Fehler verursacht. Deshalb sind sie auch für die Suche nach Heisenbugs und deren Ursachen am besten geeignet.

Operationale Modelle

Operationale Modelle beschreiben ein System durch eine Menge von Zuständen sowie Regeln, die definieren, wie das System bei einer bestimmten Eingabe von einem Zustand in den nächsten übergeht. Bei Computerprogrammen wird der Zustand durch den Wert von Variablen definiert und die Übergänge durch Algorithmen (link) vorgegeben. Aber auch viel einfachere Systeme basieren auf diesem Prinzip. Denken wir zum Beispiel an einen Getränkeautomaten, bei dem die Nutzer:in Geld einwirft und ein Getränk auswählt oder gegebenenfalls die Bestellung abbricht und das Geld zurückverlangt. Der Automat hat folgende Zustände:

1. Der initiale Zustand, in dem weder Geld eingeworfen noch ein Getränk gewählt wurde.
2. Der Zustand, in dem Geld eingeworfen wurde und der Automat darauf wartet, dass der Benutzer ein Getränk auswählt.
3. Der Zustand, in dem ausreichend Geld eingeworfen und ein Getränk ausgewählt wurde und somit das Getränk zubereitet und ausgegeben wird.

Die Übergänge zwischen den Zuständen werden kontrolliert durch die Benutzereingaben "Geld einwerfen", "Getränk auswählen" und "Abbruch". Einige, aber nicht alle Übergänge sind von externen Eingaben abhängig. Das formale Modell lässt sich wie folgt grafisch darstellen:

Natürlich kann das Modell weiter verfeinert werden, um beispielsweise den verfügbaren Bestand an Getränken und die Preise der Getränke zu berücksichtigen, aber dies ist ein grundlegendes Beispiel dafür, wie ein formales Modell eines Getränkeautomaten aussehen könnte.

Nichtdeterminismus

Eine weitere wichtige Frage bei der Modellierung von Systemen mit Heisenbugs ist, wie man die Unvorhersehbarkeit des Verhaltens am besten im Modell abbilden kann.

Im beschriebenen Getränkeautomaten wird das Verhalten des Systems durch die Eingaben eindeutig festgelegt. Jeder Zustand hat für jede Eingabe genau einen möglichen Nachfolger. Man spricht daher von einem deterministischen System. Nehmen wir nun aber an, der Getränkeautomat ist so konfiguriert, dass er nur während bestimmter Betriebszeiten Getränke ausgibt. Außerhalb der Betriebszeiten nimmt er keine Bestellungen an, sondern gibt das Geld direkt wieder aus. Das neue Modell sieht dann wie folgt aus:

Der Getränkeautomat kann auf Bestellungen also auf zwei unterschiedliche Arten reagieren. Wenn, wie in diesem Beispiel, ein Zustand für dieselbe Eingabe unterschiedliche Nachfolgezustände haben kann, spricht daher von Nichtdeterminismus. Nichtdeterminismus ist eine nötige Grundvoraussetzung dafür, dass Heisenbugs auftreten können.

Zusammenfassend haben wir herausgefunden, dass man für die Suche nach Heisenbugs am besten operationale Modelle verwendet, die Nichtdeterminismus darstellen können.