Umfang

Dieses Thema kann als Teil einer Projektarbeit oder im Rahmen einer Masterarbeit bearbeitet werden.

Problemstellung

Die B Methode ist eine formale Methode zur System- und Softwaremodellierung und -verifikation. Programme lassen sich abstrakt modellieren, als fehlerfrei beweisen und schrittweise verfeinern, bis eine Implementierungsebene erreicht wird, welche beispielsweise nach C Code übersetzt werden kann. Dies ist gerade in sicherheitskritischen Anwendungen relevant, in welchen Softwarefehler hohe Folgekosten, wie Menschenleben, mit sich bringen.

In vorangegangenen Arbeiten wurden bereits Klassifikatoren für Prädikate in klassischer B Syntax trainiert, welche pro Prädikat ein geeignetes Backend des ProB Model Checkers vorhergesagt haben, welcher bei uns am Lehrstuhl entwickelt wurde. Bei diesen Arbeiten wurden handgeschriebene Featuresets als auch Bildrepräsentationen genutzt, um die jeweiligen Machine Learning-Modelle zu trainieren. Während diese bereits gute Leistungen erzielt haben, sind wir an alternativen Repräsentationen von B Code interessiert.

Peng at el. (2015) präsentieren in ihrem Paper Building Program Vector Representations for Deep Learning einen Pretraining-Approach, welcher mittels eines neuronalen Netzes eine Vektorrepräsentation für Java-Code lernt.

Ziel dieser Arbeit soll es sein, solch eine Vektorisierung von B Code zu lernen und auf verschiedenen Klassifizierungstasks auszuwerten.

Empfohlene Vorkenntnisse

  • Python, Java
  • Grundlegendes Verständnis von Abstrakten Syntaxbäumen
  • Machine Learning
  • Neuronale Netze und Backpropagation

Kenntnisse über die B Methode sind initial nicht erforderlich, aber hilfreich.

Minimalanforderungen

  • Gelerntes Model, das Code Vektoren für B liefert
  • Auswertung der Repräsentationen über angewandte Machine Learning Tasks

Variationen/Erweiterungen

  • Vektoren für verschiedene Granularitäten von B Code (Einzelne Prädikate, Operationen, ganze Maschinen)
  • Performancevergleich mit code2vec
  • Vergleich mit anderen Feature Sets für B Code

Kontakt

Jannik Dunkelau
Raum 25.12.02.52 · jannik.dunkelau@hhu.de