Wintersemester 2016/2017

PSE – Gruppe II

Entwicklung eines Werkzeugs zur Analyse formaler Eigenschaften von Wahlverfahren

Prof. Dr. Bernhard Beckert
Sarah Grebing, Michael Kirsten

Projektinhalt

Hintergrund

Stimmzettel einer Bundestagswahl

Ein Wahlverfahren oder auch Wahlauszählverfahren ist eine Methode, individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren. Häufig ist ein solches Verfahren Teil des grundsätzlichen demokratischen Verfahrens und stellt einen wichtigen Faktor für die Glaubwürdigkeit der gesamten Wahl dar. Es ist also unerlässlich, dass Wahlverfahren wie vorgesehen funktionieren, also beispielsweise den in einer rechtlich verbindlichen Verfassung spezifizierten Anforderungen genügen. Existierende Wahlverfahren haben ungewollte und manchmal überraschende Eigenschaften aufgewiesen (z. B. negative Stimmgewichte bei den Bundestagswahlen in Deutschland). Für kompliziertere, neu-designte Wahlverfahren, die mithilfe der Unterstützung von Computern im Stimmauszählverfahren ermöglicht werden, ist es wahrscheinlich, dass sich solche Sachverhalte ebenso abzeichnen.

Im Rahmen von Forschungskollaborationen innerhalb der COST Action IC1205 "Computational Social Choice" entwickelt unsere Forschungsgruppe logik-basierte Verfahren, um Wahlverfahren auf formale Eigenschaften zu prüfen, sowie die Durchführung konkreter Wahlen mittels logik-basierter Methoden zu unterstützen.

Aufgabenbeschreibung

Stimmzettel einer australischen Präferenzwahl

Ziel dieses Projekts ist die Planung und Implementierung eines Wahl-Analyse-Tools, das für unterschiedliche Algorithmen zur Berechnung eines Wahlergebnisses verwendbar ist. Für einen Benutzer soll es dabei möglich sein, ein solches Wahlverfahren auf verschiedene Aspekte hin zu analysieren. Das Tool soll es erlauben, Annahmen und Aussagen als C-Ausdrücke bezüglich Ein- und Ausgabe sowie auch zwischen verschiedenen Ein- und Ausgaben (sogenannte relationale Eigenschaften) zu spezifizieren, die im Hintergrund von einem Verifikationswerkzeug geprüft werden.

Auszählen von Stimmzetteln einer Wahl

Dieses Werkzeug wird als Black-Box verwendet, wobei es das zu schreibende Wahl-Analyse-Tool sowohl erlaubt, selbst-geschriebene Formeln in geeigneter Form an das Verifikationswerkzeug weiterzugeben, als auch die Ausgabe des Werkzeugs (entweder ein Gegenbeispiel oder eine Erfolgsnachricht) an das Analyse-Tool weiterzuleiten. Weiterhin soll es möglich sein, das Verifikationswerkzeug für eine Liste von Eingaben im Stapelverarbeitungs-Modus anzusteuern und abzufragen.

Das Tool soll es außerdem erlauben, entsprechende Wahlverfahren selbst in der Programmiersprache C zu schreiben, auf die geeignete Form zu prüfen und an das Verifikationswerkzeug weiterzugeben. Insbesondere sollen vom Verifikationswerkzeug ausgegebene Gegenbeispiele anschaulich dargestellt werden, wobei auch relationale Eigenschaften berücksichtigt werden sollen, in denen zwei oder mehr Läufe gegenübergestellt werden. Zusätzlich soll es das Analyse-Tool erlauben, das Wahlverfahren mit konkreten Eingabedaten auszuführen.


Hinweise und Erwartungen

  • Aktives Source Code Management mittels eines Versionsverwaltungssystems
  • Automatische Softwaretests
  • Kontinuierliche Integration
  • Anwendung bzw. Einhaltung von Design Patterns, Best Practices, und Style Konventionen
  • Kommentierter Quellcode, sowie Dokumentation und Testprotokolle

