Formal verification in the design of gestural interaction

This paper shows how formal modelling can be used in the design of a dynamic gesture language defined by sequences of poses. It discusses two models at different levels of abstraction dealing with important usability issues of the language such as ambiguity and overlap in the recognition of gestures. An approach to make the language more resilient to intermediate poses is evaluated based on a timed extension of the model. A tool providing model checking for hybrid automata is used to perform systematic and automatic analysis.