Formal Verification of Multimodal Dialogs in Pervasive Environments


At the end of 2012, the W3C Multimodal Interaction Working Group published a reference architecture for a distributed multimodal dialog system. In this architecture, State Chart XML is suggested to realise the responsibilities of dialog management for a coherent, modality-agnostic description of interaction. This talk will explore some of the formal properties of SCXML and present a largely automated transformation for a subset of SCXML documents onto the input language of a model checker, allowing to formally verify the dialog behavior of interactive systems with temporal logic.