Ziel meines Projekts ist es, formale Methoden zu entwickeln, die bei der Suche und dem Beheben von Heisenbugs unterstützen. Im letzten Post habe ich Möglichkeiten beschrieben Systeme, die potentiell Heisenbugs enthalten, formal zu modellieren. Der nächste Meilenstein in meinem Projekt war es, formal zu definieren was es heißt, dass ein System, bzw. dessen Modell, einen Heisenbug enthält.

Beispiel: Getränkeautomat

Betrachten wir zunächst wieder das Getränkeautomaten Beispiel aus dem letzten Post, diesmal direkt in der Variante in der sich der Automat abhängig von der Uhrzeit unterschiedlich verhält:

Wenn die Uhrzeit nicht explizit im Modell betrachtet wird, ist es nicht möglich zu sagen, wie sich der Automat verhalten wird, wenn ein Getränk bestellt wird. Der Automat verhält sich also nichtdeterministisch. Dieser Nichtdeterminismus ist eine Grundvoraussetzung für das Entstehen von Heisenbugs. Tatsächlich kann man sagen, dass der Getränkeautomat einen Heisenbug enthält.

Nehmen wir an eine Nutzer:in kauft um 19:59 Uhr ein Getränk beim Automaten und um 20:01 Uhr versucht sie die Eingaben zu wiederholen, um ein zweites Getränk zu kaufen. Wenn der Automat aber nur bis 20:00 Uhr in Betrieb ist, wird die zweite Bestellung abgelehnt. Ist sich die Nutzer:in nicht bewusst, dass der Automat Betriebszeiten hat, wird sie das Verhalten als fehlerhaft einstufen. Ganz ähnlich verhält es sich bei Heisenbugs in Computerprogrammen.

Betrachten wir wiederum das ursprüngliche, deterministische, Modell, in dem Bestellungen immer angenommen werden, ist ein solcher Fehler nicht möglich.

Wie lassen sich die beiden Systeme also formal voneinander unterscheiden?

Properties

Formale Methoden definieren dafür Eigenschaften (engl. properties), die alle korrekten Modelle haben und alle fehlerhaften Modelle nicht haben. Die Eigenschaften werden als logische Formeln ausgedrückt. Im nächsten Schritt versucht man automatisch zu überprüfen, ob ein Modell die Eigenschaften erfüllt oder verletzt.

In den meisten Fällen, reicht es dafür Eigenschaften zu finden, die korrekte von fehlerhaften Ausführungen eines Systems unterscheiden. Formal wird eine Ausführung durch die genaue Liste der durchlaufenen Zustände und Übergänge beschrieben. In dem Getränkeautometen gibt es zum Beispiel die Ausführung a1: [Zustand 1, "Geld einwerfen", Zustand 2, "Getränk bestellen", Zustand 3], in der das Getränk erfolgreich ausgegeben wird, und die Ausführung a2:[Zustand 1, "Geld einwerfen", Zustand 2, "Getränk bestellen", Zustand 1], in der die Bestellung abgebrochen wird. Ein Modell gilt dann als korrekt, wenn alle möglichen Ausführungen im Modell die definierten Eigenschaften erfüllen.

Hyperproperties

Wie ich in meinem Projekt herausgefunden habe, reichen solch einfache Eigenschaften allerdings nicht aus um Heisenbugs zu charakterisieren. Um nachzuweisen, dass ein Heisenbug vorliegt müssen immer mindestens zwei Ausführungen betrachtet werden!

Eigenschaften, für die man mehrere Ausführungen betrachten muss, um eine Unterscheidung zu treffen, werden als Hyperproperties bezeichnet. Hyperproperties sind ein sehr aktives Forschungsfeld, z.B. werden unterschiedliche Logiken entwickelt, um Hyperproperties als logische Aussagen zu formalisieren und Algorithmen, um automatisch zu überprüfen, ob Systeme eine Hyperproperty erfüllen oder nicht.

Heisenbugs - Formale Definition

Basierend auf diesen Ergebnissen ist mein jüngster Erfolg im Projekt die Entwicklung einer logischen Formel, die als Hyperproperty definiert, was es bedeutet, dass ein Modell einen Heisenbug aufweist. Die Definition besagt, dass ein Modell einen Heisenbug aufweist, wenn es zwei Ausführungen gibt, die identische Nutzereingaben haben aber zu unterschiedlichen Ergebnissen führen. Im Getränkeautomaten Modell, gilt das zum Beispiel für Ausführungen a1 und a2. Beide Ausführungen haben Nutzereingaben "Geld einwerfen" und "Getränk bestellen". Während a1 in Zustand 3 endet, endet a2 aber in Zustand 1, was für die Benutzer:in zu unterschiedlichen Ergebnissen führt.