[Back]


Doctor's Theses (authored and supervised):

S. Radomski:
"Formal Veri cation of Multimodal Dialogs in Pervasive Environments";
Supervisor, Reviewer: G. Kappel, M. Mühlhäuser; Institut für Softwaretechnik und Interaktive Systeme, 2015; oral examination: 2015-11-24.



English abstract:
Das Entwickeln und Bereitstellen von verl asslichen und koh arenten Benutzerschnittstellen in pervasiven Umgebungen
mit einer Vielzahl von vernetzten Sensoren und Aktuatoren durch Anwendungsentwickler ist noch immer unzureichend
unterst utzt, vor allem in Hinsicht auf gemeinsame Methodologien und etablierte Standards. Das breite Spektrum
von Situationen in denen ein Benutzer in einer solchen Umgebung potentiell interagieren m ochte bedingt, dass keine
einzelne Interaktionsform jederzeit geeignet oder auch nur verf ugbar ist. Nichtsdestotrotz erwarten Anwender zurecht,
dass ihr Interaktionskontext unabh angig von der konkreten Wahl der Interaktionform bestehen bleibt.
Entsprechend lassen sich mehrere Anforderungen f ur eine Interaktionsbeschreibung in solchen Umgebungen ableiten,
so zum Beispiel die M oglichkeit zur Verteilung der Beschreibung, garantierte Koh arenz 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 osen oder generell Interaktion in pervasiven Umgebungen in Form isolierter
Forschungsprototypen umzusetzen. Bis zum heutigen Tag gibt es allerdings keinen generellen Ansatz, welcher eine
breite Unterst utzung seitens der Industrie geniesst und die einzelnen L osungen in einem koh arenten Rahmenwerk interoperabel
zusammenf uhrt. Wenngleich erste kommerzielle Produkte bereits z.B. auf der IFA 2015 und auch fr uheren
Messen vorgestellt wurden, so bleiben diese bislang doch Insell osungen, auf Produkte der Hersteller in einzelnen Konsortien
begrenzt: So hilfreich es beispielhaft auch sein mag, wenn mein BMW meiner Buderus Zentralheizung daheim
meldet, dass ich in 30 Minuten ankomme und ein warmes Wohnzimmer erwarte, so argerlich ist es doch, wenn ich in
den VW meiner Frau wechseln muss, um zuvor noch den Inhalt unseres Miele K uhlschrankes abzufragen und dabei
auch noch meinen gesamten Interaktionskontext verliere.
In der vorliegenden Dissertation werden wir im Detail den k urzlich standardisierten Ansatz des W3C f ur Interaktionbeschreibungen
in pervasiven Umgebungen betrachten, worin modalit atsagnostische Zustands ubergangsdiagramme
nach Harel modalit atsspezi sche Komponenten kontrollieren, um im Zusammenspiel die Benuzterinteraktion
formal zu beschreiben. Der wesentliche Beitrag dieser Dissertation ist hierbei eine automatische Transformation dieser
Beschreibungen auf die Eingabesprache eines Werkzeuges f ur die Modellpr ufung, um temporallogische Aussagen und
Einschr ankungen uber eben diesen Interaktionbeschreibungen veri zieren zu k onnen. Dieser Kernbeitrag wird hierbei
wie folgt evaluiert: (i) Die Teilmenge der Semantik der Interaktionsbeschreibungssprache, welche der formalen
Veri kation zug anglich ist wird identi ziert, (ii) ein Beweis f ur die Korrektheit der Transformation wird durch die
o ziellen Tests bez uglich ihrer funktionalen Anforderungen angen ahert, (iii) die Anwendbarkeit des Gesamtansatzes
wird am Besipiel einer nicht-trivialen Interaktionsbeschreibung eines kommerziellen Produktes gezeigt.
Mehrere kleinere Beitr age erg anzen diesen Kernbeitrag: (i) ein Beweis der Turingvollst andigkeit der gew ahlten Interaktionsbeschreibungssprache,
sowie das Einbetten eines Kellerautomaten, (ii) eine Transformation auf eine semantisch
aquivalente Zwischendarstellung als vereinfachte Zustandsmaschine durch geringe Erweiterungen des Standards,
(iii) eine geschlossene Formel f ur die Obergrenze von Zust anden in der Zwischendarstellung als Zustandsmaschine,
(iv) sowie mehere Erweiterungen im Rahmen des Standards, um Anwendbarkeit und Ausdrucksf ahigkeit der Interaktionsbeschreibungssprache
in Bezug auf etablierte Modellierungstechniken zu verbessern.
All diese Arbeiten sind tats achlich umgesetzt und ausprogrammiert in Form eines plattformunabh angigen, standardkonformen
C++ Interpreters der betrachteten W3C Interaktionsbeschreibungssprache, welcher unter freier Lizenz
zur Verf ugung steht. Dieser Interpreter wird bereits in kommerziellen, multimodalen Dialogsystemen eingesetzt und
diente als eine der Referenzplattformen f ur den \Implementation and Report Plan" im Rahmen des W3C Prozesses
eines Standards hin zu einer vollwertigen Empfehlung.

