Modellierung, Validierung und Ausführung von Normsetzungsprozessen (Modellierung)

Teilprojektleiter: Prof. Dr. Michael Leuschel

Erkenntnisinteresse und Fragestellung

Für internetvermittelte kooperative Normsetzung muss das technische System an den jeweiligen spezifischen Einsatzbereich angepasst werden. Insbesondere muss die technische Umsetzung einzelner Module so realisiert werden, dass diese mit geringem Aufwand adaptiert, konfiguriert und kombiniert werden können. Gleichzeitig muss gewährleistet sein, dass das technische System allgemeine Anforderungen, wie etwa Skalierbarkeit, Transparenz und Sicherheit, erfüllt.

Dieses Teilprojekt verwendet formaler Modellierung, um die genannten Herausforderungen zu lösen. Modelliert werden sowohl der rechtliche und organisatorische Kontext des Einsatzbereiches, als auch die Funktionalität ausgewählter Module. Mit formalen Analysen wird überprüft, ob die einzelnen Module untereinander kompatibel sind, und ob globale Anforderungen, wie z.B. Fairness des Aggregationsprozesses, Datenschutz oder Sicherheit, erfüllt werden. Ein wichtiger Aspekt dieses Teilprojektes ist, dass die formalen Modelle ausgewählter Module entweder direkt ausgeführt werden oder maschinell in ausführbare Programme kompiliert werden. Modelle auf hohem Abstraktionsniveau ersetzen konventionelle Programmierung, dadurch wird die Transparenz und Flexibilität der entsprechenden Module gesteigert.

Vor diesem Hintergrund lauten die zentralen Fragestellungen des Teilprojektes:

  • Wie lassen sich die zahlreichen Anforderungen und die Module eines flexiblen technischen Systems zur internetvermittelten kooperativen Normsetzung formal spezifizieren?
  • Wie kann geprüft werden, ob die Anforderungen konfliktfrei mit den bestehenden Modulen realisierbar sind?
  • Kann aus den Anforderungen und der technischen Spezifikation der Module automatisch ein für den jeweiligen Einsatzbereich angepasstes technisches Gesamtsystem erzeugt werden?

Forschungsansatz und geplantes Vorgehen

Mit diesem Teilprojekt wird der im Gesamtprojekt entwickelte Baukasten strukturiert, die einzelnen Module modelliert, zusammengeführt und verifiziert. Das Teilprojekt bildet die Schnittstelle zwischen dem Teilprojekt Technik und den anderen Teilprojekten. Es stellt eine gemeinsame formale Sprache zur Verfügung, in der die einzelnen Teilprojekte und Module untereinander kommunizieren können. Ein weiteres, auf die Interaktion mit dem System bezogenes, Ziel ist es dem Endanwender die Struktur und die Ausführung des Systems transparent darzustellen. Zusammenfassend betrachtet stellt dieses Teilprojekt sicher, dass das entwickelte technische System leicht an neue Kontexte angepasst werden kann. Das Teilprojekt ist in zwei Bereiche gegliedert:

Modellentwicklung und –validierung. Die Modellierung soll in der Sprache B erfolgen, einer formalen logik-basierten Sprache. B hat sich in verschiedenen Bereichen bewährt, unter Anderem um verteilte Systeme, Business-Prozesse oder UML Modelle, wie sie zum Teil bei adhocracy vorliegen, zu beschreiben. B zeichnet sich durch Datentypen höherer Ordnung und eine umfassende Werkzeugunterstützung aus. In diesem Projekt sollen die Modelle mit dem Werkzeug ProB validiert werden. Von besonderem Interesse ist hier die Zusammenarbeit mit dem TP Präferenzaggregation, um sowohl für verschiedene neue Verfahren automatisch Probleme, wie z.B. Manipulationsmöglichkeiten, aufzudecken als auch die Skalierbarkeit von ProB für Bedingungen über Datentypen höherer Ordnung weiter voranzutreiben. Die Rückmeldungen der Analysen und Simulationen müssen dabei auch für nicht Experten verständlich sein, was durch eine Verknüpfung von B Modellen mit natürlichsprachlichen Anforderungen durch Verwendung des Werkzeugs ProR[1] ermöglicht werden soll.

Ausführung. Für das Gesamtprojekt wird ein Softwaresystem auf Basis von adhocracy entstehen. Adhocracy  wurde in der Programmiersprache Python entwickelt, daher bietet es sich an B in Python und adhocracy einzubetten. Dies ist eines der Ziele dieses Teilprojekts. PyPy ist eine alternative Implementierung der Programmiersprache Python, die durch die Verwendung von Just-in-Time Compilation besonders effizient ist. Mit Hilfe der PyPy Technologie soll sichergestellt werden, dass die Einbettung von B in Python und adhocracy effizient ausgeführt werden kann.


[1] http://www.eclipse.org/rmf/pror/ [10.05.2012]