Das Entwickeln und Bereitstellen von verlässlichen und kohärenten Benutzerschnittstellen in pervasiven Umgebungen welche durchdrungen sind mit einer Vielzahl von vernetzten Sensoren und Aktuatoren durch Anwendungsentwickler ist noch immer unzureichend unterstützt, vor allem in Hinsicht auf eine gemeinsame Methodologie und etablierte Stan- dards. Das breite Spektrum von Situationen in denen ein Benutzer in einer solchen Umgebung potentiell interagieren möchte bedingt, dass keine einzelne Interaktionsform jederzeit geeignet oder auch nur verfügbar ist. Nichtsdestotrotz erwarten Anwender zurecht, dass ihr Interaktionskontext unabhängig von der konkreten Wahl der Interaktionform bestehen bleibt.

Entsprechend lassen sich mehrere Anforderungen für eine Interaktionsbeschreibung in solchen Umgebungen ableiten, so zum Beispiel die Notwendigkeit zur Verteilung der Beschreibung, garantierte Kohärenz in Bezug auf den Interaktionskontext und die Notwendigkeit mehrere Interaktionsformen als gleichwertig zu behandeln. In den vergangenen 50 Jahren wurde eine Vielzahl von Ansätzen wissenschaftlich beschrieben, welche den Anspruch haben, entweder vereinzelte relevante Probleme zu lösen oder generell Interaktion in solchen Umgebungen in Form isolierter Forschungsprototypen umzusetzen. Bis zum heutigen Tag gibt es allerdings keinen umfassenden Ansatz, welcher eine breite Un- terstützung seitens der Industrie genießt und die einzelnen Lösungen in einem kohärenten Rahmenwerk interoperabel zusammenführt. Wenngleich erste kommerzielle Produkte bereits z.B. auf der IFA 2015 und auch früheren Messen vorgestellt wurden, so bleiben diese bislang doch Insellösungen, auf Produkte der Hersteller in einzelnen Konsortien begrenzt: So hilfreich es beispielsweise auch sein mag, wenn der BMW eines Anwenders der Buderus Zentralheizung daheim meldet, dass in 30 Minuten ein warmes Wohnzimmer erwarte wird, so ärgerlich ist es doch, wenn man in den VW des Partners wechseln muss, um zuvor noch den Inhalt des Miele Kühlschrankes abzufragen und dabei den gesamten Interaktionskontext verliert.

In der vorliegenden Dissertation werden wir im Detail den kürzlich standardisierten Ansatz des W3C für Interaktionbeschreibungen in pervasiven Umgebungen betrachten, worin modalitätsagnostische Zustandsübergangsdiagramme nach Harel modalitätsspezifische Komponenten kontrollieren, um im Zusammenspiel die Benutzerinteraktion formal zu beschreiben. Der wesentliche Beitrag dieser Dissertation ist hierbei eine automatische Transformation dieser Beschreibungen auf die Eingabesprache eines Werkzeuges für die Modellprüfung, um temporallogische Aussagen und Einschränkungen über eben diesen Interaktionbeschreibungen verifizieren zu können. Dieser Kernbeitrag wird hier- bei wie folgt evaluiert: (i) Die Teilmenge der Semantik der Interaktionsbeschreibungssprache, welche der formalen Verifikation zugänglich ist wird identifiziert, (ii) ein Beweis für die Korrektheit der Transformation wird durch die offiziellen Tests bezüglich ihrer funktionalen Anforderungen angenähert, (iii) die Anwendbarkeit des Gesamtansatzes wird am Beispiel einer nicht-trivialen Interaktionsbeschreibung eines kommerziellen Produktes gezeigt. Mehrere kleinere Beiträge ergänzen diesen Kernbeitrag: (i) ein Beweis der Turingvollständigkeit der gewählten Interaktionsbeschreibungssprache, sowie das Einbetten eines Kellerautomaten, (ii) eine Transformation auf eine semantisch äquivalente Zwischendarstellung als vereinfachte Zustandsmaschine durch geringfügige Erweiterungen des Standards, (iii) eine geschlossene Formel für die Obergrenze von Zuständen in der Zwischendarstellung als Zustandsmaschine, sowie (iv) mehrere Erweiterungen im Rahmen des Standards, um Anwendbarkeit und Ausdrucksfähigkeit der Interaktionsbeschreibungssprache in Bezug auf etablierte Modellierungstechniken zu verbessern.

All diese Arbeiten sind tatsächlich umgesetzt und ausprogrammiert in Form eines plattformunabhängigen, standardkonformen C++ Interpreters der betrachteten W3C Interaktionsbeschreibungssprache, welcher unter freier Lizenz quelloffen zur Verfügung steht. Dieser Interpreter wird bereits in kommerziellen, multimodalen Dialogsystemen eingesetzt und diente als eine der Referenzplattformen für den "Implementation and Report Plan" im Rahmen des W3C Prozesses eines Standards hin zu einer vollwertigen Empfehlung.