Wichtige Leistungsanforderungen

  • Spezifische Funktionalitäten
    • Eingabemöglichkeit für Wahlverfahren als C Programm
    • Eingabemöglichkeit für Annahmen und Aussagen als C-Ausdrücke (mit Makros) über Ein- und Ausgabe, relationaler und funktionaler Art
    • Eingabemöglichkeit konkreter Wahldaten zu Testzwecken
    • Graphische Darstellung funktionaler und relationaler Gegenbeispiele
    • Eingabemöglichkeit unterschiedlicher Schranken zur Verifikation
    • Auswahlmöglichkeit zwischen mindestens drei verschiedenen Arten der Stimmabgabe (einfache Auswahl, Ranking, Zustimmung)
    • Unterstützung von Ein-Personen- und Parlamentswahl
  • Insgesamte Tool-Eigenschaften
    • Usability und einfache Installation
    • Erweiterbarkeit, Übersichtlichkeit und Modularität
    • Robustheit gegenüber fehlerhaften Eingaben

Gruppentermine

Abgabe der Artefakte: Jeweils montags 11:00 Uhr vor dem Kolloquium.

Termin Zeit Inhalt Ort
27.10.2016 15:45 Uhr Auftaktveranstaltung -- Projektvorstellung HSaF (Geb. 50.35)
08.11.2016 13:00 Uhr Erstes Gruppentreffen -- Folien Geb. 50.34, Raum 211
10.11.2016 13:00 Uhr Einführung: Logik, Programmverif., Bounded Model Checking & CBMC
Folien, CBMC-Beispieleigenschaften
Geb. 50.34, Raum 211
16.11.2016 12:30 Uhr Gruppentreffen -- Aufgabenstellung, Pflichtenhefts-Blatt, Weitere Wahlverfahren Geb. 50.34, Raum 201
23.11.2016 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
30.11.2016 11:30 Uhr Gruppentreffen -- Entwurfs-Blatt Geb. 50.34, Raum 201
05.12.2016 11:00 Uhr Abgabe Pflichtenheft svn-repository
07.12.2016 11:30 Uhr Kolloquium Pflichtenheft Geb. 50.34, Raum 201
14.12.2016 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
21.12.2016 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 211
24.12.2016  –  06.01.2017 Weihnachtspause
11.01.2017 11:30 Uhr Gruppentreffen -- Implementierungs-Blatt Geb. 50.34, Raum 201
16.01.2016 11:00 Uhr Abgabe Entwurf svn-repository
18.01.2016 11:30 Uhr Kolloquium Entwurf Geb. 50.34, Raum 201
25.01.2017 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
01.02.2017 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
08.02.2017 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
13.02.2017 11:00 Uhr Abgabe Implementierung svn-repository
15.02.2017 11:30 Uhr Kolloquium Implementierung -- Qualitätssicherungs-Blatt Geb. 50.34, Raum 211
16.02.2017  –  26.02.2017 Klausurenpause
01.03.2017 11:30 Uhr Gruppentreffen Geb. 50.34, Raum 201
07.03.2017 14:00 Uhr Gruppentreffen Geb. 50.34, Raum 211
16.03.2017 14:00 Uhr Gruppentreffen -- Lehrevaluationsauswertung, Abnahme-Blatt Geb. 50.34, Raum 211
20.03.2017 11:00 Uhr Abgabe Qualitätssicherung svn-repository
22.03.2017 11:30 Uhr Kolloquium Qualitätssicherung Geb. 50.34, Raum 211
30.03.2017 14:00 Uhr Interne Abnahme Geb. 50.34, Raum 211
07.04.2017 10:30 Uhr Abschlusspräsentaton Max-Syrbel-Saal (IOSB)
(Fraunhoferstraße 1)

Weiterführende Informationen und Materialien