Analyse des Designs von Git / Mercurial mit Hilfe von B
Umfang
Je nach Umfang kann das Thema sowohl als Bachelorarbeit, Teil einer Projektarbeit oder Masterarbeit bearbeitet werden.
Empfohlene Vorkenntnisse
- Kenntnisse der B Sprache (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)
Problem
In ihrem Paper “What’s Wrong with Git? A Conceptual Design Analysis” haben Santiago Perez De Rosso und Daniel Jackson das konzeptuelle Modell hinter Git (Staging Area, Branching, ….) in Alloy modelliert und analysiert um die Ursachen für die hohe Komplexität von Git zu identifizieren.
Eine ähnliche Analyse könnte mit Hilfe der B-Methode durchgeführt werden. Dabei könnte das Modell hinter Git oder Mecurial analysiert werden. Auch wäre ein Vergleich der Modelle von Git / Mercurial und Darcs interessant.
Minimalanforderungen
- formales Modell von Git oder Mercurial
- Analyse des Modells auf ein paar Szenarien
Erweiterungen
- Aufdeckung von problematischen Szenarien
- Beweisen von Eigenschaften des Modells
- Visualisierung des Modells und interaktive Ausführung
- Anbindung des formalen Modells an echte Git/Mercurial Verzeichnisse
Kontakt
Professor Michael LeuschelRaum 25.12.02.60 · michael.leuschel@hhu.de