German abstract:
Providing reliable and coherent interfaces to end-users in pervasive environments with a wealth of connected sensors
and actuators is still an area with little to no support in terms of methodologies and established standards. The wide
range of diverse situations, in which interaction in these environments potentially takes place, prevents any single
means of interaction to form a predominant approach. While one class of interaction devices, might be well suited in
one given situation, it might be wholly inapplicable in another. Yet, users rightfully expect an interaction session to
continue coherently when their situation calls for a change with regard to their means of interaction.
The entailing classes of new requirements for user interfaces, such as distributed interaction logic, guaranteed
coherence with regard to the state of the overall interaction and the necessity to e ectively support multiple modalities
as equals are addressed only insu ciently by the established approaches to model user interface that are popular today.
Much research has already been conducted in the last 50 years to develop various conceptualizations applicable to
model distributed, coherent, and / or multimodal interfaces, but so far this only lead to a plethora of isolated research
prototypes and solutions to speci c problems in the design space, with no solution having developed the inertia to
succeed in establishing a permanent foothold in industry-supported, commercial end-user applications. While rst
applications are, indeed, starting to be commercialized, e.g. as seen on IFA 2015 and even earlier fairs, their lack
of a standardized approach is still a serious obstacle to commodi cation: Having my BMW tell my Buderus central
heating system at home that I will arrive in 30 minutes and expect a warm living room is appreciated, but the overall
usefulness is diminished if I need to change into the VW of my wife to check on the contents of our Miele fridge, losing
all interaction context in between.
In this thesis, we will elaborate on an approach, recently recommended by the \W3C Multimodal Interaction
Working Group", to express the interaction logic of user interfaces in pervasive environments as modality-agnostic,
nested state-charts controlling modality-speci c components. The major contribution is a description of an automated
transformation from these state-charts, given in a XML dialect onto the input language of a model-checker. This allows
an interface designer to formally guarantee certain behaviors of the state-chart and thereby properties of the interaction
described within. This core contribution is evaluated by (i) identifying the subset of state-chart semantics applicable
for formal veri cation, (ii) approaching a proof of correctness of the transformation via the o cial tests accompanying
the state-chart description language and by (iii) showing applicability of the overall approach via transforming and
selectively verifying a non-trivial state-chart employed to describe the user interface of a commercial consumer product.
Several smaller contributions of this thesis include (i) a proof of the turing-completeness of the employed state-chart
semantics as well as the embedding of a push-down automaton, (ii) a transformation onto semantically equivalent
state-machines in a slightly extended variant of the state-chart description language with (iii) a closed-form upper
bound for the number states in the state-machine (iv) and extensions to improve the applicability and expressiveness
of the proposed state-chart formalism with regard to other established dialog modeling techniques.
All of this is actually implemented in a platform-independent C++ state-chart interpreter, compliant to the respective
W3C standards and accompanied by various tools available under a free open-source license. The interpreter is
already used in commercial deployments of multimodal dialog systems and was submitted as part of the implementation
and report plan for the respective W3C recommendation.

Keywords:
W3C, interactions, prototypes

Created from the Publication Database of the Vienna University of Technology.