Formale Spazifikationen
Korrekt - was heißt das überhaupt? (15.01.2025)
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.

 

Tags:

Formale Methoden Spezifikationen

Sarah Sallinger

Profile picture for user 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.

Skills:

Programming
,
Formal Methods
,
Logic
CAPTCHA
Diese Frage dient der Überprüfung, ob Sie ein menschlicher Besucher sind und um automatisierten SPAM zu verhindern.

    Weitere Blogbeiträge

    Datenschutzinformation
    Der datenschutzrechtliche Verantwortliche (Internet Privatstiftung Austria - Internet Foundation Austria, Österreich) würde gerne mit folgenden Diensten Ihre personenbezogenen Daten verarbeiten. Zur Personalisierung können Technologien wie Cookies, LocalStorage usw. verwendet werden. Dies ist für die Nutzung der Website nicht notwendig, ermöglicht aber eine noch engere Interaktion mit Ihnen. Falls gewünscht, können Sie Ihre Einwilligung jederzeit via unserer Datenschutzerklärung anpassen oder widerrufen.