Multimodal User Interfaces (MUIs) offer to users the possibility to interact with systems using one or more modalities. In the context of mobile systems, this will increase the flexibility of interaction and will give the choice to use the most appropriate modality. These interfaces must satisfy usability properties to guarantee that users do not reject them. Within this context, we show the benefits of using formal methods for the specification and verification of multimodal user interfaces (MUIs) for mobile systems. We focus on the usability properties and specifically on the adaptability property. We show how transition systems can be used to model the MUI and temporal logics to specify usability properties. The verification is performed by using fully automatic model-checking technique. This technique allows the verification at earlier stages of the development life cycle which decreases the high costs involved by the maintenance of such systems.
TopIntroduction
The development of new interactive devices and technologies such as speech recognition, visual recognition and gesture recognition enriches User Interfaces (UIs) interactions and allows user to interact with systems in a more natural way. Multimodal User Interfaces (MUIs) are characterized by several possibilities, defined as modalities, to interact with the systems. The users can choose the most appropriate modality for a given situation which allows them interacting with systems anytime and anywhere. They can also use more than one modality to accomplish a given task. For example, they can use speech and gesture to move a graphical object from an initial to a target position. This was studied by R. Bold in (Bold, 1980) through the command “Put That There” using speech and gesture modalities. The gesture is used to indicate the initial and the target positions of the object to be moved.
With the emerging technologies such as ambient, intelligent and ubiquitous or pervasive computing, various input and output modalities are necessary to enable efficient interaction with these systems. The latter are mainly characterized by the multiplicity of users, variety of use contexts and user mobility. At present, MUIs are developed for many of such systems using mobile devices like PDAs and mobile phones. The degrees of freedom, offered to users to interact with these systems, enhance their flexibility and adaptability to different kinds of users, such as people with special needs, as well as to dynamic environments and ambient systems. The choice given to use one or more modalities improves their accessibility to various usage contexts, and enhances the performance stability, the robustness, as well as the efficiency of communication. For example, the user may interact with the system by using speech or, if the environment is too noisy, he/she can use press keys.
The development of such systems has been studied through different aspects. The usability of User Interfaces is a one of these aspects. It is a measure of the efficiency and satisfaction with which users can achieve their goals through these UIs. It is captured through a set of properties called usability properties. Many usability properties were defined for WIMP (Window, Icon, Mouse, and Pointing device) interfaces and MUIs, but the characteristics of mobile systems require the consideration of new properties that must be satisfied to increase their usability. For instance, in a mobile environment users can switch between modalities according to their efficiency in a given environment. In an ambient system, users having different profiles must be able to interact with the system. The user profile and environment variations involve changes that must be considered for the interaction. This forces the UI developers to take into account new properties such as adaptability. The adaptability property states that the UI remains usable even if some changes have occurred within the interaction environment, like the disability of an interaction device or the user has special needs. This property is very useful for mobile systems since it increases the users’ satisfaction.