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.
Automatic validation of computational models using pseudo-3D spatio-temporal model checking
