Home | english  | Impressum | Sitemap | KIT

Modellprüfung der parlamentarischen Verfahrensregel Robert's Rules of Order

Modellprüfung der parlamentarischen Verfahrensregel Robert's Rules of Order
Typ:Diplomarbeit
Betreuer:

Prof. P. H. Schmitt
David Faragó

Links:PDF

Umfeld

Mittels Modellprüfung lassen sich gewünschte Eigenschaften von nebenläufigen Systemen rigoros überprüfen. Auch Scheduling-Algorithmen wurden von Modellprüfern erfolgreich untersucht.
Deswegen soll in dieser Diplomarbeit ein scheduling-ähnlicher Algorithmus analysiert werden: Amerikas führende parlamentarische Verfahrensregel Robert's Rules of Order (RRO). Diese ist auch in Unternehmen und Vereinen weit verbreitet, um Meetings und Mediationen erfolgreich abzuwickeln. RRO ist – im Gegensatz zu vielen anderen Fallstudien und Benchmarks für Modellprüfer – sowohl erweiterbar als auch in der Praxis weit verbreitet.

 

Themenstellung

RRO wurde in [Jonker, 2007] zwar formalisiert, aber anschließend nur mittels Simulation analysiert. In dieser Arbeit soll RRO iterativ in Promela spezifiziert und mit dem Modellprüfer Spin verifiziert werden.
Die Spezifikation soll die funktionalen Aspekte von RRO enthalten, nicht jedoch die zeitliche Komponente. Anfangs soll nur das Wesentliche wie Rollen, Events und deren Priorität spezifiziert werden. In späteren Iterationen können Spezialfälle (z.B. Präemption, Spezialevents, Modifikation der Events oder gar der Regeln von RRO selbst) hinzugenommen werden.
Zuerst sollen Standardeigenschaften wie Terminierung, Deadlock- und Livelockfreiheit verifiziert werden. Danach sollen weitere Eigenschaften, z.B. dass jeder zu Wort kommen kann, in der temporalen Logik LTL formuliert und schließlich verifiziert werden.
Gewünschte Ergebnisse sind die Resultate und Erfahrungen der Verifikation selbst, aber auch die Beschreibung und Formalisierungen von RRO, die als Vorlage für zukünftige Fallstudien und Benchmarks für Modellprüfer dienen können.

 

Voraussetzungen

Sie sollten die Vorlesung „Formale Systeme" erfolgreich besucht haben. Vertiefende Kenntnisse in Spin und Promela wären von Vorteil, sind aber nicht notwendig, sofern Sie Interesse mitbringen, sich darin einzuarbeiten.

 

Sie bekommen

* eine Diplom- oder Masterarbeit mit Entfaltungsmöglichkeiten in Theorie und Praxis, oder Teile davon als Studien- oder Bachelorarbeit

* Zugang zum Institutspoolraum; Drucker; Kaffemaschine; ggf. Schlüssel für flexible Arbeitszeiten

* bei sehr guten Arbeiten die Möglichkeit zum wissenschaftlichen Publizieren.

 

Literatur 
Catholijn M. Jonker, Martijn C. Schut, Jan Treur, Pinar Yolum (2007). Analysis of meeting protocols by formalisation, simulation, and verification. Computational & Mathematical Organanization Theory 13 (3), 283-314.