The combination of handheld devices and touch-based input modes has opened the door to more convenient and intimate interactions between humans and computers. Many of us carry them at all times, and perform tasks that are impractical with conventional computers. While this is without doubt a major advance in various aspects of usability, there are situations and contexts in which usability and convenience must be balanced against other, possibly more critical, requirements. The authors of this paper investigate the use of formal description methods for multi-touch interactions in airplane cockpits where the dependability of the interactions must satisfy requirements for safety-critical systems set by certification authorities.

Interactions can be viewed as languages: basic interaction events make up the elementary vocabulary, and they can be combined into sequences of activities according to the language syntax and given meaning through a mapping between an interaction sequence and the corresponding system command. Specifically for multi-touch interaction, such languages require a strong expressiveness since they need to be able to handle concurrent events (like gestures involving multiple fingers), and possibly multiple users.

The authors use interactive cooperative objects (ICOs) to describe the structural (static) and behavioral (dynamic) aspects of multi-touch interactions, illustrated by a formal description of the “pinch” gesture. In combination with existing tools, systems specified through ICO models can be evaluated with respect to invariant analysis, structural analysis, reachability graph analysis, and other properties.

In addition to knowing that, as airline passengers, our safety will not just rely on the trend of the day concerning “natural” and “intuitive” gestures, the ability to formally analyze certain aspects of human–computer interaction will hopefully move beyond safety-critical interaction spaces into the ones we deal with on a daily basis.