Thema: Klassifikation von Online-Verifikationsmerkmalen

Thema: Klassifikation von Online-Verifikationsmerkmalen

Grunddaten

Titel Klassifikation von Online-Verifikationsmerkmalen
Beschreibung

Motivation:
Ziel der Softwareverifikation ist es, zu beweisen oder zu widerlegen, ob ein Programm eine Spezifikation erfüllt. Viele Ansätze erforschen dabei den Zustandsraum des Programms oder berechnen Prädikate zur Abstraktion des Zustandsraums.
Im Fall eines fehlerhaften Programmes, neigen jedoch viele bestehende Techniken dazu, ihre Zeit mit der Erkundung korrekter Teile des Programmes zu verschwenden.  Eine Anpassung des Suchstrategie oder das Wechseln zu einem anderen Verifikationsalgorithmus könnte in diesen Fällen von Vorteil sein. 
Mit der Hilfe von maschinellem Lernen soll ein Algorithmus entwerfen, der diese Situationen während der Verifikation erkennt.

Heimateinrichtung Department für Informatik
Art der Arbeit konzeptuell / theoretisch
Abschlussarbeitstyp Master
Autor Jan Frederik Haltermann, M. Sc.
Status abgeschlossen
Aufgabenstellung

Ziele & Inhalt der Arbeit:
Die Erfassung relevanter Daten und die Erstellung eines aussagekräftigen Datensatzes ist ein wesentlicher Bestandteil datengetriebener Algorithmen. Ziel dieser Arbeit ist daher die automatische Generierung eines Datensatzes zum Lernen von Verifikationsverhalten.
Zu diesem Zweck sollte eine Technik entwickelt und implementiert werden, die das Suchverhalte bzw. die generierten Prädikate eines Verifikationsalgorithmus analysiert, relevante Ereignisse identifiziert und die gesammelten Informationen in einem geeigneten Format speichert.
Der entwickelte Ansatz soll dann in das Verifikationsframework CPAchecker integriert werden, welches uns auch die notwendigen Verifikationsalgorithmen liefert. Letztendlich soll die neuartige Technik zur Erzeugung eines Datensatzes eingesetzt werden, während die Performanz und Qualität des Generierungsprozesses evaluiert werden soll. Außerdem sollen einfache Entscheidungsregeln zur Vorhersage der Erfolgswahrscheinlichkeit definiert werden.

Es ist auch möglich, das Thema im Rahmen einer Masterarbeit zu bearbeiten. In diesem Fall ist die Datengenerierung nur der erste Teil. In einem zweiten Teil soll ein maschineller Lernalgorithmus entwickelt werden, der die Erfolgswahrscheinlichkeit der aktuellen Verifikation voraussagt. Der Lernalgorithmus soll dann in Bezug auf Accuracy und Laufzeit evaluiert werden.

Voraussetzung
Erstellt 13.04.2022
Abgeschlossen am 25.01.2023