Formal Methods meet Data Analysis
Umfang
Der Umfang der Arbeit lässt sich so anpassen, dass das Thema als Bachelorarbeit, Projektarbeit oder Masterarbeit bearbeitet werden kann.
Empfohlene Vorkenntnisse
- gute Kenntnisse in Java
- Kenntnisse zur Clusteranalyse (z.B. durch Besuch der Veranstaltung “Machine Learning”)
- grundlegende Kenntnisse in Compilerbau könnten hilfreich sein (z.B. durch Besuch der Veranstaltung “Compilerbau”)
- grundlegende Kenntnisse der B Sprache könnten hilfreich sein (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)
Problem
SimB ist ein Simulationstool mithilfe dessen man formale B Modelle mit Timing Eigenschaften und probabilistischen Eigenschaften simulieren kann. Basierend auf den resultierenden Ergebnissen kann man dann bestimmte (Timing/probabilistische) Verhalten mit statistischen Methoden wie z.B. Hypothesentest validieren. Clustering-Algorithmen sind Algorithmen in der Datenanalyse mithilfe dessen vorhandene Daten (umgewandelt in Vektorrepräsentationen) klassifiziert werden. Die Feature-Vektoren sind hierbei aus Machine Learning Modellen trainiert und generiert. Die Aufgabe dieser Arbeit besteht darin Clustering-Algorithmen in B zu modellieren, und mithilfe von SimB (anhand von Daten) zu simulieren. Ebenso soll untersucht werden, ob anhand der Simulationen bestimmte Anforderungen validiert werden können.
Minimalanforderungen
- Modellierung von Clustering Algorithmen
- Generierung von Simulationen aus vorhandenen Daten
Erweiterungen
- Validierung anhand von Anforderungen mit Anwendung auf Fallstudien
- ggf. Erweiterung von SimB
- ausführliche empirische Evaluation
Kontakt
Fabian Vu
Raum 25.12.02.50
Fabian.Vu@hhu.de