TU Darmstadt / ULB / TUprints

Formal verification of multimodal dialogs in pervasive environments

Radomski, Stefan :
Formal verification of multimodal dialogs in pervasive environments.
Technische Universität, Darmstadt
[Ph.D. Thesis], (2015)

[img]
Preview
Text
Formal Verification of Multimodal Dialogs in Pervasive Environments.pdf
Available under Creative Commons Attribution Non-commercial No-derivatives 3.0 de.

Download (5MB) | Preview
Item Type: Ph.D. Thesis
Title: Formal verification of multimodal dialogs in pervasive environments
Language: English
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 common 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 effectively support multiple modalities as equals are addressed only insufficiently 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 specific 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 first applications are, indeed, starting to be commercialized, \eg as seen on IFA 2015 and even earlier fairs, their lack of a standardized approach is still a serious obstacle to commodification: Having a BMW tell a Buderus central heating system that a user expects a warm living room in 30 minutes is appreciated, but the overall usefulness is diminished if one needs to change into the VW only to check on the contents of a 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-specific components. The major contribution is a description of an automated transformation from these state-charts, given in an XML dialect onto the input language of a model-checker. This allows an interface designer to formally guarantee certain behaviors of the state-charts 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 verification, (ii) approaching a proof of correctness of the transformation via the official tests accompanying the state-chart description language and by (iii) showing applicability of the overall approach via transforming 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 of 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.

Alternative Abstract:
Alternative AbstractLanguage
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.German
Place of Publication: Darmstadt
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 20 Department of Computer Science > Telecooperation
Date Deposited: 11 Dec 2015 11:01
Last Modified: 11 Dec 2015 11:01
URN: urn:nbn:de:tuda-tuprints-51841
Referees: Radomski, M.Sc. Stefan
Refereed: 24 November 2015
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/5184
Export:
Actions (login required)
View Item View Item

Downloads

Downloads per month over past year