
Förderjahr 2022 / Stipendien Call #17 / ProjektID: 6428 / Projekt: Automated Diagnosis of Heisenbugs
Wie im Blogpost zur formalen Definition von Heisenbugs beschrieben, sprechen wir von Heisenbugs wenn es in einem System zwei unterschiedliche Ausführungen gibt, die durch identische Nutzereingaben entstehen und bei denen eine Ausfühurung korrekt und eine Ausführung fehlerhaft ist. In diesem Zusammenhang stellt sich die Frage, wie man korrekte von fehlerhaften Ausführungen unterscheiden kann. Dieser Frage wollen wir in diesem Blogpost auf den Grund gehen.
Im Blogpost zur formalen Definition wird erklärt, dass formale Methoden darauf basieren, bestimmte Properties, also Eigenschaften, in Systemen zu überprüfen. Im Fachjargon werden diese Eigenschaften auch formale Spezifikationen genannt. Ausführungen sind genau dann korrekt, wenn sie eine gewisse Eigenschaft, die als formale Spezifikation dient, erfüllen.
In der Forschung im Bereich formale Methoden, wird meist davon ausgegangen, dass formale Spezifikationen von Systementwickler:innen oder Nutzer:innen bereitgestellt werden und Analysemethoden direkt darauf aufbauen können.
Die herausfordernde Suche nach passenden Spezifikationen
Wie sich herausgestellt hat, ist das Entwickeln einer solchen formalen Spezifikation, die genau das beabsichtigte Systemverhalten einfängt, in der Praxis jedoch alles andere als trivial. Betrachten wir dazu das Beispiel des Getränkeautomaten, das in einem verherigen Blogpost vorgestellt wurde. Eine Eigenschaft für die Spezifikation könnte in etwa lauten:
"Wenn Geld eingeworfen wird und ein Getränk bestellt wird, wird auch ein Getränk ausgegeben."
Während diese Eigenschaft auf den ersten Blick schlüssig erscheinen mag, erfasst sie das gewünschte Systemverhalten nicht vollständig. So berücksichtigt die Eigenschaft zum Beispiel nicht, welches Getränk ausgegeben wird. Eine verfeinerte Version könnte folgendermaßen aussehen:
"Wenn Geld eingeworfen wird und ein bestimmtes Getränk bestellt wird, wird genau dieses Getränk ausgegeben."
Ein zusätzliches Teilprojekt
Da jede Analyse nur so gut ist wie die Spezifikation, auf der sie basiert, ist es entscheidend, möglichst präzise Spezifikationen zu verwenden. Aus diesem Grund habe ich beschlossen, dieses Thema als zusätzliches Teilprojekt in meiner Arbeit genauer zu untersuchen. Insbesondere arbeite ich Methoden aus, die helfen sollen, den iterativen Entwicklungsprozess von formalen Spezifikationen in die richtige Richtung zu lenken. Der nächste Blogpost wird unsere ersten Forschungsergebnisse zu diesem Thema vorstellen.
Sarah Sallinger

I am a PhD student in the Rigorous Systems Engineering group at TU Wien. I am driven by the desire to better understand the inner workings of complex computer systems and I want to develop tools that help in this process. My research interests broadly span the fields of computer aided verification, program analysis and automated bug detection and diagnosis.